We prove the intermediate claim L1: ∀n, nat_p n → ∀X, (∀x ∈ X, SNo x) → equip X (ordsucc n) → ∃x, SNo_max_of X x.
Apply nat_ind to the current goal.
Let X be given.
Assume HX.
Assume H1: equip X 1.
Apply equip_sym X 1 H1 to the current goal.
Let f be given.
Assume Hf: bij 1 X f.
Apply bijE 1 X f Hf to the current goal.
Assume Hf1 Hf2 Hf3.
We use f 0 to witness the existential quantifier.
We will prove SNo_max_of X (f 0).
We will prove f 0 ∈ X ∧ SNo (f 0) ∧ ∀y ∈ X, SNo y → y ≤ f 0.
We prove the intermediate claim Lf0X: f 0 ∈ X.
An exact proof term for the current goal is Hf1 0 In_0_1.
Apply and3I to the current goal.
We will prove f 0 ∈ X.
An exact proof term for the current goal is Lf0X.
An exact proof term for the current goal is HX (f 0) Lf0X.
Let y be given.
Assume Hy: y ∈ X.
Assume Hy2: SNo y.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ 1.
Assume Hyi: f i = y.
We will prove y ≤ f 0.
rewrite the current goal using Hyi (from right to left).
Apply cases_1 i Hi to the current goal.
We will prove f 0 ≤ f 0.
Apply SNoLe_ref to the current goal.
Let n be given.
Assume Hn.
Assume IHn: ∀X, (∀x ∈ X, SNo x) → equip X (ordsucc n) → ∃x, SNo_max_of X x.
Let X be given.
Assume HX.
Assume H1: equip X (ordsucc (ordsucc n)).
Apply equip_sym X (ordsucc (ordsucc n)) H1 to the current goal.
Let f be given.
Assume Hf: bij (ordsucc (ordsucc n)) X f.
Apply bijE (ordsucc (ordsucc n)) X f Hf to the current goal.
Assume Hf1 Hf2 Hf3.
Set X' to be the term {f i|i ∈ ordsucc n}.
We prove the intermediate claim LX'1: X' ⊆ X.
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred (ordsucc n) f w Hw to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Assume Hwi: w = f i.
rewrite the current goal using Hwi (from left to right).
We will prove f i ∈ X.
Apply Hf1 i to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We prove the intermediate claim LX'2: equip X' (ordsucc n).
Apply equip_sym to the current goal.
We will prove ∃f : set → set, bij (ordsucc n) X' f.
We use f to witness the existential quantifier.
Apply bijI to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hi.
Let i be given.
Assume Hi.
Let j be given.
Assume Hj.
Assume Hij: f i = f j.
Apply Hf2 to the current goal.
We will prove i ∈ ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hi.
We will prove j ∈ ordsucc (ordsucc n).
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Hj.
An exact proof term for the current goal is Hij.
Let w be given.
Assume Hw: w ∈ X'.
Apply ReplE_impred (ordsucc n) f w Hw to the current goal.
Let i be given.
Assume Hi: i ∈ ordsucc n.
Assume Hwi: w = f i.
We use i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hi.
Use symmetry.
An exact proof term for the current goal is Hwi.
Apply IHn X' (λx' Hx' ⇒ HX x' (LX'1 x' Hx')) LX'2 to the current goal.
Let z be given.
Assume H.
Apply H to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: z ∈ X'.
Assume Hz2: SNo z.
Assume Hz3: ∀y ∈ X', SNo y → y ≤ z.
We prove the intermediate claim Lfn1: f (ordsucc n) ∈ X.
Apply Hf1 (ordsucc n) to the current goal.
Apply ordsuccI2 to the current goal.
We prove the intermediate claim Lfn1': SNo (f (ordsucc n)).
Apply HX (f (ordsucc n)) Lfn1 to the current goal.
Apply SNoLtLe_or z (f (ordsucc n)) Hz2 Lfn1' to the current goal.
Assume H2: z < f (ordsucc n).
We use (f (ordsucc n)) to witness the existential quantifier.
We will prove f (ordsucc n) ∈ X ∧ SNo (f (ordsucc n)) ∧ ∀y ∈ X, SNo y → y ≤ f (ordsucc n).
Apply and3I to the current goal.
An exact proof term for the current goal is Lfn1.
An exact proof term for the current goal is Lfn1'.
Let y be given.
Assume Hy Hy2.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ ordsucc (ordsucc n).
Assume Hyi: f i = y.
Apply ordsuccE (ordsucc n) i Hi to the current goal.
Assume H3: i ∈ ordsucc n.
We will prove y ≤ f (ordsucc n).
Apply SNoLe_tra y z (f (ordsucc n)) Hy2 Hz2 Lfn1' to the current goal.
We will prove y ≤ z.
Apply Hz3 y to the current goal.
We will prove y ∈ X'.
rewrite the current goal using Hyi (from right to left).
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Hy2.
We will prove z ≤ f (ordsucc n).
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is H2.
Assume H3: i = ordsucc n.
rewrite the current goal using Hyi (from right to left).
rewrite the current goal using H3 (from left to right).
We will prove f (ordsucc n) ≤ f (ordsucc n).
Apply SNoLe_ref to the current goal.
Assume H2: f (ordsucc n) ≤ z.
We use z to witness the existential quantifier.
We will prove z ∈ X ∧ SNo z ∧ ∀y ∈ X, SNo y → y ≤ z.
Apply and3I to the current goal.
An exact proof term for the current goal is LX'1 z Hz1.
An exact proof term for the current goal is Hz2.
Let y be given.
Assume Hy Hy2.
Apply Hf3 y Hy to the current goal.
Let i be given.
Assume H.
Apply H to the current goal.
Assume Hi: i ∈ ordsucc (ordsucc n).
Assume Hyi: f i = y.
Apply ordsuccE (ordsucc n) i Hi to the current goal.
Assume H3: i ∈ ordsucc n.
We will prove y ≤ z.
Apply Hz3 y to the current goal.
We will prove y ∈ X'.
rewrite the current goal using Hyi (from right to left).
We will prove f i ∈ X'.
Apply ReplI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Hy2.
Assume H3: i = ordsucc n.
rewrite the current goal using Hyi (from right to left).
rewrite the current goal using H3 (from left to right).
We will prove f (ordsucc n) ≤ z.
An exact proof term for the current goal is H2.
Let X be given.
Assume HX.
Assume H1: finite X.
Apply H1 to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: n ∈ ω.
Apply nat_inv n (omega_nat_p n Hn) to the current goal.
Assume Hn0: n = 0.
rewrite the current goal using Hn0 (from left to right).
Assume H2: equip X 0.
Assume H3: X ≠ 0.
We will prove False.
Apply H2 to the current goal.
Let f be given.
Assume Hf: bij X 0 f.
Apply bijE X 0 f Hf to the current goal.
Assume Hf1 _ _.
Apply H3 to the current goal.
Apply Empty_eq to the current goal.
Let x be given.
Assume Hx.
Apply EmptyE (f x) to the current goal.
An exact proof term for the current goal is Hf1 x Hx.
Assume H.
Apply H to the current goal.
Let m be given.
Assume H.
Apply H to the current goal.
Assume Hm: nat_p m.
Assume Hnm: n = ordsucc m.
rewrite the current goal using Hnm (from left to right).
Assume H2: equip X (ordsucc m).
Assume _.
An exact proof term for the current goal is L1 m Hm X HX H2.
∎