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.
Assume H0: ordinal x2.
Apply H0 with PNo_lenbdd x2 x0 ⟶ PNo_lenbdd x2 x1 ⟶ ∀ x3 : ι → ο . 8033b.. x0 x1 x2 x3 ⟶ 8033b.. x0 x1 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)).
Assume H1: TransSet x2.
Assume H2: ∀ x3 . prim1 x3 x2 ⟶ TransSet x3.
Assume H3: PNo_lenbdd x2 x0.
Assume H4: PNo_lenbdd x2 x1.
Let x3 of type ι → ο be given.
Assume H5: 8033b.. x0 x1 x2 x3.
Apply H5 with 8033b.. x0 x1 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)).
Assume H6: 6f2c4.. x0 x2 x3.
Assume H7: dafc2.. x1 x2 x3.
Claim L8: ...
...
Claim L9: ...
...
Apply andI with 6f2c4.. x0 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)), dafc2.. x1 (4ae4a.. x2) (λ x4 . or (x3 x4) (x4 = x2)) leaving 2 subgoals.
Let x4 of type ι be given.
Assume H10: prim1 x4 (4ae4a.. x2).
Let x5 of type ι → ο be given.
Assume H11: 8356a.. x0 x4 x5.
Claim L12: ...
...
Apply unknownprop_37f5b5c6ee0011f262b499567d54413188e5bd83bd5555e5f3caca08d2fd472f with x4, x2, 4ae4a.. x2, x5, x3, λ x6 . or (x3 x6) (x6 = x2) leaving 5 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H0.
The subproof is completed by applying L8.
Apply H11 with 40dde.. x4 x5 x2 x3.
Let x6 of type ι be given.
Assume H13: (λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (35b9b.. x4 x5 x7 x8))) x6.
Apply H13 with 40dde.. x4 x5 x2 x3.
Assume H14: ordinal x6.
Assume H15: ∃ x7 : ι → ο . and (x0 x6 x7) (35b9b.. x4 x5 x6 x7).
Apply H15 with 40dde.. x4 x5 x2 x3.
Let x7 of type ι → ο be given.
Assume H16: (λ x8 : ι → ο . and (x0 x6 x8) (35b9b.. x4 x5 x6 x8)) x7.
Apply H16 with 40dde.. x4 x5 x2 x3.
Assume H17: x0 x6 x7.
Assume H18: 35b9b.. x4 x5 x6 x7.
Claim L19: 8356a.. x0 x6 x7
Let x8 of type ο be given.
Assume H19: ∀ x9 . and (ordinal x9) (∃ x10 : ι → ο . and (x0 x9 x10) (35b9b.. x6 x7 x9 x10)) ⟶ x8.
Apply H19 with x6.
Apply andI with ordinal x6, ∃ x9 : ι → ο . and (x0 x6 x9) (35b9b.. x6 x7 x6 x9) leaving 2 subgoals.
The subproof is completed by applying H14.
Let x9 of type ο be given.
Assume H20: ∀ x10 : ι → ο . and (x0 x6 x10) (35b9b.. x6 x7 x6 x10) ⟶ x9.
Apply H20 with x7.
Apply andI with x0 x6 x7, 35b9b.. x6 x7 x6 x7 leaving 2 subgoals.
The subproof is completed by applying H17.
The subproof is completed by applying unknownprop_ac07215c6ebe89023e9a4e8747fc5b9f09008a47b8850229ec563a36216227e7 with x6, x7.
Apply unknownprop_81ad141295a808fea0b45ad277e31915f7577f7fce50f799a6434a1b613c1ee0 with x4, x6, x2, x5, x7, x3 leaving 5 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H14.
The subproof is completed by applying H0.
The subproof is completed by applying H18.
Apply H6 with x6, x7 leaving 2 subgoals.
Apply H3 with x6, x7.
The subproof is completed by applying H17.
The subproof is completed by applying L19.
...
...
■