Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply andI with TransSet (9d271.. x0), ∀ x1 . x1 ∈ 9d271.. x0 ⟶ TransSet x1 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0: x1 ∈ {x2 ∈ V_ x0|ordinal x2}.
Apply SepE with V_ x0, ordinal, x1, x1 ⊆ 9d271.. x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x1 ∈ V_ x0.
Assume H2: ordinal x1.
Let x2 of type ι be given.
Assume H3: x2 ∈ x1.
Apply SepI with V_ x0, λ x3 . ordinal x3, x2 leaving 2 subgoals.
Apply unknownprop_2db13168d0906b1c33dd9956e4244fb20fdb495d0c65d9833035772e7d401c89 with x0, x1, x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
Apply ordinal_Hered with x1, x2 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H0: x1 ∈ {x2 ∈ V_ x0|ordinal x2}.
Apply SepE with V_ x0, ordinal, x1, TransSet x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x1 ∈ V_ x0.
Assume H2: ordinal x1.
Apply H2 with TransSet x1.
Assume H3: TransSet x1.
Assume H4: ∀ x2 . x2 ∈ x1 ⟶ TransSet x2.
The subproof is completed by applying H3.
■