Let X, Tx and P be given.
Assume HTx: topology_on X Tx.
Assume HPsubFS: P ⊆ function_space X R.
Assume HPui: ∀f x0 : set, f ∈ P → x0 ∈ X → apply_fun f x0 ∈ unit_interval.
Assume HPlf: ∀x0 : set, x0 ∈ X → ∃N : set, N ∈ Tx ∧ x0 ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.
Let x be given.
Assume HxX: x ∈ X.
Apply (HPlf x HxX) to the current goal.
Let N be given.
Assume HNpack: N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.
We prove the intermediate claim HN1: N ∈ Tx ∧ x ∈ N.
An exact proof term for the current goal is (andEL (N ∈ Tx ∧ x ∈ N) (∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0) HNpack).
We prove the intermediate claim HxN: x ∈ N.
An exact proof term for the current goal is (andER (N ∈ Tx) (x ∈ N) HN1).
We prove the intermediate claim HexF0: ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.
An exact proof term for the current goal is (andER (N ∈ Tx ∧ x ∈ N) (∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0) HNpack).
Apply HexF0 to the current goal.
Let F0 be given.
Assume HF0pack: finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.
We use F0 to witness the existential quantifier.
We prove the intermediate claim HF0left: finite F0 ∧ F0 ⊆ P.
An exact proof term for the current goal is (andEL (finite F0 ∧ F0 ⊆ P) (∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0) HF0pack).
We prove the intermediate claim HF0fin: finite F0.
An exact proof term for the current goal is (andEL (finite F0) (F0 ⊆ P) HF0left).
We prove the intermediate claim HF0subP: F0 ⊆ P.
An exact proof term for the current goal is (andER (finite F0) (F0 ⊆ P) HF0left).
We prove the intermediate claim HF0prop: ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.
An exact proof term for the current goal is (andER (finite F0 ∧ F0 ⊆ P) (∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0) HF0pack).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HF0left.
Let f be given.
Assume HfP: f ∈ P.
Assume Hfx: apply_fun f x ≠ 0.
We prove the intermediate claim HxSupp: x ∈ support_of X Tx f.
An exact proof term for the current goal is (support_of_contains_nonzero X Tx f x HTx HxX Hfx).
We prove the intermediate claim Hmeet: support_of X Tx f ∩ N ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (support_of X Tx f ∩ N) x (binintersectI (support_of X Tx f) N x HxSupp HxN)).
An exact proof term for the current goal is (HF0prop f HfP Hmeet).
Apply (finite_ex_bijection_from_omega F0 HF0fin) to the current goal.
Let n be given.
Assume Hn: ∃e : set, n ∈ ω ∧ bijection n F0 e.
Apply Hn to the current goal.
Let e be given.
Assume Hne: n ∈ ω ∧ bijection n F0 e.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (n ∈ ω) (bijection n F0 e) Hne).
We use e to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andER (n ∈ ω) (bijection n F0 e) Hne).
Set step to be the term (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)).
Set p to be the term graph (ordsucc n) (λm : set ⇒ nat_primrec 0 step m).
We use p to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n (andEL (n ∈ ω) (bijection n F0 e) Hne)).
We prove the intermediate claim Htotp: total_function_on p (ordsucc n) R.
Apply (total_function_on_graph (ordsucc n) R (λm : set ⇒ nat_primrec 0 step m)) to the current goal.
Let m be given.
Assume HmIn: m ∈ ordsucc n.
Set Pw to be the term (λt : set ⇒ t ∈ ordsucc n → nat_primrec 0 step t ∈ R).
We prove the intermediate claim Hbase: Pw 0.
Assume _.
rewrite the current goal using (nat_primrec_0 0 step) (from left to right).
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hstep: ∀t : set, nat_p t → Pw t → Pw (ordsucc t).
Let t be given.
Assume HtNat: nat_p t.
Assume IH: Pw t.
Assume HtSIn: ordsucc t ∈ ordsucc n.
We prove the intermediate claim Hsub: ordsucc t ⊆ n.
An exact proof term for the current goal is (nat_ordsucc_trans n HnNat (ordsucc t) HtSIn).
We prove the intermediate claim HtInN: t ∈ n.
An exact proof term for the current goal is (Hsub t (ordsuccI2 t)).
We prove the intermediate claim HtInSuccN: t ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n t HtInN).
We prove the intermediate claim HaccR: nat_primrec 0 step t ∈ R.
An exact proof term for the current goal is (IH HtInSuccN).
We prove the intermediate claim Hefun: function_on e n F0.
An exact proof term for the current goal is (andEL (function_on e n F0) (∀y : set, y ∈ F0 → ∃x0 : set, x0 ∈ n ∧ apply_fun e x0 = y ∧ (∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x0)) (andER (n ∈ ω) (bijection n F0 e) Hne)).
We prove the intermediate claim HetF0: apply_fun e t ∈ F0.
An exact proof term for the current goal is (Hefun t HtInN).
We prove the intermediate claim HetP: apply_fun e t ∈ P.
An exact proof term for the current goal is (HF0subP (apply_fun e t) HetF0).
We prove the intermediate claim HetFS: apply_fun e t ∈ function_space X R.
An exact proof term for the current goal is (HPsubFS (apply_fun e t) HetP).
We prove the intermediate claim HetFun: function_on (apply_fun e t) X R.
An exact proof term for the current goal is (function_on_of_function_space (apply_fun e t) X R HetFS).
We prove the intermediate claim HetxR: apply_fun (apply_fun e t) x ∈ R.
An exact proof term for the current goal is (HetFun x HxX).
rewrite the current goal using (nat_primrec_S 0 step t HtNat) (from left to right).
An exact proof term for the current goal is (real_add_SNo (nat_primrec 0 step t) HaccR (apply_fun (apply_fun e t) x) HetxR).
We prove the intermediate claim HmNat: nat_p m.
Apply (ordsuccE n m HmIn) to the current goal.
Assume HmInN: m ∈ n.
An exact proof term for the current goal is (nat_p_trans n HnNat m HmInN).
Assume Hmeq: m = n.
rewrite the current goal using Hmeq (from left to right).
An exact proof term for the current goal is HnNat.
We prove the intermediate claim HPw: Pw m.
An exact proof term for the current goal is (nat_ind Pw Hbase Hstep m HmNat).
An exact proof term for the current goal is (HPw HmIn).
An exact proof term for the current goal is (total_function_on_function_on p (ordsucc n) R Htotp).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n (andEL (n ∈ ω) (bijection n F0 e) Hne)).
We prove the intermediate claim H0In: 0 ∈ ordsucc n.
An exact proof term for the current goal is (nat_0_in_ordsucc n HnNat).
rewrite the current goal using (apply_fun_graph (ordsucc n) (λm : set ⇒ nat_primrec 0 step m) 0 H0In) (from left to right).
rewrite the current goal using (nat_primrec_0 0 step) (from left to right).
Use reflexivity.
Let k be given.
Assume HkIn: k ∈ n.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n (andEL (n ∈ ω) (bijection n F0 e) Hne)).
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (nat_p_trans n HnNat k HkIn).
We prove the intermediate claim HkInSuccN: k ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n k HkIn).
We prove the intermediate claim HkSInSuccN: ordsucc k ∈ ordsucc n.
An exact proof term for the current goal is (nat_ordsucc_in_ordsucc n HnNat k HkIn).
rewrite the current goal using (apply_fun_graph (ordsucc n) (λm : set ⇒ nat_primrec 0 step m) (ordsucc k) HkSInSuccN) (from left to right).
rewrite the current goal using (nat_primrec_S 0 step k HkNat) (from left to right).
rewrite the current goal using (apply_fun_graph (ordsucc n) (λm : set ⇒ nat_primrec 0 step m) k HkInSuccN) (from right to left).
Use reflexivity.
∎