Let N, X and y be given.
Assume H1: y ∉ X.
Assume H2: equip N X.
Apply H2 to the current goal.
Let f be given.
Assume Hf: bij N X f.
Apply bijE N X f Hf to the current goal.
Assume Hf1: ∀u ∈ N, f u ∈ X.
Assume Hf2: ∀u v ∈ N, f u = f v → u = v.
Assume Hf3: ∀w ∈ X, ∃u ∈ N, f u = w.
We prove the intermediate claim L1: ∃g : set → set, (∀u ∈ N, g u = f u) ∧ g N = y.
Set g to be the term λu ⇒ if u ∈ N then f u else y of type set → set.
We use g to witness the existential quantifier.
Apply andI to the current goal.
Let u be given.
Assume Hu: u ∈ N.
We will prove g u = f u.
An exact proof term for the current goal is If_i_1 (u ∈ N) (f u) y Hu.
We will prove g N = y.
An exact proof term for the current goal is If_i_0 (N ∈ N) (f N) y (In_irref N).
Apply L1 to the current goal.
Let g be given.
Assume H.
Apply H to the current goal.
Assume Hg1: ∀u ∈ N, g u = f u.
Assume Hg2: g N = y.
We will prove ∃g : set → set, bij (ordsucc N) (X ∪ {y}) g.
We use g to witness the existential quantifier.
Apply bijI to the current goal.
Let u be given.
Assume Hu: u ∈ ordsucc N.
Apply ordsuccE N u Hu to the current goal.
Assume H3: u ∈ N.
We will prove g u ∈ X ∪ {y}.
Apply binunionI1 to the current goal.
rewrite the current goal using Hg1 u H3 (from left to right).
We will prove f u ∈ X.
An exact proof term for the current goal is Hf1 u H3.
Assume H3: u = N.
We will prove g u ∈ X ∪ {y}.
Apply binunionI2 to the current goal.
We will prove g u ∈ {y}.
rewrite the current goal using H3 (from left to right).
rewrite the current goal using Hg2 (from left to right).
We will prove y ∈ {y}.
Apply SingI to the current goal.
Let u be given.
Assume Hu: u ∈ ordsucc N.
Let v be given.
Assume Hv: v ∈ ordsucc N.
We will prove g u = g v → u = v.
Apply ordsuccE N u Hu to the current goal.
Assume H3: u ∈ N.
rewrite the current goal using Hg1 u H3 (from left to right).
Apply ordsuccE N v Hv to the current goal.
Assume H4: v ∈ N.
rewrite the current goal using Hg1 v H4 (from left to right).
We will prove f u = f v → u = v.
An exact proof term for the current goal is Hf2 u H3 v H4.
Assume H4: v = N.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Assume H5: f u = y.
We will prove False.
Apply H1 to the current goal.
We will prove y ∈ X.
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is Hf1 u H3.
Assume H3: u = N.
Apply ordsuccE N v Hv to the current goal.
Assume H4: v ∈ N.
rewrite the current goal using H3 (from left to right).
rewrite the current goal using Hg2 (from left to right).
rewrite the current goal using Hg1 v H4 (from left to right).
Assume H5: y = f v.
We will prove False.
Apply H1 to the current goal.
We will prove y ∈ X.
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is Hf1 v H4.
Assume H4: v = N.
Assume _.
We will prove u = v.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw: w ∈ X ∪ {y}.
We will prove ∃u ∈ ordsucc N, g u = w.
Apply binunionE X {y} w Hw to the current goal.
Assume H3: w ∈ X.
Apply Hf3 w H3 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume H4: u ∈ N.
Assume H5: f u = w.
We use u to witness the existential quantifier.
Apply andI to the current goal.
We will prove u ∈ ordsucc N.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H4.
We will prove g u = w.
rewrite the current goal using Hg1 u H4 (from left to right).
An exact proof term for the current goal is H5.
Assume H3: w ∈ {y}.
We use N to witness the existential quantifier.
Apply andI to the current goal.
We will prove N ∈ ordsucc N.
Apply ordsuccI2 to the current goal.
We will prove g N = w.
rewrite the current goal using SingE y w H3 (from left to right).
An exact proof term for the current goal is Hg2.
∎