Let x0 of type ι be given.
Apply equip_atleastp with
u2,
x0.
The subproof is completed by applying H0.
Apply unknownprop_8d334858d1804afd99b1b9082715c7f916daee31e697b66b5c752e0c8756ebae with
x0,
∃ x1 . and (x1 ∈ x0) (∃ x2 . and (x2 ∈ x0) (and (x1 = x2 ⟶ ∀ x3 : ο . x3) (x0 = UPair x1 x2))) leaving 2 subgoals.
The subproof is completed by applying L1.
Let x1 of type ι be given.
Assume H2: x1 ∈ x0.
Let x2 of type ι be given.
Assume H3: x2 ∈ x0.
Assume H4: x1 = x2 ⟶ ∀ x3 : ο . x3.
Let x3 of type ο be given.
Assume H5:
∀ x4 . and (x4 ∈ x0) (∃ x5 . and (x5 ∈ x0) (and (x4 = x5 ⟶ ∀ x6 : ο . x6) (x0 = UPair x4 x5))) ⟶ x3.
Apply H5 with
x1.
Apply andI with
x1 ∈ x0,
∃ x4 . and (x4 ∈ x0) (and (x1 = x4 ⟶ ∀ x5 : ο . x5) (x0 = UPair x1 x4)) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x4 of type ο be given.
Assume H6:
∀ x5 . and (x5 ∈ x0) (and (x1 = x5 ⟶ ∀ x6 : ο . x6) (x0 = UPair x1 x5)) ⟶ x4.
Apply H6 with
x2.
Apply andI with
x2 ∈ x0,
and (x1 = x2 ⟶ ∀ x5 : ο . x5) (x0 = UPair x1 x2) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply andI with
x1 = x2 ⟶ ∀ x5 : ο . x5,
x0 = UPair x1 x2 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply set_ext with
x0,
UPair x1 x2 leaving 2 subgoals.
Let x5 of type ι be given.
Assume H7: x5 ∈ x0.
Apply dneg with
x5 ∈ UPair x1 x2.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
u2 leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply atleastp_tra with
u3,
x0,
u2 leaving 2 subgoals.
Apply unknownprop_8a21f6cb5fc1714044127ec01eb34af4a43c7190a9ab55c5830d9c24f7e274f6 with
x0,
x1,
x2,
x5 leaving 6 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
The subproof is completed by applying H4.
Assume H9: x1 = x5.
Apply H8.
Apply H9 with
λ x6 x7 . x5 ∈ UPair x7 x2.
The subproof is completed by applying UPairI1 with x5, x2.
Assume H9: x2 = x5.
Apply H8.
Apply H9 with
λ x6 x7 . x5 ∈ UPair x1 x7.
The subproof is completed by applying UPairI2 with x1, x5.
Apply equip_atleastp with
x0,
u2.
Apply equip_sym with
u2,
x0.
The subproof is completed by applying H0.
Let x5 of type ι be given.
Assume H7:
x5 ∈ UPair x1 x2.
Apply UPairE with
x5,
x1,
x2,
x5 ∈ x0 leaving 3 subgoals.
The subproof is completed by applying H7.
Assume H8: x5 = x1.
Apply H8 with
λ x6 x7 . x7 ∈ x0.
The subproof is completed by applying H2.
Assume H8: x5 = x2.
Apply H8 with
λ x6 x7 . x7 ∈ x0.
The subproof is completed by applying H3.