Let f and N be given.
Assume Htot: total_function_on f ω ω.
Assume Hfg: functional_graph f.
Assume Hdom: graph_domain_subset f ω.
Assume Hinc: omega_strictly_increasing f.
Assume HNomega: N ∈ ω.
We prove the intermediate claim HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNomega).
We prove the intermediate claim HsuccN: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
We prove the intermediate claim HfFun: function_on f ω ω.
An exact proof term for the current goal is (total_function_on_function_on f ω ω Htot).
We prove the intermediate claim Hexbad: ∃i : set, i ∈ ordsucc N ∧ ¬ (apply_fun f i ∈ N).
We prove the intermediate claim Hex1: ∃i : set, ¬ (i ∈ ordsucc N → apply_fun f i ∈ N).
Apply (not_all_ex_demorgan_i (λi : set ⇒ i ∈ ordsucc N → apply_fun f i ∈ N)) to the current goal.
Assume Hall: ∀i : set, i ∈ ordsucc N → apply_fun f i ∈ N.
We prove the intermediate claim Hrange: ∀i ∈ ordsucc N, (apply_fun f i) ∈ N.
Let i be given.
Assume Hi: i ∈ ordsucc N.
An exact proof term for the current goal is (Hall i Hi).
We prove the intermediate claim Hinj: ∀i j ∈ ordsucc N, apply_fun f i = apply_fun f j → i = j.
Let i be given.
Assume Hi: i ∈ ordsucc N.
Let j be given.
Assume Hj: j ∈ ordsucc N.
Assume Heq: apply_fun f i = apply_fun f j.
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (omega_TransSet (ordsucc N) HsuccN i Hi).
We prove the intermediate claim HjO: j ∈ ω.
An exact proof term for the current goal is (omega_TransSet (ordsucc N) HsuccN j Hj).
We prove the intermediate claim Hord_i: ordinal i.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal i HiO).
We prove the intermediate claim Hord_j: ordinal j.
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal j HjO).
Apply (ordinal_trichotomy_or_impred i j Hord_i Hord_j (i = j)) to the current goal.
Assume Hij: i ∈ j.
We prove the intermediate claim HfiIn: apply_fun f i ∈ apply_fun f j.
An exact proof term for the current goal is (Hinc i j HiO HjO Hij).
We prove the intermediate claim Hneq: apply_fun f i ≠ apply_fun f j.
Assume Heq'.
We prove the intermediate claim Hsubst: ∀S T : set, S = T → apply_fun f i ∈ S → apply_fun f i ∈ T.
Let S and T be given.
Assume HeqST.
Assume Hmem.
rewrite the current goal using HeqST (from right to left).
An exact proof term for the current goal is Hmem.
We prove the intermediate claim Hsym: apply_fun f j = apply_fun f i.
rewrite the current goal using Heq' (from right to left).
Use reflexivity.
We prove the intermediate claim Hself: apply_fun f i ∈ apply_fun f i.
An exact proof term for the current goal is (Hsubst (apply_fun f j) (apply_fun f i) Hsym HfiIn).
An exact proof term for the current goal is (In_irref (apply_fun f i) Hself).
An exact proof term for the current goal is (FalseE (Hneq Heq) (i = j)).
Assume Hij: i = j.
An exact proof term for the current goal is Hij.
Assume Hji: j ∈ i.
We prove the intermediate claim HfjIn: apply_fun f j ∈ apply_fun f i.
An exact proof term for the current goal is (Hinc j i HjO HiO Hji).
We prove the intermediate claim Hneq: apply_fun f j ≠ apply_fun f i.
Assume Heq'.
We prove the intermediate claim Hsubst: ∀S T : set, S = T → apply_fun f j ∈ S → apply_fun f j ∈ T.
Let S and T be given.
Assume HeqST.
Assume Hmem.
rewrite the current goal using HeqST (from right to left).
An exact proof term for the current goal is Hmem.
We prove the intermediate claim Hsym: apply_fun f i = apply_fun f j.
rewrite the current goal using Heq' (from right to left).
Use reflexivity.
We prove the intermediate claim Hself: apply_fun f j ∈ apply_fun f j.
An exact proof term for the current goal is (Hsubst (apply_fun f i) (apply_fun f j) Hsym HfjIn).
An exact proof term for the current goal is (In_irref (apply_fun f j) Hself).
We prove the intermediate claim HsymHeq: apply_fun f j = apply_fun f i.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (FalseE (Hneq HsymHeq) (i = j)).
We prove the intermediate claim Hbad: ¬ (∀i j ∈ ordsucc N, (λt : set ⇒ apply_fun f t) i = (λt : set ⇒ apply_fun f t) j → i = j).
An exact proof term for the current goal is (PigeonHole_nat N HNnat (λt : set ⇒ apply_fun f t) Hrange).
We prove the intermediate claim Hgood: ∀i j ∈ ordsucc N, (λt : set ⇒ apply_fun f t) i = (λt : set ⇒ apply_fun f t) j → i = j.
Let i be given.
Assume Hi: i ∈ ordsucc N.
Let j be given.
Assume Hj: j ∈ ordsucc N.
An exact proof term for the current goal is (Hinj i Hi j Hj).
An exact proof term for the current goal is (Hbad Hgood).
Apply Hex1 to the current goal.
Let i be given.
Assume Hnimp.
We prove the intermediate claim Hipair: i ∈ ordsucc N ∧ ¬ (apply_fun f i ∈ N).
An exact proof term for the current goal is (not_imp (i ∈ ordsucc N) (apply_fun f i ∈ N) Hnimp).
We use i to witness the existential quantifier.
An exact proof term for the current goal is Hipair.
Apply Hexbad to the current goal.
Let k be given.
Assume Hkpair.
We prove the intermediate claim HkInSucc: k ∈ ordsucc N.
An exact proof term for the current goal is (andEL (k ∈ ordsucc N) (¬ (apply_fun f k ∈ N)) Hkpair).
We prove the intermediate claim HknotIn: ¬ (apply_fun f k ∈ N).
An exact proof term for the current goal is (andER (k ∈ ordsucc N) (¬ (apply_fun f k ∈ N)) Hkpair).
We prove the intermediate claim HkOmega: k ∈ ω.
An exact proof term for the current goal is (omega_TransSet (ordsucc N) HsuccN k HkInSucc).
We prove the intermediate claim HfkOmega: apply_fun f k ∈ ω.
An exact proof term for the current goal is (HfFun k HkOmega).
We prove the intermediate claim HfkOrd: ordinal (apply_fun f k).
An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal (apply_fun f k) HfkOmega).
Apply (ordinal_trichotomy_or_impred (apply_fun f k) N HfkOrd (ordinal_Hered ω omega_ordinal N HNomega) (∃k0 : set, k0 ∈ ω ∧ N ⊆ apply_fun f k0)) to the current goal.
Assume Hlt: apply_fun f k ∈ N.
An exact proof term for the current goal is (FalseE (HknotIn Hlt) (∃k0 : set, k0 ∈ ω ∧ N ⊆ apply_fun f k0)).
Assume Heq: apply_fun f k = N.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HkOmega.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Subq_ref N).
Assume Hgt: N ∈ apply_fun f k.
We use k to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HkOmega.
We prove the intermediate claim Htrans: TransSet (apply_fun f k).
An exact proof term for the current goal is (andEL (TransSet (apply_fun f k)) (∀beta ∈ apply_fun f k, TransSet beta) HfkOrd).
An exact proof term for the current goal is (Htrans N Hgt).
∎