Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H0: UPair (UPair x0 x1) (Sing x0) = UPair (UPair x2 x3) (Sing x2).
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: UPair x0 x3 ∈ UPair (UPair x0 x1) (Sing x0)
Apply L2 with λ x4 x5 . UPair x0 x3 ∈ x5.
The subproof is completed by applying L3.
Apply UPairE with UPair x0 x3, UPair x0 x1, Sing x0, x1 = x3 leaving 3 subgoals.
The subproof is completed by applying L4.
Assume H5: UPair x0 x3 = UPair x0 x1.
Claim L6: x1 ∈ UPair x0 x3
Apply H5 with λ x4 x5 . x1 ∈ x5.
The subproof is completed by applying UPairI2 with x0, x1.
Apply UPairE with x1, x0, x3, x1 = x3 leaving 3 subgoals.
The subproof is completed by applying L6.
Assume H7: x1 = x0.
Claim L8: x3 ∈ UPair x0 x1
Apply H5 with λ x4 x5 . x3 ∈ x4.
The subproof is completed by applying UPairI2 with x0, x3.
Apply UPairE with x3, x0, x1, x1 = x3 leaving 3 subgoals.
The subproof is completed by applying L8.
Assume H9: x3 = x0.
Apply H9 with λ x4 x5 . x1 = x5.
The subproof is completed by applying H7.
Assume H9: x3 = x1.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H9 with λ x5 x6 . x4 x6 x5.
Assume H7: x1 = x3.
The subproof is completed by applying H7.
Assume H5: UPair x0 x3 = Sing x0.
Claim L6: Sing x0 = UPair x0 x3
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H5 with λ x5 x6 . x4 x6 x5.
Apply Sing_inv with x0, UPair x0 x3, x1 = x3 leaving 2 subgoals.
The subproof is completed by applying L6.
Assume H7: x0 ∈ UPair x0 x3.
Assume H8: ∀ x4 . x4 ∈ UPair x0 x3 ⟶ x4 = x0.
Claim L9: x3 = x0
Apply H8 with x3.
The subproof is completed by applying UPairI2 with x0, x3.
Apply L9 with λ x4 x5 . x1 = x5.
Claim L10: UPair (UPair x0 x1) (Sing x0) = UPair (UPair x0 x0) (Sing x0)
Apply L9 with λ x4 x5 . UPair (UPair x0 x1) (Sing x0) = UPair (UPair x0 x4) (Sing x0).
The subproof is completed by applying L2.
Claim L11: UPair x0 x1 ∈ Sing (Sing x0)
Apply unknownprop_36456668efb81fed7214a2a55c58885a793c080b2e11698015706b30a4b318d6 with Sing x0, λ x4 x5 . UPair x0 x1 ∈ x5.
Apply unknownprop_36456668efb81fed7214a2a55c58885a793c080b2e11698015706b30a4b318d6 with x0, λ x4 x5 . UPair x0 x1 ∈ UPair x5 (Sing x0).
Apply L10 with λ x4 x5 . UPair x0 x1 ∈ x4.
The subproof is completed by applying UPairI1 with UPair x0 x1, Sing x0.
Claim L12: Sing x0 = UPair x0 x1
Let x4 of type ι → ι → ο be given.
Apply SingE with Sing x0, UPair x0 x1, λ x5 x6 . x4 x6 x5.
The subproof is completed by applying L11.
Apply Sing_inv with x0, UPair x0 x1, x1 = x0 leaving 2 subgoals.
The subproof is completed by applying L12.
Assume H13: x0 ∈ UPair x0 x1.
Assume H14: ∀ x4 . x4 ∈ UPair x0 x1 ⟶ x4 = x0.
Apply H14 with x1.
The subproof is completed by applying UPairI2 with x0, x1.
■