Search for blocks/addresses/...

Proofgold Proof

pf
Apply In_ind with λ x0 . ∀ x1 . x0 ⊆ V_ x1 ⟶ V_ x0 ⊆ V_ x1.
Let x0 of type ι be given.
Assume H0: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x1 ⊆ V_ x2 ⟶ V_ x1 ⊆ V_ x2.
Let x1 of type ι be given.
Assume H1: x0 ⊆ V_ x1.
Let x2 of type ι be given.
Assume H2: x2 ∈ V_ x0.
Apply V_E with x2, x0, x2 ∈ V_ x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H3: x3 ∈ x0.
Assume H4: x2 ⊆ V_ x3.
Claim L5: x3 ∈ V_ x1
Apply H1 with x3.
The subproof is completed by applying H3.
Apply V_E with x3, x1, x2 ∈ V_ x1 leaving 2 subgoals.
The subproof is completed by applying L5.
Let x4 of type ι be given.
Assume H6: x4 ∈ x1.
Assume H7: x3 ⊆ V_ x4.
Claim L8: V_ x3 ⊆ V_ x4
Apply H0 with x3, x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H7.
Claim L9: x2 ⊆ V_ x4
Apply Subq_tra with x2, V_ x3, V_ x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying L8.
Apply V_I with x2, x4, x1 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L9.
■