Let z be given.
Assume Hz.
Apply OSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx: HSNo x.
Assume Hy: HSNo y.
Assume Hzxy: z = HSNo_pair x y.
Let v be given.
Assume Hv: v ∈ ⋃ (HSNo_pair x y).
Apply UnionE_impred (HSNo_pair x y) v Hv to the current goal.
Let u be given.
Assume H1: v ∈ u.
Assume H2: u ∈ HSNo_pair x y.
Apply binunionE x {w ''|w ∈ y} u H2 to the current goal.
Assume H3: u ∈ x.
We prove the intermediate claim L1: v ∈ ⋃ x.
An exact proof term for the current goal is UnionI x v u H1 H3.
We will prove ordinal v ∨ ∃i ∈ 5, v = {i}.
An exact proof term for the current goal is extension_SNoElt_mon 4 5 (ordsuccI1 4) x (HSNo_ExtendedSNoElt_4 x Hx) v L1.
Assume H3: u ∈ {w ''|w ∈ y}.
Apply ReplE_impred y ctag u H3 to the current goal.
Let w be given.
Assume Hw: w ∈ y.
Assume H4: u = w ''.
We prove the intermediate claim L2: v ∈ w ''.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H1.
Apply binunionE w {{4}} v L2 to the current goal.
Assume H5: v ∈ w.
We prove the intermediate claim L3: v ∈ ⋃ y.
An exact proof term for the current goal is UnionI y v w H5 Hw.
An exact proof term for the current goal is extension_SNoElt_mon 4 5 (ordsuccI1 4) y (HSNo_ExtendedSNoElt_4 y Hy) v L3.
Assume H5: v ∈ {{4}}.
We will prove ordinal v ∨ ∃i ∈ 5, v = {i}.
Apply orIR to the current goal.
We use 4 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 4 ∈ 5.
An exact proof term for the current goal is In_4_5.
We will prove v = {4}.
An exact proof term for the current goal is SingE {4} v H5.
∎