Let x0 of type ι be given.
Assume H2:
∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2).
Apply unknownprop_500d1e737e2209e4c583d05afc878803ba55ca9b82cd3357b41edde686af0c3b with
u6,
x0,
False leaving 4 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying H1.
The subproof is completed by applying L3.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H5: x2 ∈ x0.
Assume H6: x1 ⊆ x0.
Assume H7: x1 ⊆ x2.
Apply unknownprop_9c3c4976195baf6bd37497317b74ca268d712dfbd75862a7bcb0572a39ded839 with
u5,
x1,
False leaving 4 subgoals.
The subproof is completed by applying nat_5.
The subproof is completed by applying H4.
Let x3 of type ι be given.
Assume H8: x3 ∈ x1.
Apply L3 with
x3.
Apply H6 with
x3.
The subproof is completed by applying H8.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H9: x4 ∈ x1.
Assume H10: x3 ⊆ x1.
Assume H11: x3 ⊆ x4.
Apply unknownprop_385697d8441c5f778e16c97ac3fd3d842ad68223c4d1882ce705cb1375e178b5 with
x4,
λ x5 . x4 = x5 ⟶ False leaving 7 subgoals.
Apply setminusI with
u22,
u17,
x4 leaving 2 subgoals.
Apply H0 with
x4.
Apply H6 with
x4.
The subproof is completed by applying H9.
The subproof is completed by applying L17.
Apply unknownprop_385697d8441c5f778e16c97ac3fd3d842ad68223c4d1882ce705cb1375e178b5 with
x2,
λ x5 . x2 = x5 ⟶ False leaving 7 subgoals.
The subproof is completed by applying L19.
Apply In_irref with
x2.
Apply H21 with
λ x5 x6 . x6 ∈ x2.
Apply H20 with
λ x5 x6 . x5 ∈ x2.
The subproof is completed by applying L13.
Apply L14.
Apply H20 with
λ x5 x6 . 0aea9.. x6 x2.
Apply H21 with
λ x5 x6 . 0aea9.. u17 x6.
The subproof is completed by applying unknownprop_851ce1d42fc45a6a636e8fc2b70c48e32b67c56703b52990b181e84673fc1c05.
Let x5 of type ι be given.
Assume H22: x5 ∈ x3.
Apply unknownprop_14e19ebc7e16f882d3be4482dbe497cecb7597969c9cae0a9f87fe87a0ee217a with
x5,
λ x6 . x6 ∈ x3 ⟶ x6 ∈ u12 leaving 19 subgoals.
Apply H20 with
λ x6 x7 . x3 ⊆ x6,
x5 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H22.
Assume H23: 0 ∈ x3.
The subproof is completed by applying unknownprop_a2ef0c58cfd090f3c9e6e7916f6b56032d6bdd4de509aa9fb32f7308f99daf5a.
The subproof is completed by applying unknownprop_b1b74a38cb206cf70f2e2bbc4ccd3cbdbf8c8df3defd64ff8c8a7258b3a2047a.
The subproof is completed by applying unknownprop_987ba5536dee4e8ff190eaeed4d2bb3ab5d85c45e6623acb29ce14f019a19681.
The subproof is completed by applying unknownprop_cf5ceb5c8b16071a67f4b018bbc8955118e3633f8bcf650790850107ad2027ee.
The subproof is completed by applying unknownprop_4fce167ccdcc7fb45429dcf8a3db15dc462c457fe760841310c58bc94a706ed3.
The subproof is completed by applying unknownprop_75d836f404cbbeae78f524a2ea7f26282023039d9accd25589aa1c1720bb8121.
The subproof is completed by applying unknownprop_73e4e62694bfb193433658c654297b6ed3eb985937a9e426b510b83e68de24d1.
The subproof is completed by applying unknownprop_a31357c4255c39823e518ff3fc8fa06c75e6252111ceae22b3d4f1c89a01d10b.
The subproof is completed by applying unknownprop_89f074e5696e72c1d0b8f6c7a30d07f4920551bfce89ff386ae0ecf5a82d48e4.
The subproof is completed by applying unknownprop_2453a2b3484043c8ce568faca0a1096a3c2d75e863532a7d5d6a9f964c17a76f.
The subproof is completed by applying unknownprop_e58cb2c6f977d1b0d5350ed902991ead1b80327bc1b160612a3fd1cd20c9fd3b.
The subproof is completed by applying unknownprop_2e87f3f906df12d03519748b94abd9f72cc673eb197d25aaf167a3737a0cc14b.
Apply FalseE with
u12 ∈ u12.
Apply H2 with
u12,
x2 leaving 4 subgoals.
Apply L16 with
u12.
The subproof is completed by applying H23.
The subproof is completed by applying H5.
Apply L18.
Apply H24 with
λ x6 x7 . x6 ∈ u17.
The subproof is completed by applying unknownprop_b7a4a37161804b376f25028de76b0714142123cbd842ba90c86afe8baa6a8a9e.
Apply H21 with
λ x6 x7 . 0aea9.. u12 x7.
Apply unknownprop_750bbfd209cbbc2638525ff49836b8d57a9d46b5b0085915178b80f8528ec332 with
λ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. x7 (55574.. u19) = λ x8 x9 . x8.
Apply unknownprop_82a4043338dce48d58934c215ccdbe85be545db6869ac125d5e92b153cac28bb with
x3 leaving 3 subgoals.
The subproof is completed by applying L22.
Apply equip_atleastp with
u5,
x3.
The subproof is completed by applying H8.
Let x5 of type ι be given.
Assume H23: x5 ∈ x3.
Let x6 of type ι be given.
Assume H24: x6 ∈ x3.
Assume H25: x5 = x6 ⟶ ∀ x7 : ο . x7.
Apply H2 with
x5,
x6 leaving 4 subgoals.
Apply L16 with
x5.
The subproof is completed by applying H23.
Apply L16 with
x6.
The subproof is completed by applying H24.
The subproof is completed by applying H25.
Apply unknownprop_331d7f66eeb37dc381bf2e3606d3b3c601f9b8768b689e8985564581b76a5fdc with
x5,
x6 leaving 3 subgoals.
Apply unknownprop_46307dd0174fa26aaad235a343e8b6e719715159a425e7aad1f30f101888c98c with
x5.
Apply L22 with
x5.
The subproof is completed by applying H23.
Apply unknownprop_46307dd0174fa26aaad235a343e8b6e719715159a425e7aad1f30f101888c98c with
x6.
Apply L22 with
x6.
The subproof is completed by applying H24.
The subproof is completed by applying H26.