Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ιι be given.
Assume H0: ∀ x2 . x2x0ordinal (x1 x2).
Apply andI with TransSet (famunion x0 (λ x2 . x1 x2)), ∀ x2 . x2famunion x0 (λ x3 . x1 x3)TransSet x2 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H1: x2famunion x0 (λ x3 . x1 x3).
Apply famunionE with x0, x1, x2, x2famunion x0 x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H2: (λ x4 . and (x4x0) (x2x1 x4)) x3.
Apply H2 with x2famunion x0 x1.
Assume H3: x3x0.
Assume H4: x2x1 x3.
Claim L5: ordinal (x1 x3)
Apply H0 with x3.
The subproof is completed by applying H3.
Apply L5 with x2famunion x0 (λ x4 . x1 x4).
Assume H6: TransSet (x1 x3).
Assume H7: ∀ x4 . x4x1 x3TransSet x4.
Let x4 of type ι be given.
Assume H8: x4x2.
Claim L9: x4x1 x3
Apply H6 with x2, x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply famunionI with x0, x1, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L9.
Let x2 of type ι be given.
Assume H1: x2famunion x0 (λ x3 . x1 x3).
Apply famunionE with x0, x1, x2, TransSet x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H2: (λ x4 . and (x4x0) (x2x1 x4)) x3.
Apply H2 with TransSet x2.
Assume H3: x3x0.
Assume H4: x2x1 x3.
Claim L5: ordinal (x1 x3)
Apply H0 with x3.
The subproof is completed by applying H3.
Claim L6: ordinal x2
Apply ordinal_Hered with x1 x3, x2 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H4.
Apply L6 with TransSet x2.
Assume H7: TransSet x2.
Assume H8: ∀ x4 . x4x2TransSet x4.
The subproof is completed by applying H7.