Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: equip u2 x0.
Claim L1: atleastp u2 x0
Apply equip_atleastp with u2, x0.
The subproof is completed by applying H0.
Apply unknownprop_8d334858d1804afd99b1b9082715c7f916daee31e697b66b5c752e0c8756ebae with x0, ∃ x1 . and (x1x0) (∃ x2 . and (x2x0) (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: x1x0.
Let x2 of type ι be given.
Assume H3: x2x0.
Assume H4: x1 = x2∀ x3 : ο . x3.
Let x3 of type ο be given.
Assume H5: ∀ x4 . and (x4x0) (∃ x5 . and (x5x0) (and (x4 = x5∀ x6 : ο . x6) (x0 = UPair x4 x5)))x3.
Apply H5 with x1.
Apply andI with x1x0, ∃ x4 . and (x4x0) (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 (x5x0) (and (x1 = x5∀ x6 : ο . x6) (x0 = UPair x1 x5))x4.
Apply H6 with x2.
Apply andI with x2x0, 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: x5x0.
Apply dneg with x5UPair x1 x2.
Assume H8: nIn 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 . x5UPair x7 x2.
The subproof is completed by applying UPairI1 with x5, x2.
Assume H9: x2 = x5.
Apply H8.
Apply H9 with λ x6 x7 . x5UPair 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: x5UPair x1 x2.
Apply UPairE with x5, x1, x2, x5x0 leaving 3 subgoals.
The subproof is completed by applying H7.
Assume H8: x5 = x1.
Apply H8 with λ x6 x7 . x7x0.
The subproof is completed by applying H2.
Assume H8: x5 = x2.
Apply H8 with λ x6 x7 . x7x0.
The subproof is completed by applying H3.