Let X, f, g and f' be given.
Assume HX: infinite X.
Assume Hf1: ∀Z ⊆ X, infinite Z → f Z ⊆ Z ∧ infinite (f Z).
Assume Hg1: ∀Z ⊆ X, infinite Z → g Z ∈ Z ∧ g Z ∉ f Z.
Assume Hf'0: f' 0 = f X.
Assume Hf'S: ∀m, nat_p m → f' (ordsucc m) = f (f' m).
We prove the intermediate claim Lf'1: ∀m, nat_p m → f' m ⊆ X ∧ infinite (f' m).
Apply nat_ind to the current goal.
rewrite the current goal using Hf'0 (from left to right).
We will prove f X ⊆ X ∧ infinite (f X).
An exact proof term for the current goal is Hf1 X (λu H ⇒ H) HX.
Let m be given.
Assume Hm.
Assume IHm.
Apply IHm to the current goal.
Assume IHm1: f' m ⊆ X.
Assume IHm2: infinite (f' m).
We will prove f' (ordsucc m) ⊆ X ∧ infinite (f' (ordsucc m)).
rewrite the current goal using Hf'S m Hm (from left to right).
We will prove f (f' m) ⊆ X ∧ infinite (f (f' m)).
Apply Hf1 (f' m) IHm1 IHm2 to the current goal.
Assume H3: f (f' m) ⊆ f' m.
Assume H4: infinite (f (f' m)).
Apply andI to the current goal.
Apply Subq_tra (f (f' m)) (f' m) X H3 to the current goal.
An exact proof term for the current goal is IHm1.
An exact proof term for the current goal is H4.
We prove the intermediate claim Lgf'mm'addSubq: ∀m ∈ ω, ∀m', nat_p m' → f' (m + m') ⊆ f' m.
Let m be given.
Assume Hm.
Apply nat_ind to the current goal.
We will prove f' (m + 0) ⊆ f' m.
rewrite the current goal using add_nat_0R m (from left to right).
An exact proof term for the current goal is Subq_ref (f' m).
Let m' be given.
Assume Hm'.
Assume IHm': f' (m + m') ⊆ f' m.
We will prove f' (m + ordsucc m') ⊆ f' m.
rewrite the current goal using add_nat_SR m m' Hm' (from left to right).
We will prove f' (ordsucc (m + m')) ⊆ f' m.
rewrite the current goal using Hf'S (m + m') (add_nat_p m (omega_nat_p m Hm) m' Hm') (from left to right).
We will prove f (f' (m + m')) ⊆ f' m.
Apply Subq_tra (f (f' (m + m'))) (f' (m + m')) (f' m) to the current goal.
Apply Lf'1 (m + m') (add_nat_p m (omega_nat_p m Hm) m' Hm') to the current goal.
Assume Hfmm'X: f' (m + m') ⊆ X.
Assume Hfmm'inf: infinite (f' (m + m')).
Apply Hf1 (f' (m + m')) Hfmm'X Hfmm'inf to the current goal.
Assume H3: f (f' (m + m')) ⊆ f' (m + m').
Assume _.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is IHm'.
We prove the intermediate claim Lgf'mm'Subq: ∀m m' ∈ ω, m ⊆ m' → f' m' ⊆ f' m.
Let m be given.
Assume Hm: m ∈ ω.
Let m' be given.
Assume Hm': m' ∈ ω.
Assume Hmm': m ⊆ m'.
Apply nat_Subq_add_ex m (omega_nat_p m Hm) m' (omega_nat_p m' Hm') Hmm' to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: nat_p k.
Assume Hm'km: m' = k + m.
We will prove f' m' ⊆ f' m.
rewrite the current goal using Hm'km (from left to right).
We will prove f' (k + m) ⊆ f' m.
rewrite the current goal using add_nat_com k Hk m (omega_nat_p m Hm) (from left to right).
We will prove f' (m + k) ⊆ f' m.
An exact proof term for the current goal is Lgf'mm'addSubq m Hm k Hk.
We prove the intermediate claim Lgf'injlem: ∀m ∈ ω, ∀m' ∈ m, g (f' m') ≠ g (f' m).
Let m be given.
Assume Hm: m ∈ ω.
Let m' be given.
Assume Hm': m' ∈ m.
Assume H3: g (f' m') = g (f' m).
We prove the intermediate claim LmN: nat_p m.
Apply omega_nat_p to the current goal.
An exact proof term for the current goal is Hm.
We prove the intermediate claim Lmo: ordinal m.
Apply nat_p_ordinal to the current goal.
An exact proof term for the current goal is LmN.
We prove the intermediate claim Lm'N: nat_p m'.
An exact proof term for the current goal is nat_p_trans m (omega_nat_p m Hm) m' Hm'.
We prove the intermediate claim Lf'mff'm': f' m ⊆ f (f' m').
Apply Hf'S m' Lm'N (λu _ ⇒ f' m ⊆ u) to the current goal.
We will prove f' m ⊆ f' (ordsucc m').
Apply Lgf'mm'Subq (ordsucc m') (omega_ordsucc m' (nat_p_omega m' Lm'N)) m Hm to the current goal.
We will prove ordsucc m' ⊆ m.
An exact proof term for the current goal is ordinal_ordsucc_In_Subq m Lmo m' Hm'.
Apply Lf'1 m (omega_nat_p m Hm) to the current goal.
Assume H4: f' m ⊆ X.
Assume H5: infinite (f' m).
Apply Hg1 (f' m) H4 H5 to the current goal.
Assume H6: g (f' m) ∈ f' m.
Assume _.
Apply Lf'1 m' Lm'N to the current goal.
Assume H7: f' m' ⊆ X.
Assume H8: infinite (f' m').
Apply Hg1 (f' m') H7 H8 to the current goal.
Assume _.
Assume H9: g (f' m') ∉ f (f' m').
Apply H9 to the current goal.
We will prove g (f' m') ∈ f (f' m').
rewrite the current goal using H3 (from left to right).
We will prove g (f' m) ∈ f (f' m').
An exact proof term for the current goal is Lf'mff'm' (g (f' m)) H6.
Apply and3I to the current goal.
An exact proof term for the current goal is Lf'1.
An exact proof term for the current goal is Lgf'mm'Subq.
Let m be given.
Assume Hm: m ∈ ω.
Let m' be given.
Assume Hm': m' ∈ ω.
Assume Hgf'mm': g (f' m) = g (f' m').
Apply ordinal_trichotomy_or_impred m m' (nat_p_ordinal m (omega_nat_p m Hm)) (nat_p_ordinal m' (omega_nat_p m' Hm')) to the current goal.
Assume Hmm': m ∈ m'.
We will prove False.
Apply Lgf'injlem m' Hm' m Hmm' to the current goal.
We will prove g (f' m) = g (f' m').
An exact proof term for the current goal is Hgf'mm'.
Assume Hmm': m = m'.
An exact proof term for the current goal is Hmm'.
Assume Hm'm: m' ∈ m.
We will prove False.
Apply Lgf'injlem m Hm m' Hm'm to the current goal.
We will prove g (f' m') = g (f' m).
Use symmetry.
An exact proof term for the current goal is Hgf'mm'.
∎