Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ setminus omega 2.
Let x1 of type ο be given.
Assume H1: ∀ x2 . x2 ∈ omega ⟶ x0 = ordsucc (ordsucc x2) ⟶ x1.
Apply setminusE with omega, 2, x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2: x0 ∈ omega.
Assume H3: nIn x0 2.
Claim L4: x0 ∈ setminus omega 1
Apply setminusI with omega, 1, x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H4: x0 ∈ 1.
Apply H3.
Apply Subq_1_2 with x0.
The subproof is completed by applying H4.
Apply unknownprop_e18849ea271b9fad1d1f55210e57a4e42a5b850b4f5bda4268b35baef08a0fd5 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying L4.
Let x2 of type ι be given.
Assume H5: x2 ∈ omega.
Assume H6: x0 = ordsucc x2.
Claim L7: x2 ∈ setminus omega 1
Apply setminusI with omega, 1, x2 leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H7: x2 ∈ 1.
Apply H3.
Apply H6 with λ x3 x4 . x4 ∈ 2.
Apply ordinal_ordsucc_In with 1, x2 leaving 2 subgoals.
The subproof is completed by applying ordinal_1.
The subproof is completed by applying H7.
Apply unknownprop_e18849ea271b9fad1d1f55210e57a4e42a5b850b4f5bda4268b35baef08a0fd5 with x2, x1 leaving 2 subgoals.
The subproof is completed by applying L7.
Let x3 of type ι be given.
Assume H8: x3 ∈ omega.
Assume H9: x2 = ordsucc x3.
Apply H1 with x3 leaving 2 subgoals.
The subproof is completed by applying H8.
Apply H9 with λ x4 x5 . x0 = ordsucc x4.
The subproof is completed by applying H6.
■