Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι → ο be given.
Apply unknownprop_bb6913ebe2634287cee79eec3455dee22199094183798d61ce3f582de16f34dd with x0, λ x2 . In x2 (PSNo x0 x1), x1.
Let x2 of type ι be given.
Assume H1: In x2 x0.
Apply unknownprop_a818f53272de918398012791887b763f90bf043f961a4f625d98076ca0b8b392 with In x2 (PSNo x0 x1), x1 x2 leaving 2 subgoals.
Claim L2: ∀ x3 . In x3 x0 ⟶ x1 x3 ⟶ In x3 x0 ⟶ x1 x3
Let x3 of type ι be given.
Assume H2: In x3 x0.
Assume H3: x1 x3.
Assume H4: In x3 x0.
The subproof is completed by applying H3.
Claim L3: ∀ x3 . In x3 x0 ⟶ not (x1 x3) ⟶ In ((λ x4 . SetAdjoin x4 (Sing 1)) x3) x0 ⟶ x1 ((λ x4 . SetAdjoin x4 (Sing 1)) x3)
Let x3 of type ι be given.
Assume H3: In x3 x0.
Assume H4: not (x1 x3).
Assume H5: In ((λ x4 . SetAdjoin x4 (Sing 1)) x3) x0.
Apply FalseE with x1 ((λ x4 . SetAdjoin x4 (Sing 1)) x3).
Apply unknownprop_a42f4d742e476dc9e91f3062bb40a923513a37a8678f32dfc5f9e261116d23ba with x0, x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
Assume H4: In x2 (PSNo x0 x1).
Apply unknownprop_6a486d2f7d911fc69f373a3a2aa953ced5a8fb2233dc09710907454779c0b8a5 with x0, x1, λ x3 . In x3 x0 ⟶ x1 x3, x2 leaving 4 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Assume H2: x1 x2.
Apply unknownprop_26f5054f55e1cc99d707390045c57973d733124f73202e22abda7782932b774a with x0, x1, x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
■