Let x0 of type ι be given.
Assume H2:
∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ 0aea9.. x1 x2.
Apply unknownprop_5a83a108ad757ace387d2c518b5833379f1ee4db5a9903e44819e140b2ab80ec with
x0,
False leaving 3 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H3: x1 ∈ x0.
Apply nat_p_ordinal with
x1.
Apply nat_p_trans with
u22,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c873eeccdf6e645ee19271ea61e3647072d01ff54e75e19478129f6b14f6a5a5.
Apply H0 with
x1.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H3: x1 ∈ x0.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Let x3 of type ι be given.
Assume H5: x3 ∈ x0.
Assume H6: x1 ∈ x2.
Assume H7: x2 ∈ x3.
set y4 to be ...
Apply unknownprop_385697d8441c5f778e16c97ac3fd3d842ad68223c4d1882ce705cb1375e178b5 with
x3,
λ x5 . x3 = x5 ⟶ ∀ x6 : ο . x6 leaving 7 subgoals.
Apply setminusI with
u22,
u17,
x3 leaving 2 subgoals.
Apply H0 with
x3.
The subproof is completed by applying H5.
Apply nat_trans with
u17,
x3,
x2 leaving 3 subgoals.
The subproof is completed by applying nat_17.
The subproof is completed by applying H13.
The subproof is completed by applying H7.
Apply L12 with
λ x5 . x5 ∈ u17 leaving 3 subgoals.
Apply nat_trans with
u17,
x2,
x1 leaving 3 subgoals.
The subproof is completed by applying nat_17.
The subproof is completed by applying L14.
The subproof is completed by applying H6.
The subproof is completed by applying L14.
The subproof is completed by applying H13.
Apply unknownprop_97757aa046fc628a1493769feaf18aac5937e0cb3d98e54a6c0796c9e5514262 with
y4 leaving 3 subgoals.
The subproof is completed by applying L15.
Apply L11 with
λ x5 x6 . atleastp u3 x6.
Apply unknownprop_11c6158bd93dbd27daaa9a84a43404be6ccbf75f900b1e28dfa453e64ea6c96b with
u2,
UPair x1 x2,
x3 leaving 2 subgoals.
Assume H16:
x3 ∈ UPair x1 x2.
Apply UPairE with
x3,
x1,
x2,
False leaving 3 subgoals.
The subproof is completed by applying H16.
Assume H17: x3 = x1.
Apply In_no2cycle with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply H17 with
λ x5 x6 . x6 ∈ x2.
The subproof is completed by applying H6.
Assume H17: x3 = x2.
Apply In_irref with
x3.
Apply H17 with
λ x5 x6 . x6 ∈ x3.
The subproof is completed by applying H7.
Apply equip_atleastp with
u2,
UPair x1 x2.
Apply unknownprop_3ec052b482c9586393801a691570db7db5e41e6f5045529f723594be820ae083 with
UPair x1 x2,
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying UPairI1 with x1, x2.
The subproof is completed by applying UPairI2 with x1, x2.
Assume H16: x1 = x2.
Apply In_irref with
x1.
Apply H16 with
λ x5 x6 . x1 ∈ x6.
The subproof is completed by applying H6.
Let x5 of type ι be given.
The subproof is completed by applying UPairE with x5, x1, x2.
Let x5 of type ι be given.
Assume H16: x5 ∈ y4.
Let x6 of type ι be given.
Assume H17: x6 ∈ y4.
Assume H18: x5 = x6 ⟶ ∀ x7 : ο . x7.
Apply unknownprop_e16ab3d50baafeaf90a0ee1065332204d3827bebf1dd68c1acb8dccd52cf984e with
x5,
x6 leaving 3 subgoals.
Apply L15 with
x5.
The subproof is completed by applying H16.
Apply L15 with
x6.
The subproof is completed by applying H17.
Apply H2 with
x5,
x6 leaving 3 subgoals.
Apply L12 with
λ x7 . x7 ∈ x0,
x5 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H16.
Apply L12 with
λ x7 . x7 ∈ x0,
x6 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
Apply unknownprop_14e19ebc7e16f882d3be4482dbe497cecb7597969c9cae0a9f87fe87a0ee217a with
x2,
λ x5 . x2 = x5 ⟶ ∀ x6 : ο . x6 leaving 19 subgoals.
Apply H13 with
λ x5 x6 . x2 ∈ x5.
The subproof is completed by applying H7.
Assume H14: x2 = 0.
Apply EmptyE with
x1.
Apply H14 with
λ x5 x6 . x1 ∈ x5.
The subproof is completed by applying H6.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
Apply unknownprop_d32c2e377314b1972e17c149653f6099c7ac9647b19ffa42c03b41634506f348 with
λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. (λ x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 . x8) x5 = λ x7 x8 . x7.
Apply unknownprop_6479a43174f47c77b90f2d570c9fecae99b692135893ea46f64f47a06da93bf8 with
λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. x5 (55574.. u17) = λ x7 x8 . x7.
Apply H13 with
λ x5 x6 . 0aea9.. u1 x5 leaving 3 subgoals.
Apply H14 with
λ x5 x6 . 0aea9.. x5 x3.
The subproof is completed by applying L10.
The subproof is completed by applying unknownprop_1afe5bcc1ba465f8960fb0a631ff7e0909f148989239e1a12216b32c4243fcb9.
The subproof is completed by applying unknownprop_73689b0c9165815f69613261fb00fc9845786a5bb0f82650ada96717b3516f42.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
Apply unknownprop_d32c2e377314b1972e17c149653f6099c7ac9647b19ffa42c03b41634506f348 with
λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. (λ x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 . x9) x5 = λ x7 x8 . x7.
Apply unknownprop_7d6f755c8dc7037da5498a72b88a0cb818b42f84cba832342d390734f147b368 with
λ x5 x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. x5 (55574.. u17) = λ x7 x8 . x7.
Apply H13 with
λ x5 x6 . 0aea9.. u2 x5 leaving 3 subgoals.
Apply H14 with
λ x5 x6 . 0aea9.. x5 x3.
The subproof is completed by applying L10.
The subproof is completed by applying unknownprop_c273888099fc7f5bb484aed59e7b9ddaa3881c926823f96bfbe4f41471c65743.
The subproof is completed by applying unknownprop_73689b0c9165815f69613261fb00fc9845786a5bb0f82650ada96717b3516f42.