Apply andI to the current goal.

Let x be given.

Assume HxM: x ∈ m.

We prove the intermediate claim HxS: x ∈ ordsucc m.

An exact proof term for the current goal is (ordsuccI1 m x HxM).

We prove the intermediate claim HfunS: function_on e (ordsucc m) F.

An exact proof term for the current goal is (andEL (function_on e (ordsucc m) F) (∀y : set, y ∈ F → ∃x0 : set, x0 ∈ ordsucc m ∧ apply_fun e x0 = y ∧ (∀x' : set, x' ∈ ordsucc m → apply_fun e x' = y → x' = x0)) Hbij).

We prove the intermediate claim HxF: apply_fun e x ∈ F.

An exact proof term for the current goal is (HfunS x HxS).

We prove the intermediate claim Hxm: ¬ (x = m).

Assume Heq: x = m.

We prove the intermediate claim Hmm: m ∈ m.

rewrite the current goal using Heq (from right to left) at position 1.

An exact proof term for the current goal is HxM.

An exact proof term for the current goal is ((In_irref m) Hmm).

We prove the intermediate claim HnotSing: apply_fun e x ∉ {apply_fun e m}.

Assume Hsing: apply_fun e x ∈ {apply_fun e m}.

We prove the intermediate claim Heqem: apply_fun e x = apply_fun e m.

An exact proof term for the current goal is (SingE (apply_fun e m) (apply_fun e x) Hsing).

We prove the intermediate claim HmS: m ∈ ordsucc m.

An exact proof term for the current goal is (ordsuccI2 m).

We prove the intermediate claim Heqxm: x = m.

An exact proof term for the current goal is (bijection_inj (ordsucc m) F e x m Hbij HxS HmS Heqem).

An exact proof term for the current goal is (Hxm Heqxm).

An exact proof term for the current goal is (setminusI F {apply_fun e m} (apply_fun e x) HxF HnotSing).

Let y be given.

Assume Hy: y ∈ (F ∖ {apply_fun e m}).

We prove the intermediate claim HyPack: y ∈ F ∧ y ∉ {apply_fun e m}.

An exact proof term for the current goal is (setminusE F {apply_fun e m} y Hy).

We prove the intermediate claim HyF: y ∈ F.

An exact proof term for the current goal is (andEL (y ∈ F) (y ∉ {apply_fun e m}) HyPack).

We prove the intermediate claim HyNot: y ∉ {apply_fun e m}.

An exact proof term for the current goal is (andER (y ∈ F) (y ∉ {apply_fun e m}) HyPack).

We prove the intermediate claim HuniqAll: ∀y0 : set, y0 ∈ F → ∃x0 : set, x0 ∈ ordsucc m ∧ apply_fun e x0 = y0 ∧ (∀x' : set, x' ∈ ordsucc m → apply_fun e x' = y0 → x' = x0).

An exact proof term for the current goal is (andER (function_on e (ordsucc m) F) (∀y0 : set, y0 ∈ F → ∃x0 : set, x0 ∈ ordsucc m ∧ apply_fun e x0 = y0 ∧ (∀x' : set, x' ∈ ordsucc m → apply_fun e x' = y0 → x' = x0)) Hbij).

Apply (HuniqAll y HyF) to the current goal.

Let x0 be given.

Assume Hx0pack.

We prove the intermediate claim Hx0AB: x0 ∈ ordsucc m ∧ apply_fun e x0 = y.

An exact proof term for the current goal is (andEL (x0 ∈ ordsucc m ∧ apply_fun e x0 = y) (∀x' : set, x' ∈ ordsucc m → apply_fun e x' = y → x' = x0) Hx0pack).

We prove the intermediate claim Hx0S: x0 ∈ ordsucc m.

An exact proof term for the current goal is (andEL (x0 ∈ ordsucc m) (apply_fun e x0 = y) Hx0AB).

We prove the intermediate claim Heqx0: apply_fun e x0 = y.

An exact proof term for the current goal is (andER (x0 ∈ ordsucc m) (apply_fun e x0 = y) Hx0AB).

We prove the intermediate claim HuniqS: ∀x' : set, x' ∈ ordsucc m → apply_fun e x' = y → x' = x0.

An exact proof term for the current goal is (andER (x0 ∈ ordsucc m ∧ apply_fun e x0 = y) (∀x' : set, x' ∈ ordsucc m → apply_fun e x' = y → x' = x0) Hx0pack).

We prove the intermediate claim Hx0case: x0 ∈ m ∨ x0 = m.

An exact proof term for the current goal is (ordsuccE m x0 Hx0S).

We prove the intermediate claim Hx0M: x0 ∈ m.

Apply (Hx0case (x0 ∈ m)) to the current goal.

Assume H0: x0 ∈ m.

An exact proof term for the current goal is H0.

Assume H0: x0 = m.

Apply FalseE to the current goal.

We prove the intermediate claim HyEq: y = apply_fun e m.

rewrite the current goal using Heqx0 (from right to left).

rewrite the current goal using H0 (from left to right).

Use reflexivity.

We prove the intermediate claim HySing: y ∈ {apply_fun e m}.

rewrite the current goal using HyEq (from left to right).

An exact proof term for the current goal is (SingI (apply_fun e m)).

An exact proof term for the current goal is (HyNot HySing).

We use x0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0M.

An exact proof term for the current goal is Heqx0.

Let x' be given.

Assume Hx'M: x' ∈ m.

Assume Heq': apply_fun e x' = y.

We prove the intermediate claim Hx'S: x' ∈ ordsucc m.

An exact proof term for the current goal is (ordsuccI1 m x' Hx'M).

An exact proof term for the current goal is (HuniqS x' Hx'S Heq').