Let Xi, Ti and j be given.
Assume Hchain: coherent_chain Xi Ti.
Assume HjO: j ∈ ω.
Set A0 to be the term (∀t : set, t ∈ ω → topology_on (apply_fun Xi t) (apply_fun Ti t)).
Set B0 to be the term (∀t : set, t ∈ ω → apply_fun Xi t ⊆ apply_fun Xi (ordsucc t)).
Set C0 to be the term (∀t : set, t ∈ ω → subspace_topology (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) (apply_fun Xi t) = apply_fun Ti t).
Set D0 to be the term (∀t : set, t ∈ ω → closed_in (apply_fun Xi (ordsucc t)) (apply_fun Ti (ordsucc t)) (apply_fun Xi t)).
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).
Set p to be the term (λn : set ⇒ ∀i : set, i ∈ n → apply_fun Xi i ⊆ apply_fun Xi n).
We prove the intermediate claim Hbase: p 0.
Let i be given.
Assume Hi0: i ∈ 0.
We will prove apply_fun Xi i ⊆ apply_fun Xi 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE i Hi0).
We prove the intermediate claim Hstep: ∀n : set, nat_p n → p n → p (ordsucc n).
Let n be given.
Assume HnNat: nat_p n.
Assume HnIH: p n.
We will prove p (ordsucc n).
Let i be given.
Assume HiSn: i ∈ ordsucc n.
Apply (ordsuccE n i HiSn (apply_fun Xi i ⊆ apply_fun Xi (ordsucc n))) to the current goal.
Assume Hin: i ∈ n.
We prove the intermediate claim Hsub1: apply_fun Xi i ⊆ apply_fun Xi n.
An exact proof term for the current goal is (HnIH i Hin).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (nat_p_omega n HnNat).
We prove the intermediate claim Hsub2: apply_fun Xi n ⊆ apply_fun Xi (ordsucc n).
An exact proof term for the current goal is (HB n HnO).
An exact proof term for the current goal is (Subq_tra (apply_fun Xi i) (apply_fun Xi n) (apply_fun Xi (ordsucc n)) Hsub1 Hsub2).
Assume Heq: i = n.
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (nat_p_omega n HnNat).
An exact proof term for the current goal is (HB n HnO).
We prove the intermediate claim HjNat: nat_p j.
An exact proof term for the current goal is (omega_nat_p j HjO).
We prove the intermediate claim Hjprop: p j.
An exact proof term for the current goal is (nat_ind p Hbase Hstep j HjNat).
Let i be given.
Assume Hij: i ∈ j.
An exact proof term for the current goal is (Hjprop i Hij).
∎