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 x0PNo_lenbdd x2 x1∀ x3 : ι → ο . 8033b.. x0 x1 x2 x38033b.. x0 x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2∀ x5 : ο . x5)).
Assume H1: TransSet x2.
Assume H2: ∀ x3 . prim1 x3 x2TransSet 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 . and (x3 x4) (x4 = x2∀ x5 : ο . x5)).
Assume H6: 6f2c4.. x0 x2 x3.
Assume H7: dafc2.. x1 x2 x3.
Claim L8: ...
...
Claim L9: ...
...
Apply andI with 6f2c4.. x0 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2∀ x5 : ο . x5)), dafc2.. x1 (4ae4a.. x2) (λ x4 . and (x3 x4) (x4 = x2∀ x5 : ο . x5)) 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 H11 with 40dde.. x4 x5 (4ae4a.. x2) (λ x6 . and (x3 x6) (x6 = x2∀ x7 : ο . x7)).
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 (4ae4a.. x2) (λ x7 . and (x3 x7) (x7 = x2∀ x8 : ο . x8)).
Assume H14: ordinal x6.
Assume H15: ∃ x7 : ι → ο . and (x0 x6 x7) (35b9b.. x4 x5 x6 x7).
Apply H15 with 40dde.. x4 x5 (4ae4a.. x2) (λ x7 . and (x3 x7) (x7 = x2∀ x8 : ο . x8)).
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 (4ae4a.. x2) (λ x8 . and (x3 x8) (x8 = x2∀ x9 : ο . x9)).
Assume H17: x0 x6 x7.
Assume H18: 35b9b.. x4 x5 x6 x7.
Apply unknownprop_81ad141295a808fea0b45ad277e31915f7577f7fce50f799a6434a1b613c1ee0 with x4, x6, 4ae4a.. x2, x5, x7, λ x8 . and (x3 x8) (x8 = x2∀ x9 : ο . x9) leaving 5 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H14.
The subproof is completed by applying L8.
The subproof is completed by applying H18.
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Apply unknownprop_73b6444bcb1b9cb998566f55e286e78644e785a99d955b3281cf269899ab486c with x6, 4ae4a.. x2, x7, λ x8 . and (x3 x8) (x8 = x2∀ x9 : ο . x9), 40dde.. x6 x7 (4ae4a.. x2) (λ x8 . and (x3 x8) (x8 = x2∀ x9 : ο . x9)) leaving 4 subgoals.
...
...
...
...
...