Apply In_ind with
λ x0 . V_ (9d271.. x0) = V_ x0.
Let x0 of type ι be given.
Apply set_ext with
V_ (9d271.. x0),
V_ x0 leaving 2 subgoals.
Apply V_Subq_2 with
9d271.. x0,
x0.
The subproof is completed by applying Sep_Subq with
V_ x0,
ordinal.
Let x1 of type ι be given.
Apply V_E with
x1,
x0,
x1 ∈ V_ (9d271.. x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ x0.
Apply H0 with
x2,
λ x3 x4 . x1 ⊆ x3 ⟶ x1 ∈ V_ (9d271.. x0) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply V_I with
x1,
9d271.. x2,
9d271.. x0 leaving 2 subgoals.
Apply unknownprop_24ba76162cbabacbe8136cf5d6f6295437383ecf4b3946427a5b4b7d60ed1941 with
x2,
x0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.