Let X, Tx, Y, d, fn, N and eps be given.
Assume HTx: topology_on X Tx.
Assume Hd: metric_on_total Y d.
Assume Hcont: ∀n : set, n ∈ ω → continuous_map X Tx Y (metric_topology Y d) (apply_fun fn n).
Assume HN: N ∈ ω.
Assume HepsR: eps ∈ R.
We will prove closed_in X Tx (A_N_eps X Y d fn N eps).
Set Ubad to be the term {x ∈ X|∃n : set, n ∈ ω ∧ N ⊆ n ∧ ∃m : set, m ∈ ω ∧ N ⊆ m ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x))}.
We prove the intermediate claim HdefA: A_N_eps X Y d fn N eps = {x ∈ X|∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) eps}.
Use reflexivity.
We prove the intermediate claim HeqComp: A_N_eps X Y d fn N eps = X ∖ Ubad.
rewrite the current goal using HdefA (from left to right).
Apply set_ext to the current goal.
Let x be given.
Assume HxA: x ∈ {x0 ∈ X|∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps}.
We will prove x ∈ X ∖ Ubad.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps) x HxA).
We prove the intermediate claim HxProp: ∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) eps.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps) x HxA).
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
Assume HxU: x ∈ Ubad.
We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ N ⊆ n ∧ ∃m : set, m ∈ ω ∧ N ⊆ m ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃n0 : set, n0 ∈ ω ∧ N ⊆ n0 ∧ ∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x0,apply_fun (apply_fun fn m0) x0))) x HxU).
Apply Hexn to the current goal.
Let n be given.
Assume Hn.
We prove the intermediate claim HnCore: (n ∈ ω ∧ N ⊆ n).
An exact proof term for the current goal is (andEL (n ∈ ω ∧ N ⊆ n) (∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m0) x))) Hn).
We prove the intermediate claim Hexm: ∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m0) x)).
An exact proof term for the current goal is (andER (n ∈ ω ∧ N ⊆ n) (∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m0) x))) Hn).
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (N ⊆ n) HnCore).
We prove the intermediate claim HNn: N ⊆ n.
An exact proof term for the current goal is (andER (n ∈ ω) (N ⊆ n) HnCore).
Apply Hexm to the current goal.
Let m0 be given.
Assume Hm0.
We prove the intermediate claim Hm0Core: (m0 ∈ ω ∧ N ⊆ m0).
An exact proof term for the current goal is (andEL (m0 ∈ ω ∧ N ⊆ m0) (Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m0) x))) Hm0).
We prove the intermediate claim Hlt: Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m0) x)).
An exact proof term for the current goal is (andER (m0 ∈ ω ∧ N ⊆ m0) (Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m0) x))) Hm0).
We prove the intermediate claim Hm0O: m0 ∈ ω.
An exact proof term for the current goal is (andEL (m0 ∈ ω) (N ⊆ m0) Hm0Core).
We prove the intermediate claim HNm0: N ⊆ m0.
An exact proof term for the current goal is (andER (m0 ∈ ω) (N ⊆ m0) Hm0Core).
We prove the intermediate claim Hle: Rle (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m0) x)) eps.
An exact proof term for the current goal is (HxProp n HnO HNn m0 Hm0O HNm0).
An exact proof term for the current goal is ((RleE_nlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m0) x)) eps Hle) Hlt).
Let x be given.
Assume Hx: x ∈ X ∖ Ubad.
We will prove x ∈ {x0 ∈ X|∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps}.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (setminusE1 X Ubad x Hx).
We prove the intermediate claim HxNotU: x ∉ Ubad.
An exact proof term for the current goal is (setminusE2 X Ubad x Hx).
Apply (SepI X (λx0 : set ⇒ ∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps) x HxX) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HNn: N ⊆ n.
Let m be given.
Assume HmO: m ∈ ω.
Assume HNm: N ⊆ m.
We prove the intermediate claim HfnOn: function_on (apply_fun fn n) X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y (metric_topology Y d) (apply_fun fn n) (Hcont n HnO)).
We prove the intermediate claim HfmOn: function_on (apply_fun fn m) X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y (metric_topology Y d) (apply_fun fn m) (Hcont m HmO)).
We prove the intermediate claim HnxY: apply_fun (apply_fun fn n) x ∈ Y.
An exact proof term for the current goal is (HfnOn x HxX).
We prove the intermediate claim HmxY: apply_fun (apply_fun fn m) x ∈ Y.
An exact proof term for the current goal is (HfmOn x HxX).
We prove the intermediate claim HdTot: total_function_on d (setprod Y Y) R.
An exact proof term for the current goal is (metric_on_total_total_function Y d Hd).
We prove the intermediate claim Hpair: (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x) ∈ setprod Y Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun (apply_fun fn n) x) (apply_fun (apply_fun fn m) x) HnxY HmxY).
We prove the intermediate claim HdxR: apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x) ∈ R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y d (setprod Y Y) R (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x) HdTot Hpair).
Apply (RleI (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) eps HdxR HepsR) to the current goal.
Assume Hlt: Rlt eps (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)).
We prove the intermediate claim HxBad: x ∈ Ubad.
Apply (SepI X (λx0 : set ⇒ ∃n0 : set, n0 ∈ ω ∧ N ⊆ n0 ∧ ∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x0,apply_fun (apply_fun fn m0) x0))) x HxX) to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
An exact proof term for the current goal is HNn.
We use m to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HmO.
An exact proof term for the current goal is HNm.
An exact proof term for the current goal is Hlt.
An exact proof term for the current goal is (HxNotU HxBad).
rewrite the current goal using HeqComp (from left to right).
We prove the intermediate claim HUbad: Ubad ∈ Tx.
Set Veps to be the term {r ∈ R|Rlt eps r}.
We prove the intermediate claim HVeps: Veps ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_in_R_standard_topology eps HepsR).
Set IndN to be the term {k ∈ ω|N ⊆ k}.
Set Iprod to be the term setprod IndN IndN.
Set Fam to be the term {preimage_of X (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) Veps|p ∈ Iprod}.
We prove the intermediate claim HFamSub: Fam ⊆ Tx.
Let U be given.
Assume HU: U ∈ Fam.
Apply (ReplE_impred Iprod (λp0 : set ⇒ preimage_of X (compose_fun X (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) d) Veps) U HU (U ∈ Tx)) to the current goal.
Let p be given.
Assume Hp: p ∈ Iprod.
Assume HeqU: U = preimage_of X (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) Veps.
We prove the intermediate claim Hp0In: p 0 ∈ IndN.
An exact proof term for the current goal is (ap0_Sigma IndN (λk : set ⇒ IndN) p Hp).
We prove the intermediate claim Hp1In: p 1 ∈ IndN.
An exact proof term for the current goal is (ap1_Sigma IndN (λk : set ⇒ IndN) p Hp).
We prove the intermediate claim HnO: (p 0) ∈ ω.
An exact proof term for the current goal is (SepE1 ω (λk : set ⇒ N ⊆ k) (p 0) Hp0In).
We prove the intermediate claim HmO: (p 1) ∈ ω.
An exact proof term for the current goal is (SepE1 ω (λk : set ⇒ N ⊆ k) (p 1) Hp1In).
Set n to be the term p 0.
Set m to be the term p 1.
Set h to be the term compose_fun X (pair_map X (apply_fun fn n) (apply_fun fn m)) d.
We prove the intermediate claim HpairCont: continuous_map X Tx (setprod Y Y) (product_topology Y (metric_topology Y d) Y (metric_topology Y d)) (pair_map X (apply_fun fn n) (apply_fun fn m)).
An exact proof term for the current goal is (maps_into_products_axiom X Tx Y (metric_topology Y d) Y (metric_topology Y d) (apply_fun fn n) (apply_fun fn m) (Hcont n HnO) (Hcont m HmO)).
We prove the intermediate claim Hdcont: continuous_map (setprod Y Y) (product_topology Y (metric_topology Y d) Y (metric_topology Y d)) R R_standard_topology d.
An exact proof term for the current goal is (metric_distance_continuous Y d Hd).
We prove the intermediate claim Hhcont: continuous_map X Tx R R_standard_topology h.
An exact proof term for the current goal is (composition_continuous X Tx (setprod Y Y) (product_topology Y (metric_topology Y d) Y (metric_topology Y d)) R R_standard_topology (pair_map X (apply_fun fn n) (apply_fun fn m)) d HpairCont Hdcont).
We prove the intermediate claim HpreIn: preimage_of X h Veps ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology h Hhcont Veps HVeps).
rewrite the current goal using HeqU (from left to right).
An exact proof term for the current goal is HpreIn.
We prove the intermediate claim HUbadEq: Ubad = ⋃ Fam.
Apply set_ext to the current goal.
Let x be given.
Assume HxU: x ∈ Ubad.
We will prove x ∈ ⋃ Fam.
We prove the intermediate claim Hexnm: ∃n0 : set, n0 ∈ ω ∧ N ⊆ n0 ∧ ∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x)).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃n0 : set, n0 ∈ ω ∧ N ⊆ n0 ∧ ∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x0,apply_fun (apply_fun fn m0) x0))) x HxU).
Apply Hexnm to the current goal.
Let n0 be given.
Assume Hn0.
We prove the intermediate claim Hn0Core: (n0 ∈ ω ∧ N ⊆ n0).
An exact proof term for the current goal is (andEL (n0 ∈ ω ∧ N ⊆ n0) (∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x))) Hn0).
We prove the intermediate claim Hexm0: ∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x)).
An exact proof term for the current goal is (andER (n0 ∈ ω ∧ N ⊆ n0) (∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x))) Hn0).
We prove the intermediate claim Hn0O: n0 ∈ ω.
An exact proof term for the current goal is (andEL (n0 ∈ ω) (N ⊆ n0) Hn0Core).
We prove the intermediate claim HNn0: N ⊆ n0.
An exact proof term for the current goal is (andER (n0 ∈ ω) (N ⊆ n0) Hn0Core).
Apply Hexm0 to the current goal.
Let m0 be given.
Assume Hm0.
We prove the intermediate claim Hm0Core: (m0 ∈ ω ∧ N ⊆ m0).
An exact proof term for the current goal is (andEL (m0 ∈ ω ∧ N ⊆ m0) (Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x))) Hm0).
We prove the intermediate claim Hlt: Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x)).
An exact proof term for the current goal is (andER (m0 ∈ ω ∧ N ⊆ m0) (Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x))) Hm0).
We prove the intermediate claim Hm0O: m0 ∈ ω.
An exact proof term for the current goal is (andEL (m0 ∈ ω) (N ⊆ m0) Hm0Core).
We prove the intermediate claim HNm0: N ⊆ m0.
An exact proof term for the current goal is (andER (m0 ∈ ω) (N ⊆ m0) Hm0Core).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∃n1 : set, n1 ∈ ω ∧ N ⊆ n1 ∧ ∃m1 : set, m1 ∈ ω ∧ N ⊆ m1 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n1) x0,apply_fun (apply_fun fn m1) x0))) x HxU).
We prove the intermediate claim Hn0In: n0 ∈ IndN.
An exact proof term for the current goal is (SepI ω (λk : set ⇒ N ⊆ k) n0 Hn0O HNn0).
We prove the intermediate claim Hm0In: m0 ∈ IndN.
An exact proof term for the current goal is (SepI ω (λk : set ⇒ N ⊆ k) m0 Hm0O HNm0).
Set p0 to be the term (n0,m0).
We prove the intermediate claim Hp0: p0 ∈ Iprod.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma IndN IndN n0 m0 Hn0In Hm0In).
Set U0 to be the term preimage_of X (compose_fun X (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) d) Veps.
We prove the intermediate claim HU0Fam: U0 ∈ Fam.
An exact proof term for the current goal is (ReplI Iprod (λp1 : set ⇒ preimage_of X (compose_fun X (pair_map X (apply_fun fn (p1 0)) (apply_fun fn (p1 1))) d) Veps) p0 Hp0).
We prove the intermediate claim HxU0in: x ∈ U0.
We prove the intermediate claim HxCond: apply_fun (compose_fun X (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) d) x ∈ Veps.
We prove the intermediate claim Hn0Fn: function_on (apply_fun fn n0) X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y (metric_topology Y d) (apply_fun fn n0) (Hcont n0 Hn0O)).
We prove the intermediate claim Hm0Fn: function_on (apply_fun fn m0) X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y (metric_topology Y d) (apply_fun fn m0) (Hcont m0 Hm0O)).
We prove the intermediate claim Hn0xY: apply_fun (apply_fun fn n0) x ∈ Y.
An exact proof term for the current goal is (Hn0Fn x HxX).
We prove the intermediate claim Hm0xY: apply_fun (apply_fun fn m0) x ∈ Y.
An exact proof term for the current goal is (Hm0Fn x HxX).
We prove the intermediate claim HdTot: total_function_on d (setprod Y Y) R.
An exact proof term for the current goal is (metric_on_total_total_function Y d Hd).
We prove the intermediate claim Hpair: (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x) ∈ setprod Y Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun (apply_fun fn n0) x) (apply_fun (apply_fun fn m0) x) Hn0xY Hm0xY).
We prove the intermediate claim HdvalR: apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x) ∈ R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y d (setprod Y Y) R (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x) HdTot Hpair).
We prove the intermediate claim Happ0: apply_fun (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) x = (apply_fun (apply_fun fn (p0 0)) x,apply_fun (apply_fun fn (p0 1)) x).
An exact proof term for the current goal is (pair_map_apply X Y Y (apply_fun fn (p0 0)) (apply_fun fn (p0 1)) x HxX).
We prove the intermediate claim Happ1: apply_fun (compose_fun X (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) d) x = apply_fun d (apply_fun (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) x).
An exact proof term for the current goal is (compose_fun_apply X (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) d x HxX).
rewrite the current goal using Happ1 (from left to right).
rewrite the current goal using Happ0 (from left to right).
rewrite the current goal using (tuple_2_0_eq n0 m0) (from left to right).
rewrite the current goal using (tuple_2_1_eq n0 m0) (from left to right).
An exact proof term for the current goal is (SepI R (λr : set ⇒ Rlt eps r) (apply_fun d (apply_fun (apply_fun fn n0) x,apply_fun (apply_fun fn m0) x)) HdvalR Hlt).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (compose_fun X (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) d) x0 ∈ Veps) x HxX HxCond).
An exact proof term for the current goal is (UnionI Fam x U0 HxU0in HU0Fam).
Let x be given.
Assume Hx: x ∈ ⋃ Fam.
We will prove x ∈ Ubad.
Apply (UnionE_impred Fam x Hx (x ∈ Ubad)) to the current goal.
Let U be given.
Assume HxU: x ∈ U.
Assume HU: U ∈ Fam.
We prove the intermediate claim Hexp: ∃p : set, p ∈ Iprod ∧ U = preimage_of X (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) Veps.
An exact proof term for the current goal is (ReplE Iprod (λp0 : set ⇒ preimage_of X (compose_fun X (pair_map X (apply_fun fn (p0 0)) (apply_fun fn (p0 1))) d) Veps) U HU).
Apply Hexp to the current goal.
Let p be given.
Assume Hp.
We prove the intermediate claim HpI: p ∈ Iprod.
An exact proof term for the current goal is (andEL (p ∈ Iprod) (U = preimage_of X (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) Veps) Hp).
We prove the intermediate claim HUdef: U = preimage_of X (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) Veps.
An exact proof term for the current goal is (andER (p ∈ Iprod) (U = preimage_of X (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) Veps) Hp).
We prove the intermediate claim Hp0In: p 0 ∈ IndN.
An exact proof term for the current goal is (ap0_Sigma IndN (λk : set ⇒ IndN) p HpI).
We prove the intermediate claim Hp1In: p 1 ∈ IndN.
An exact proof term for the current goal is (ap1_Sigma IndN (λk : set ⇒ IndN) p HpI).
We prove the intermediate claim HnO: (p 0) ∈ ω.
An exact proof term for the current goal is (SepE1 ω (λk : set ⇒ N ⊆ k) (p 0) Hp0In).
We prove the intermediate claim HmO: (p 1) ∈ ω.
An exact proof term for the current goal is (SepE1 ω (λk : set ⇒ N ⊆ k) (p 1) Hp1In).
We prove the intermediate claim HNn: N ⊆ (p 0).
An exact proof term for the current goal is (SepE2 ω (λk : set ⇒ N ⊆ k) (p 0) Hp0In).
We prove the intermediate claim HNm: N ⊆ (p 1).
An exact proof term for the current goal is (SepE2 ω (λk : set ⇒ N ⊆ k) (p 1) Hp1In).
We prove the intermediate claim HxPre: x ∈ preimage_of X (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) Veps.
We will prove x ∈ preimage_of X (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) Veps.
rewrite the current goal using HUdef (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) x0 ∈ Veps) x HxPre).
We prove the intermediate claim HxVal: apply_fun (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) x ∈ Veps.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (compose_fun X (pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1))) d) x0 ∈ Veps) x HxPre).
Set fpair to be the term pair_map X (apply_fun fn (p 0)) (apply_fun fn (p 1)).
We prove the intermediate claim HpairEq: apply_fun fpair x = (apply_fun (apply_fun fn (p 0)) x,apply_fun (apply_fun fn (p 1)) x).
An exact proof term for the current goal is (pair_map_apply X Y Y (apply_fun fn (p 0)) (apply_fun fn (p 1)) x HxX).
We prove the intermediate claim HcompEq: apply_fun (compose_fun X fpair d) x = apply_fun d (apply_fun fpair x).
An exact proof term for the current goal is (compose_fun_apply X fpair d x HxX).
We prove the intermediate claim HvalIn: apply_fun d (apply_fun (apply_fun fn (p 0)) x,apply_fun (apply_fun fn (p 1)) x) ∈ Veps.
We will prove apply_fun d (apply_fun (apply_fun fn (p 0)) x,apply_fun (apply_fun fn (p 1)) x) ∈ Veps.
rewrite the current goal using HpairEq (from right to left).
rewrite the current goal using HcompEq (from right to left).
An exact proof term for the current goal is HxVal.
We prove the intermediate claim Hlt: Rlt eps (apply_fun d (apply_fun (apply_fun fn (p 0)) x,apply_fun (apply_fun fn (p 1)) x)).
An exact proof term for the current goal is (SepE2 R (λr : set ⇒ Rlt eps r) (apply_fun d (apply_fun (apply_fun fn (p 0)) x,apply_fun (apply_fun fn (p 1)) x)) HvalIn).
Apply (SepI X (λx0 : set ⇒ ∃n0 : set, n0 ∈ ω ∧ N ⊆ n0 ∧ ∃m0 : set, m0 ∈ ω ∧ N ⊆ m0 ∧ Rlt eps (apply_fun d (apply_fun (apply_fun fn n0) x0,apply_fun (apply_fun fn m0) x0))) x HxX) to the current goal.
We use (p 0) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HnO.
An exact proof term for the current goal is HNn.
We use (p 1) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HmO.
An exact proof term for the current goal is HNm.
An exact proof term for the current goal is Hlt.
We prove the intermediate claim HUnionIn: ⋃ Fam ∈ Tx.
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx Fam HFamSub).
An exact proof term for the current goal is (topology_union_axiom X Tx HTx Fam HFamPow).
rewrite the current goal using HUbadEq (from left to right).
An exact proof term for the current goal is HUnionIn.
An exact proof term for the current goal is (closed_of_open_complement X Tx Ubad HTx HUbad).
∎