Let x0 of type ι be given.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Apply nat_p_ordinal with
x0.
The subproof is completed by applying L1.
Apply set_ext with
SNoS_ x0,
famunion x0 (λ x1 . {x2 ∈ SNoS_ omega|SNoLev x2 = x1}),
λ x1 x2 . finite x2 leaving 3 subgoals.
Let x1 of type ι be given.
Assume H3:
x1 ∈ SNoS_ x0.
Apply SNoS_E2 with
x0,
x1,
x1 ∈ famunion x0 (λ x2 . {x3 ∈ SNoS_ omega|SNoLev x3 = x2}) leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H3.
Apply famunionI with
x0,
λ x2 . {x3 ∈ SNoS_ omega|SNoLev x3 = x2},
SNoLev x1,
x1 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply SepI with
SNoS_ omega,
λ x2 . SNoLev x2 = SNoLev x1,
x1 leaving 2 subgoals.
Apply SNoS_Subq with
x0,
omega,
x1 leaving 4 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying omega_ordinal.
Apply omega_TransSet with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Let x3 of type ι → ι → ο be given.
Assume H8: x3 y2 y2.
The subproof is completed by applying H8.
Let x1 of type ι be given.
Apply famunionE_impred with
x0,
λ x2 . {x3 ∈ SNoS_ omega|SNoLev x3 = x2},
x1,
x1 ∈ SNoS_ x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Apply SepE with
SNoS_ omega,
λ x3 . SNoLev x3 = x2,
x1,
x1 ∈ SNoS_ x0 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply SNoS_E2 with
omega,
x1,
x1 ∈ SNoS_ x0 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H6.
Apply SNoS_I with
x0,
x1,
SNoLev x1 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply H7 with
λ x3 x4 . x4 ∈ x0.
The subproof is completed by applying H4.
Apply famunion_nat_finite with
λ x1 . {x2 ∈ SNoS_ omega|SNoLev x2 = x1},
x0 leaving 2 subgoals.
The subproof is completed by applying L1.
Let x1 of type ι be given.
Assume H3: x1 ∈ x0.
Let x2 of type ο be given.
Apply H4 with
exp_SNo_nat 2 x1.
Apply andI with
exp_SNo_nat 2 x1 ∈ omega,
equip {x3 ∈ SNoS_ omega|SNoLev x3 = x1} (exp_SNo_nat 2 x1) leaving 2 subgoals.
Apply nat_p_omega with
exp_SNo_nat 2 x1.
Apply nat_exp_SNo_nat with
2,
x1 leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply nat_p_trans with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H3.
Apply SNoS_omega_Lev_equip with
x1.
Apply nat_p_trans with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H3.