Let Xi, Ti, i and k be given.
Assume Hchain: coherent_chain Xi Ti.
Assume HiO: i ∈ ω.
Assume HkO: k ∈ ω.
Set A0 to be the term (∀j : set, j ∈ ω → topology_on (apply_fun Xi j) (apply_fun Ti j)).
Set B0 to be the term (∀j : set, j ∈ ω → apply_fun Xi j ⊆ apply_fun Xi (ordsucc j)).
Set C0 to be the term (∀j : set, j ∈ ω → subspace_topology (apply_fun Xi (ordsucc j)) (apply_fun Ti (ordsucc j)) (apply_fun Xi j) = apply_fun Ti j).
Set D0 to be the term (∀j : set, j ∈ ω → closed_in (apply_fun Xi (ordsucc j)) (apply_fun Ti (ordsucc j)) (apply_fun Xi j)).
We prove the intermediate claim Habc: ((A0 ∧ B0) ∧ C0).
An exact proof term for the current goal is (andEL ((A0 ∧ B0) ∧ C0) D0 Hchain).
We prove the intermediate claim Hab: (A0 ∧ B0).
An exact proof term for the current goal is (andEL (A0 ∧ B0) C0 Habc).
We prove the intermediate claim HB: B0.
An exact proof term for the current goal is (andER A0 B0 Hab).
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (omega_nat_p k HkO).
Set p to be the term (λt : set ⇒ apply_fun Xi i ⊆ apply_fun Xi (add_nat i t)).
We prove the intermediate claim Hbase: p 0.
We will prove apply_fun Xi i ⊆ apply_fun Xi (add_nat i 0).
rewrite the current goal using (add_nat_0R i) (from left to right).
An exact proof term for the current goal is (Subq_ref (apply_fun Xi i)).
We prove the intermediate claim Hstep: ∀t : set, nat_p t → p t → p (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume HtIH: apply_fun Xi i ⊆ apply_fun Xi (add_nat i t).
We will prove apply_fun Xi i ⊆ apply_fun Xi (add_nat i (ordsucc t)).
rewrite the current goal using (add_nat_SR i t HtNat) (from left to right).
We prove the intermediate claim HiNat: nat_p i.
An exact proof term for the current goal is (omega_nat_p i HiO).
We prove the intermediate claim HitNat: nat_p (add_nat i t).
An exact proof term for the current goal is (add_nat_p i HiNat t HtNat).
We prove the intermediate claim HitO: (add_nat i t) ∈ ω.
An exact proof term for the current goal is (nat_p_omega (add_nat i t) HitNat).
We prove the intermediate claim Hsucc: apply_fun Xi (add_nat i t) ⊆ apply_fun Xi (ordsucc (add_nat i t)).
An exact proof term for the current goal is (HB (add_nat i t) HitO).
An exact proof term for the current goal is (Subq_tra (apply_fun Xi i) (apply_fun Xi (add_nat i t)) (apply_fun Xi (ordsucc (add_nat i t))) HtIH Hsucc).
An exact proof term for the current goal is (nat_ind p Hbase Hstep k HkNat).
∎