Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: equip u1 x0.
Apply H0 with ∃ x1 . and (x1x0) (x0 = Sing x1).
Let x1 of type ιι be given.
Assume H1: bij u1 x0 x1.
Apply bijE with u1, x0, x1, ∃ x2 . and (x2x0) (x0 = Sing x2) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: ∀ x2 . x2u1x1 x2x0.
Assume H3: ∀ x2 . x2u1∀ x3 . x3u1x1 x2 = x1 x3x2 = x3.
Assume H4: ∀ x2 . x2x0∃ x3 . and (x3u1) (x1 x3 = x2).
Let x2 of type ο be given.
Assume H5: ∀ x3 . and (x3x0) (x0 = Sing x3)x2.
Apply H5 with x1 0.
Apply andI with x1 0x0, x0 = Sing (x1 0) leaving 2 subgoals.
Apply H2 with 0.
The subproof is completed by applying In_0_1.
Apply set_ext with x0, Sing (x1 0) leaving 2 subgoals.
Let x3 of type ι be given.
Assume H6: x3x0.
Apply H4 with x3, x3Sing (x1 0) leaving 2 subgoals.
The subproof is completed by applying H6.
Let x4 of type ι be given.
Assume H7: (λ x5 . and (x5u1) (x1 x5 = x3)) x4.
Apply H7 with x3Sing (x1 0).
Assume H8: x41.
Apply cases_1 with x4, λ x5 . x1 x5 = x3x3Sing (x1 0) leaving 2 subgoals.
The subproof is completed by applying H8.
Assume H9: x1 0 = x3.
Apply H9 with λ x5 x6 . x3Sing x6.
The subproof is completed by applying SingI with x3.
Let x3 of type ι be given.
Assume H6: x3Sing (x1 0).
Apply SingE with x1 0, x3, λ x4 x5 . x5x0 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply H2 with 0.
The subproof is completed by applying In_0_1.