Let b and x be given.
Assume Hb: b ∈ basis_of_subbasis R_omega_space (product_subbasis_full ω (const_space_family ω R R_standard_topology)).
Assume Hxb: x ∈ b.
We will prove b ∩ Romega_infty ≠ Empty.
Set X to be the term R_omega_space.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set S to be the term product_subbasis_full ω Xi.
Set B to be the term basis_of_subbasis X S.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is Hb.
We prove the intermediate claim Hbfin: b ∈ finite_intersections_of X S.
An exact proof term for the current goal is (SepE1 (finite_intersections_of X S) (λb0 : set ⇒ b0 ≠ Empty) b HbB).
We prove the intermediate claim Hbne: b ≠ Empty.
An exact proof term for the current goal is (SepE2 (finite_intersections_of X S) (λb0 : set ⇒ b0 ≠ Empty) b HbB).
Apply (ReplE_impred (finite_subcollections S) (λF0 : set ⇒ intersection_of_family X F0) b Hbfin (b ∩ Romega_infty ≠ Empty)) to the current goal.
Let F be given.
Assume HF: F ∈ finite_subcollections S.
Assume Hbeq: b = intersection_of_family X F.
rewrite the current goal using Hbeq (from left to right) at position 1.
We prove the intermediate claim HFpow: F ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim HFsubS: F ⊆ S.
An exact proof term for the current goal is (PowerE S F HFpow).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) F HF).
We prove the intermediate claim HxInt: x ∈ intersection_of_family X F.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U : set, U ∈ F → x0 ∈ U) x HxInt).
We prove the intermediate claim HxAll: ∀s : set, s ∈ F → x ∈ s.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ F → x0 ∈ U) x HxInt).
Set CylFam to be the term λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}.
Set pick_i to be the term λs : set ⇒ Eps_i (λi : set ⇒ i ∈ ω ∧ s ∈ CylFam i).
We prove the intermediate claim Hpick_omega: ∀s : set, s ∈ F → pick_i s ∈ ω.
Let s be given.
Assume HsF: s ∈ F.
We will prove pick_i s ∈ ω.
We prove the intermediate claim HsS: s ∈ S.
An exact proof term for the current goal is (HFsubS s HsF).
We prove the intermediate claim Hex: ∃i : set, i ∈ ω ∧ s ∈ CylFam i.
An exact proof term for the current goal is (famunionE ω (λi : set ⇒ CylFam i) s HsS).
We prove the intermediate claim Hpick: pick_i s ∈ ω ∧ s ∈ CylFam (pick_i s).
An exact proof term for the current goal is (Eps_i_ex (λi : set ⇒ i ∈ ω ∧ s ∈ CylFam i) Hex).
An exact proof term for the current goal is (andEL (pick_i s ∈ ω) (s ∈ CylFam (pick_i s)) Hpick).
We prove the intermediate claim Hpick_in: ∀s : set, s ∈ F → s ∈ CylFam (pick_i s).
Let s be given.
Assume HsF: s ∈ F.
We will prove s ∈ CylFam (pick_i s).
We prove the intermediate claim HsS: s ∈ S.
An exact proof term for the current goal is (HFsubS s HsF).
We prove the intermediate claim Hex: ∃i : set, i ∈ ω ∧ s ∈ CylFam i.
An exact proof term for the current goal is (famunionE ω (λi : set ⇒ CylFam i) s HsS).
We prove the intermediate claim Hpick: pick_i s ∈ ω ∧ s ∈ CylFam (pick_i s).
An exact proof term for the current goal is (Eps_i_ex (λi : set ⇒ i ∈ ω ∧ s ∈ CylFam i) Hex).
An exact proof term for the current goal is (andER (pick_i s ∈ ω) (s ∈ CylFam (pick_i s)) Hpick).
Set J to be the term {pick_i s|s ∈ F}.
We prove the intermediate claim HJfin: finite J.
An exact proof term for the current goal is (Repl_finite (λs : set ⇒ pick_i s) F HFfin).
We prove the intermediate claim HJsub: J ⊆ ω.
Let j be given.
Assume Hj: j ∈ J.
We will prove j ∈ ω.
Apply (ReplE_impred F (λs : set ⇒ pick_i s) j Hj (j ∈ ω)) to the current goal.
Let s be given.
Assume HsF: s ∈ F.
Assume Hjeq: j = pick_i s.
rewrite the current goal using Hjeq (from left to right).
An exact proof term for the current goal is (Hpick_omega s HsF).
We prove the intermediate claim Hexn: ∃n ∈ ω, ∀m ∈ J, m ∈ n.
An exact proof term for the current goal is (finite_subset_of_omega_bounded J HJsub HJfin).
Apply Hexn to the current goal.
Let n be given.
Assume Hnand.
We prove the intermediate claim HnO: n ∈ ω.
An exact proof term for the current goal is (andEL (n ∈ ω) (∀m ∈ J, m ∈ n) Hnand).
We prove the intermediate claim Hnprop: ∀m ∈ J, m ∈ n.
An exact proof term for the current goal is (andER (n ∈ ω) (∀m ∈ J, m ∈ n) Hnand).
Set h to be the term λi : set ⇒ If_i (n ∈ i) 0 (apply_fun x i).
Set f to be the term graph ω h.
We prove the intermediate claim HhR: ∀i : set, i ∈ ω → h i ∈ R.
Let i be given.
Assume Hi: i ∈ ω.
We will prove h i ∈ R.
We prove the intermediate claim Hhdef: h i = If_i (n ∈ i) 0 (apply_fun x i).
Use reflexivity.
Apply (xm (n ∈ i)) to the current goal.
Assume Hni: n ∈ i.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (If_i_1 (n ∈ i) 0 (apply_fun x i) Hni) (from left to right).
An exact proof term for the current goal is real_0.
Assume Hnni: ¬ (n ∈ i).
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (If_i_0 (n ∈ i) 0 (apply_fun x i) Hnni) (from left to right).
An exact proof term for the current goal is (Romega_coord_in_R x i HxX Hi).
We prove the intermediate claim HfX: f ∈ X.
An exact proof term for the current goal is (graph_omega_in_Romega_space h HhR).
We prove the intermediate claim Hftilde: f ∈ Romega_tilde n.
We will prove f ∈ Romega_tilde n.
We will prove f ∈ {f0 ∈ X|∀i : set, i ∈ ω → n ∈ i → apply_fun f0 i = 0}.
Apply (SepI X (λf0 : set ⇒ ∀i : set, i ∈ ω → n ∈ i → apply_fun f0 i = 0) f HfX) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
Assume Hni: n ∈ i.
We will prove apply_fun f i = 0.
We prove the intermediate claim Happ: apply_fun f i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hhdef: h i = If_i (n ∈ i) 0 (apply_fun x i).
Use reflexivity.
rewrite the current goal using Hhdef (from left to right).
rewrite the current goal using (If_i_1 (n ∈ i) 0 (apply_fun x i) Hni) (from left to right).
Use reflexivity.
We prove the intermediate claim HfA: f ∈ Romega_infty.
We will prove f ∈ Romega_infty.
Set Y to be the term Romega_tilde n.
We prove the intermediate claim HYn: Y ∈ {Romega_tilde k|k ∈ ω}.
An exact proof term for the current goal is (ReplI ω (λk : set ⇒ Romega_tilde k) n HnO).
An exact proof term for the current goal is (UnionI {Romega_tilde k|k ∈ ω} f Y Hftilde HYn).
We prove the intermediate claim HfInt: f ∈ intersection_of_family X F.
We will prove f ∈ intersection_of_family X F.
We will prove f ∈ {x0 ∈ X|∀U : set, U ∈ F → x0 ∈ U}.
Apply (SepI X (λx0 : set ⇒ ∀U : set, U ∈ F → x0 ∈ U) f HfX) to the current goal.
Let s be given.
Assume HsF: s ∈ F.
We will prove f ∈ s.
We prove the intermediate claim HsCyl: s ∈ CylFam (pick_i s).
An exact proof term for the current goal is (Hpick_in s HsF).
Apply (ReplE_impred (space_family_topology Xi (pick_i s)) (λU : set ⇒ product_cylinder ω Xi (pick_i s) U) s HsCyl (f ∈ s)) to the current goal.
Let U be given.
Assume HU: U ∈ space_family_topology Xi (pick_i s).
Assume Hseq: s = product_cylinder ω Xi (pick_i s) U.
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim Hxs: x ∈ s.
An exact proof term for the current goal is (HxAll s HsF).
We prove the intermediate claim HxCyl: x ∈ product_cylinder ω Xi (pick_i s) U.
rewrite the current goal using Hseq (from right to left).
An exact proof term for the current goal is Hxs.
We prove the intermediate claim Hxcylprop: (pick_i s ∈ ω ∧ U ∈ space_family_topology Xi (pick_i s)) ∧ apply_fun x (pick_i s) ∈ U.
An exact proof term for the current goal is (SepE2 (product_space ω Xi) (λf0 : set ⇒ (pick_i s ∈ ω ∧ U ∈ space_family_topology Xi (pick_i s)) ∧ apply_fun f0 (pick_i s) ∈ U) x HxCyl).
We prove the intermediate claim HxUi: apply_fun x (pick_i s) ∈ U.
An exact proof term for the current goal is (andER (pick_i s ∈ ω ∧ U ∈ space_family_topology Xi (pick_i s)) (apply_fun x (pick_i s) ∈ U) Hxcylprop).
We prove the intermediate claim Hidx: pick_i s ∈ ω.
An exact proof term for the current goal is (Hpick_omega s HsF).
We prove the intermediate claim HidxJ: pick_i s ∈ J.
An exact proof term for the current goal is (ReplI F (λs0 : set ⇒ pick_i s0) s HsF).
We prove the intermediate claim Hidxn: pick_i s ∈ n.
An exact proof term for the current goal is (Hnprop (pick_i s) HidxJ).
We prove the intermediate claim Hnot_nin: ¬ (n ∈ pick_i s).
Assume Hnin: n ∈ pick_i s.
An exact proof term for the current goal is (In_no2cycle (pick_i s) n Hidxn Hnin).
We will prove f ∈ product_cylinder ω Xi (pick_i s) U.
We will prove f ∈ {f0 ∈ product_space ω Xi|pick_i s ∈ ω ∧ U ∈ space_family_topology Xi (pick_i s) ∧ apply_fun f0 (pick_i s) ∈ U}.
We prove the intermediate claim HfProd: f ∈ product_space ω Xi.
An exact proof term for the current goal is HfX.
We prove the intermediate claim Hpropf: pick_i s ∈ ω ∧ U ∈ space_family_topology Xi (pick_i s) ∧ apply_fun f (pick_i s) ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hidx.
An exact proof term for the current goal is HU.
We will prove apply_fun f (pick_i s) ∈ U.
We prove the intermediate claim Happf: apply_fun f (pick_i s) = h (pick_i s).
An exact proof term for the current goal is (apply_fun_graph ω h (pick_i s) Hidx).
rewrite the current goal using Happf (from left to right).
We prove the intermediate claim Hhdef: h (pick_i s) = If_i (n ∈ pick_i s) 0 (apply_fun x (pick_i s)).
Use reflexivity.
rewrite the current goal using Hhdef (from left to right).
We prove the intermediate claim Hif: If_i (n ∈ pick_i s) 0 (apply_fun x (pick_i s)) = apply_fun x (pick_i s).
An exact proof term for the current goal is (If_i_0 (n ∈ pick_i s) 0 (apply_fun x (pick_i s)) Hnot_nin).
rewrite the current goal using Hif (from left to right).
An exact proof term for the current goal is HxUi.
An exact proof term for the current goal is (SepI (product_space ω Xi) (λf0 : set ⇒ pick_i s ∈ ω ∧ U ∈ space_family_topology Xi (pick_i s) ∧ apply_fun f0 (pick_i s) ∈ U) f HfProd Hpropf).
Assume Hempty: (intersection_of_family X F) ∩ Romega_infty = Empty.
We will prove False.
We prove the intermediate claim HfB: f ∈ intersection_of_family X F.
An exact proof term for the current goal is HfInt.
We prove the intermediate claim HfBA: f ∈ (intersection_of_family X F) ∩ Romega_infty.
An exact proof term for the current goal is (binintersectI (intersection_of_family X F) Romega_infty f HfB HfA).
We prove the intermediate claim HfE: f ∈ Empty.
We prove the intermediate claim HsubE: (intersection_of_family X F) ∩ Romega_infty ⊆ Empty.
rewrite the current goal using Hempty (from left to right).
An exact proof term for the current goal is (Subq_ref Empty).
An exact proof term for the current goal is (HsubE f HfBA).
An exact proof term for the current goal is (EmptyE f HfE).
∎