Let X, N and x be given.
Assume Hx: x ∈ X.
Assume H1: equip X (ordsucc N).
Apply equip_sym X (ordsucc N) H1 to the current goal.
Let f be given.
Assume Hf: bij (ordsucc N) X f.
Apply bijE (ordsucc N) X f Hf to the current goal.
Assume Hf1: ∀u ∈ ordsucc N, f u ∈ X.
Assume Hf2: ∀u v ∈ ordsucc N, f u = f v → u = v.
Assume Hf3: ∀y ∈ X, ∃u ∈ ordsucc N, f u = y.
Apply equip_sym to the current goal.
We will prove equip N (X ∖ {x}).
Apply Hf3 x Hx to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ ordsucc N.
Assume Hfw: f w = x.
Apply ordsuccE N w Hw to the current goal.
Assume H2: w ∈ N.
We prove the intermediate claim L1: f N ≠ x.
Assume H3: f N = x.
We prove the intermediate claim L1a: f w = f N.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is Hfw.
Apply In_irref N to the current goal.
We will prove N ∈ N.
rewrite the current goal using Hf2 w (ordsuccI1 N w H2) N (ordsuccI2 N) L1a (from right to left) at position 1.
We will prove w ∈ N.
An exact proof term for the current goal is H2.
We prove the intermediate claim L2: ∀u ∈ N, f u ≠ f N.
Let u be given.
Assume Hu: u ∈ N.
Assume H3: f u = f N.
Apply In_irref N to the current goal.
We will prove N ∈ N.
rewrite the current goal using Hf2 u (ordsuccI1 N u Hu) N (ordsuccI2 N) H3 (from right to left) at position 1.
We will prove u ∈ N.
An exact proof term for the current goal is Hu.
We prove the intermediate claim L3: ∃g : set → set, (∀u ∈ ordsucc N, u ≠ w → g u = f u) ∧ g w = f N.
Set g to be the term λu ⇒ if u = w then f N else f u 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 ∈ ordsucc N.
Assume H3: u ≠ w.
An exact proof term for the current goal is If_i_0 (u = w) (f N) (f u) H3.
We will prove (if w = w then f N else f w) = f N.
An exact proof term for the current goal is If_i_1 (w = w) (f N) (f w) (λq H ⇒ H).
Apply L3 to the current goal.
Let g be given.
Assume H.
Apply H to the current goal.
Assume Hg1: ∀u ∈ ordsucc N, u ≠ w → g u = f u.
Assume Hg2: g w = f N.
We will prove ∃g : set → set, bij N (X ∖ {x}) g.
We use g to witness the existential quantifier.
Apply bijI to the current goal.
Let u be given.
Assume Hu: u ∈ N.
We will prove g u ∈ X ∖ {x}.
Apply xm (u = w) to the current goal.
Assume H3: u = w.
rewrite the current goal using H3 (from left to right).
rewrite the current goal using Hg2 (from left to right).
We will prove f N ∈ X ∖ {x}.
Apply setminusI to the current goal.
We will prove f N ∈ X.
An exact proof term for the current goal is Hf1 N (ordsuccI2 N).
Assume H4: f N ∈ {x}.
Apply L1 to the current goal.
We will prove f N = x.
Apply SingE to the current goal.
An exact proof term for the current goal is H4.
Assume H3: u ≠ w.
rewrite the current goal using Hg1 u (ordsuccI1 N u Hu) H3 (from left to right).
We will prove f u ∈ X ∖ {x}.
Apply setminusI to the current goal.
We will prove f u ∈ X.
An exact proof term for the current goal is Hf1 u (ordsuccI1 N u Hu).
Assume H4: f u ∈ {x}.
Apply H3 to the current goal.
We will prove u = w.
Apply Hf2 u (ordsuccI1 N u Hu) w Hw to the current goal.
We will prove f u = f w.
rewrite the current goal using Hfw (from left to right).
We will prove f u = x.
Apply SingE to the current goal.
An exact proof term for the current goal is H4.
Let u be given.
Assume Hu: u ∈ N.
Let v be given.
Assume Hv: v ∈ N.
We will prove g u = g v → u = v.
Apply xm (u = w) to the current goal.
Assume H3: u = w.
Apply xm (v = w) to the current goal.
Assume H4: v = w.
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.
Assume H4: v ≠ w.
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 (ordsuccI1 N v Hv) H4 (from left to right).
Assume H5: f N = f v.
We will prove False.
Apply L2 v Hv to the current goal.
We will prove f v = f N.
Use symmetry.
An exact proof term for the current goal is H5.
Assume H3: u ≠ w.
rewrite the current goal using Hg1 u (ordsuccI1 N u Hu) H3 (from left to right).
Apply xm (v = w) to the current goal.
Assume H4: v = w.
rewrite the current goal using H4 (from left to right).
rewrite the current goal using Hg2 (from left to right).
Assume H5: f u = f N.
We will prove False.
Apply L2 u Hu to the current goal.
We will prove f u = f N.
An exact proof term for the current goal is H5.
Assume H4: v ≠ w.
rewrite the current goal using Hg1 v (ordsuccI1 N v Hv) 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 (ordsuccI1 N u Hu) v (ordsuccI1 N v Hv).
Let y be given.
Assume Hy: y ∈ X ∖ {x}.
Apply setminusE X {x} y Hy to the current goal.
Assume Hy1: y ∈ X.
Assume Hy2: y ∉ {x}.
Apply Hf3 y Hy1 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu1: u ∈ ordsucc N.
Assume Hu2: f u = y.
We prove the intermediate claim L4: u ≠ w.
Assume H3: u = w.
Apply Hy2 to the current goal.
We will prove y ∈ {x}.
rewrite the current goal using Hu2 (from right to left).
rewrite the current goal using Hfw (from right to left).
rewrite the current goal using H3 (from left to right).
Apply SingI to the current goal.
Apply ordsuccE N u Hu1 to the current goal.
Assume H3: u ∈ N.
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
We will prove g u = y.
rewrite the current goal using Hg1 u Hu1 L4 (from left to right).
We will prove f u = y.
An exact proof term for the current goal is Hu2.
Assume H3: u = N.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
We will prove g w = y.
rewrite the current goal using Hg2 (from left to right).
We will prove f N = y.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is Hu2.
Assume H2: w = N.
We will prove ∃g : set → set, bij N (X ∖ {x}) g.
We use f to witness the existential quantifier.
Apply bijI to the current goal.
Let u be given.
Assume Hu: u ∈ N.
We will prove f u ∈ X ∖ {x}.
Apply setminusI to the current goal.
An exact proof term for the current goal is Hf1 u (ordsuccI1 N u Hu).
Assume H3: f u ∈ {x}.
We prove the intermediate claim L5: u = N.
Apply Hf2 u (ordsuccI1 N u Hu) N (ordsuccI2 N) to the current goal.
We will prove f u = f N.
rewrite the current goal using H2 (from right to left).
rewrite the current goal using Hfw (from left to right).
We will prove f u = x.
Apply SingE to the current goal.
An exact proof term for the current goal is H3.
Apply In_irref N to the current goal.
We will prove N ∈ N.
rewrite the current goal using L5 (from right to left) at position 1.
We will prove u ∈ N.
An exact proof term for the current goal is Hu.
Let u be given.
Assume Hu: u ∈ N.
Let v be given.
Assume Hv: v ∈ N.
We will prove f u = f v → u = v.
An exact proof term for the current goal is Hf2 u (ordsuccI1 N u Hu) v (ordsuccI1 N v Hv).
Let y be given.
Assume Hy: y ∈ X ∖ {x}.
Apply setminusE X {x} y Hy to the current goal.
Assume Hy1: y ∈ X.
Assume Hy2: y ∉ {x}.
Apply Hf3 y Hy1 to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu1: u ∈ ordsucc N.
Assume Hu2: f u = y.
We use u to witness the existential quantifier.
Apply andI to the current goal.
We will prove u ∈ N.
Apply ordsuccE N u Hu1 to the current goal.
Assume H3: u ∈ N.
An exact proof term for the current goal is H3.
Assume H3: u = N.
We will prove False.
Apply Hy2 to the current goal.
We will prove y ∈ {x}.
rewrite the current goal using Hu2 (from right to left).
rewrite the current goal using H3 (from left to right).
rewrite the current goal using H2 (from right to left).
We will prove f w ∈ {x}.
rewrite the current goal using Hfw (from left to right).
Apply SingI to the current goal.
We will prove f u = y.
An exact proof term for the current goal is Hu2.
∎