Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2:
∀ x2 . x2 ∈ x1 ⟶ ordinal x2.
Let x2 of type ο be given.
Assume H3:
∀ x3 x4 . equip x0 x3 ⟶ x4 ∈ x1 ⟶ x3 ⊆ x1 ⟶ x3 ⊆ x4 ⟶ x1 = binunion x3 (Sing x4) ⟶ x2.
Apply unknownprop_500d1e737e2209e4c583d05afc878803ba55ca9b82cd3357b41edde686af0c3b with
x0,
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply equip_atleastp with
ordsucc x0,
x1.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H5: x4 ∈ x1.
Assume H6: x3 ⊆ x1.
Assume H7: x3 ⊆ x4.
Apply H3 with
x3,
x4 leaving 5 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Let x5 of type ι → ι → ο be given.
Apply unknownprop_47f88c1ef3f7e70202dad4a7dc31cddd63e4c9699c68a0cdfa175af999543412 with
binunion x3 (Sing x4),
x1,
λ x6 x7 . x5 x7 x6 leaving 3 subgoals.
Apply adjoin_finite with
x3,
x4.
Let x6 of type ο be given.
Apply H8 with
x0.
Apply andI with
x0 ∈ omega,
equip x3 x0 leaving 2 subgoals.
Apply nat_p_omega with
x0.
The subproof is completed by applying H0.
Apply equip_sym with
x0,
x3.
The subproof is completed by applying H4.
Apply equip_atleastp with
x1,
binunion x3 (Sing x4).
Apply equip_tra with
x1,
ordsucc x0,
binunion x3 (Sing x4) leaving 2 subgoals.
Apply equip_sym with
ordsucc x0,
x1.
The subproof is completed by applying H1.
Apply add_nat_0R with
x0,
λ x6 x7 . equip (ordsucc x6) (binunion x3 (Sing x4)).
Apply add_nat_SR with
x0,
0,
λ x6 x7 . equip x6 (binunion x3 (Sing x4)) leaving 2 subgoals.
The subproof is completed by applying nat_0.
Apply equip_tra with
add_nat x0 1,
setsum x0 1,
binunion x3 (Sing x4) leaving 2 subgoals.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
x0,
1,
x0,
1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying nat_1.
The subproof is completed by applying equip_ref with x0.
The subproof is completed by applying equip_ref with 1.
Apply equip_sym with
binunion x3 (Sing x4),
setsum x0 1.
Apply unknownprop_8fed54475e70b18fbe9db03f1a81cd38ab9b210f0bea8d2bb706323c288b83da with
x3,
Sing x4,
x0,
1 leaving 3 subgoals.
Apply equip_sym with
x0,
x3.
The subproof is completed by applying H4.
The subproof is completed by applying unknownprop_be1ab2772f2343e1b7afd526582f606d68258ba3f0b6521a351e0ecb8bf3c52e with x4.
Let x6 of type ι be given.
Assume H8: x6 ∈ x3.
Apply In_irref with
x4.
Apply H7 with
x4.
Apply SingE with
x4,
x6,
λ x7 x8 . x7 ∈ x3 leaving 2 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H8.
Apply binunion_Subq_min with
x3,
Sing x4,
x1 leaving 2 subgoals.
The subproof is completed by applying H6.
Let x6 of type ι be given.
Apply SingE with
x4,
x6,
λ x7 x8 . x8 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H5.