Let x0 of type ι be given.
Assume H4:
∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (0aea9.. x1 x2).
Apply unknownprop_500d1e737e2209e4c583d05afc878803ba55ca9b82cd3357b41edde686af0c3b with
u4,
x0,
False leaving 4 subgoals.
The subproof is completed by applying nat_4.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H5: x1 ∈ x0.
Apply nat_p_ordinal with
x1.
Apply nat_p_trans with
u18,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b6349b103ec0c23863292fe6c57a85341c64566cbff4099647a6f20c72c67730.
Apply H0 with
x1.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H6: x2 ∈ x0.
Assume H7: x1 ⊆ x0.
Assume H8: x1 ⊆ x2.
Apply unknownprop_935b4a8fadd952cd34e110361e4180aa6697c0a19acd68c7a8d8ecd0a08c957f with
x2,
λ x3 . x2 = x3 ⟶ ∀ x4 : ο . x4 leaving 8 subgoals.
Apply setminusI with
u18,
u12,
x2 leaving 2 subgoals.
Apply H0 with
x2.
The subproof is completed by applying H6.
Let x3 of type ι be given.
Apply binunionE with
x1,
Sing x2,
x3,
x3 ∈ u12 leaving 3 subgoals.
The subproof is completed by applying H11.
Assume H12: x3 ∈ x1.
Apply nat_trans with
u12,
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying nat_12.
The subproof is completed by applying H10.
Apply H8 with
x3.
The subproof is completed by applying H12.
Assume H12:
x3 ∈ Sing x2.
Apply SingE with
x2,
x3,
λ x4 x5 . x5 ∈ u12 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H10.
Apply unknownprop_82a4043338dce48d58934c215ccdbe85be545db6869ac125d5e92b153cac28bb with
binunion x1 (Sing x2) leaving 3 subgoals.
The subproof is completed by applying L11.
Apply equip_atleastp with
u5,
binunion x1 (Sing x2).
Apply equip_tra with
u5,
setsum x1 (Sing x2),
binunion x1 (Sing x2) leaving 2 subgoals.
Apply unknownprop_150e303ecf8a7227a9f23528d11666f9ad495de0a25ae8fba20dedf2c3db2f83 with
λ x3 x4 . equip x3 (setsum x1 (Sing x2)).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
u4,
u1,
x1,
Sing x2 leaving 4 subgoals.
The subproof is completed by applying nat_4.
The subproof is completed by applying nat_1.
The subproof is completed by applying H5.
Apply equip_sym with
Sing x2,
u1.
The subproof is completed by applying unknownprop_be1ab2772f2343e1b7afd526582f606d68258ba3f0b6521a351e0ecb8bf3c52e with x2.
Apply equip_sym with
binunion x1 (Sing x2),
setsum x1 (Sing x2).
Apply unknownprop_8fed54475e70b18fbe9db03f1a81cd38ab9b210f0bea8d2bb706323c288b83da with
x1,
Sing x2,
x1,
Sing x2 leaving 3 subgoals.
The subproof is completed by applying equip_ref with x1.
The subproof is completed by applying equip_ref with
Sing x2.
Let x3 of type ι be given.
Assume H12: x3 ∈ x1.
Assume H13:
x3 ∈ Sing x2.
Apply In_irref with
x2.
Apply SingE with
x2,
x3,
λ x4 x5 . x4 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying H13.
Apply H8 with
x3.
The subproof is completed by applying H12.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H14: x3 = x4 ⟶ ∀ x5 : ο . x5.
Apply H4 with
x3,
x4 leaving 4 subgoals.
Apply L9 with
x3.
The subproof is completed by applying H12.
Apply L9 with
x4.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
Apply unknownprop_331d7f66eeb37dc381bf2e3606d3b3c601f9b8768b689e8985564581b76a5fdc with
x3,
x4 leaving 3 subgoals.
Apply unknownprop_46307dd0174fa26aaad235a343e8b6e719715159a425e7aad1f30f101888c98c with
x3.
Apply L11 with
x3.
The subproof is completed by applying H12.
Apply unknownprop_46307dd0174fa26aaad235a343e8b6e719715159a425e7aad1f30f101888c98c with
x4.
Apply L11 with
x4.
The subproof is completed by applying H13.
The subproof is completed by applying H15.
Apply H2 with
x2 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H10 with
λ x3 x4 . 94591.. (55574.. x4) (55574.. u19) = λ x5 x6 . x5.
Apply unknownprop_750bbfd209cbbc2638525ff49836b8d57a9d46b5b0085915178b80f8528ec332 with
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. x4 (55574.. u19) = λ x5 x6 . x5.
Apply unknownprop_9ef01be1d276345c463186441a5675fe07097ab01b8002e94389de481ccaa0f8 with
λ x3 x4 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. (λ x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 . x17) x4 = λ x5 x6 . x5.
Let x3 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.