Let X and y be given.
Assume H1.
Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Assume H2: equip X n.
Apply equip_sym X n 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: ∀i ∈ n, f i ∈ X.
Assume Hf2: ∀i j ∈ n, f i = f j → i = j.
Assume Hf3: ∀x ∈ X, ∃i ∈ n, f i = x.
Apply xm (y ∈ X) to the current goal.
Assume H3: y ∈ X.
We prove the intermediate claim L1: X ∪ {y} = X.
Apply set_ext to the current goal.
Let x be given.
Assume Hx.
Apply binunionE X {y} x Hx to the current goal.
Assume H4.
An exact proof term for the current goal is H4.
Assume H4: x ∈ {y}.
rewrite the current goal using SingE y x H4 (from left to right).
An exact proof term for the current goal is H3.
Apply binunion_Subq_1 to the current goal.
rewrite the current goal using L1 (from left to right).
An exact proof term for the current goal is H1.
Assume H3: y ∉ X.
We will prove ∃m ∈ ω, equip (X ∪ {y}) m.
We use ordsucc n to witness the existential quantifier.
Apply andI to the current goal.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is Hn.
We will prove equip (X ∪ {y}) (ordsucc n).
Apply equip_sym to the current goal.
We will prove ∃g : set → set, bij (ordsucc n) (X ∪ {y}) g.
We prove the intermediate claim Lg: ∃g : set → set, (∀i ∈ n, g i = f i) ∧ g n = y.
We use (λi : set ⇒ if i ∈ n then f i else y) to witness the existential quantifier.
Apply andI to the current goal.
Let i be given.
Assume Hi.
An exact proof term for the current goal is If_i_1 (i ∈ n) (f i) y Hi.
An exact proof term for the current goal is If_i_0 (n ∈ n) (f n) y (In_irref n).
Apply Lg to the current goal.
Let g be given.
Assume H.
Apply H to the current goal.
Assume Hg1 Hg2.
We use g to witness the existential quantifier.
Apply bijI to the current goal.
We will prove ∀i ∈ ordsucc n, g i ∈ X ∪ {y}.
Let i be given.
Assume Hi.
Apply ordsuccE n i Hi to the current goal.
Assume H4: i ∈ n.
Apply binunionI1 to the current goal.
rewrite the current goal using Hg1 i H4 (from left to right).
We will prove f i ∈ X.
An exact proof term for the current goal is Hf1 i H4.
Assume H4: i = n.
Apply binunionI2 to the current goal.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Apply SingI to the current goal.
We will prove ∀i j ∈ ordsucc n, g i = g j → i = j.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
Apply ordsuccE n i Hi to the current goal.
Assume H4: i ∈ n.
rewrite the current goal using Hg1 i H4 (from left to right).
Apply ordsuccE n j Hj to the current goal.
Assume H5: j ∈ n.
rewrite the current goal using Hg1 j H5 (from left to right).
An exact proof term for the current goal is Hf2 i H4 j H5.
Assume H5: j = n.
rewrite the current goal using H5 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Assume H6: f i = y.
We will prove False.
Apply H3 to the current goal.
We will prove y ∈ X.
rewrite the current goal using H6 (from right to left).
An exact proof term for the current goal is Hf1 i H4.
Assume H4: i = n.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Apply ordsuccE n j Hj to the current goal.
Assume H5: j ∈ n.
rewrite the current goal using Hg1 j H5 (from left to right).
Assume H6: y = f j.
We will prove False.
Apply H3 to the current goal.
We will prove y ∈ X.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Hf1 j H5.
Assume H5: j = n.
rewrite the current goal using H5 (from left to right).
Assume _.
We will prove n = n.
Use reflexivity.
We will prove ∀x ∈ X ∪ {y}, ∃i ∈ ordsucc n, g i = x.
Let x be given.
Assume Hx.
Apply binunionE X {y} x Hx to the current goal.
Assume H4: x ∈ X.
Apply Hf3 x H4 to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ n.
Assume H5: f i = x.
We use i to witness the existential quantifier.
Apply andI to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We will prove g i = x.
rewrite the current goal using Hg1 i Hi (from left to right).
An exact proof term for the current goal is H5.
Assume H4: x ∈ {y}.
We use n to witness the existential quantifier.
Apply andI to the current goal.
Apply ordsuccI2 to the current goal.
We will prove g n = x.
rewrite the current goal using SingE y x H4 (from left to right).
An exact proof term for the current goal is Hg2.
∎