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.
The subproof is completed by applying L6.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H8: x2 ∈ x0.
Assume H9: x1 ⊆ x0.
Assume H10: x1 ⊆ x2.
Apply unknownprop_9c3c4976195baf6bd37497317b74ca268d712dfbd75862a7bcb0572a39ded839 with
u3,
x1,
False leaving 4 subgoals.
The subproof is completed by applying nat_3.
The subproof is completed by applying H7.
Let x3 of type ι be given.
Assume H12: x3 ∈ x1.
Apply L6 with
x3.
Apply H9 with
x3.
The subproof is completed by applying H12.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H13: x4 ∈ x1.
Assume H14: x3 ⊆ x1.
Assume H15: x3 ⊆ x4.
Apply unknownprop_9c3c4976195baf6bd37497317b74ca268d712dfbd75862a7bcb0572a39ded839 with
u2,
x3,
False leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying H12.
Let x5 of type ι be given.
Assume H22: x5 ∈ x3.
Apply L6 with
x5.
Apply H9 with
x5.
Apply H14 with
x5.
The subproof is completed by applying H22.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H23: x6 ∈ x3.
Assume H24: x5 ⊆ x3.
Assume H25: x5 ⊆ x6.
Apply unknownprop_bf17ea03608bec2ab1db40555d0b2aea03020efffda1ccd3dabfc161366b81c8 with
x2,
λ x7 . x2 = x7 ⟶ ∀ x8 : ο . x8 leaving 6 subgoals.
Apply setminusI with
u16,
u12,
x2 leaving 2 subgoals.
Apply H0 with
x2.
The subproof is completed by applying H8.
Let x7 of type ι be given.
Apply binunionE with
x1,
Sing x2,
x7,
x7 ∈ u12 leaving 3 subgoals.
The subproof is completed by applying H41.
Apply unknownprop_82a4043338dce48d58934c215ccdbe85be545db6869ac125d5e92b153cac28bb with
binunion x1 (Sing x2) leaving 3 subgoals.
The subproof is completed by applying L41.
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
λ x7 x8 . equip x7 (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 H7.
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 x7 of type ι be given.
Assume H42: x7 ∈ x1.
Assume H43:
x7 ∈ Sing x2.
Apply In_irref with
x2.
Apply SingE with
x2,
x7,
λ x8 x9 . x8 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying H43.
Apply H10 with
x7.
The subproof is completed by applying H42.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H44: x7 = x8 ⟶ ∀ x9 : ο . x9.
Apply H4 with
x7,
x8 leaving 4 subgoals.
Apply L11 with
x7.
The subproof is completed by applying H42.
Apply L11 with
x8.
The subproof is completed by applying H43.
The subproof is completed by applying H44.
Apply unknownprop_331d7f66eeb37dc381bf2e3606d3b3c601f9b8768b689e8985564581b76a5fdc with
x7,
x8 leaving 3 subgoals.
Apply unknownprop_46307dd0174fa26aaad235a343e8b6e719715159a425e7aad1f30f101888c98c with
x7.
Apply L41 with
x7.
The subproof is completed by applying H42.
Apply unknownprop_46307dd0174fa26aaad235a343e8b6e719715159a425e7aad1f30f101888c98c with
x8.
Apply L41 with
x8.
The subproof is completed by applying H43.
The subproof is completed by applying H45.