Let x0 of type ι be given.
Assume H0:
∀ x1 . x1 ∈ x0 ⟶ ordinal x1.
Apply andI with
TransSet (prim3 x0),
∀ x1 . x1 ∈ prim3 x0 ⟶ TransSet x1 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1:
x1 ∈ prim3 x0.
Apply UnionE_impred with
x0,
x1,
x1 ⊆ prim3 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x1 ∈ x2.
Assume H3: x2 ∈ x0.
Apply H0 with
x2.
The subproof is completed by applying H3.
Apply L4 with
x1 ⊆ prim3 x0.
Assume H6:
∀ x3 . x3 ∈ x2 ⟶ TransSet x3.
Let x3 of type ι be given.
Assume H7: x3 ∈ x1.
Claim L8: x3 ∈ x2
Apply H5 with
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H7.
Apply UnionI with
x0,
x3,
x2 leaving 2 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H1:
x1 ∈ prim3 x0.
Apply UnionE_impred with
x0,
x1,
TransSet x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x1 ∈ x2.
Assume H3: x2 ∈ x0.
Apply H0 with
x2.
The subproof is completed by applying H3.
Apply ordinal_Hered with
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
Apply L5 with
TransSet x1.
Assume H7:
∀ x3 . x3 ∈ x1 ⟶ TransSet x3.
The subproof is completed by applying H6.