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 Hx0: x ∈ Romega_tilde 0.
Assume Hxb: x ∈ b.
We will prove b ∩ image_of Romega_singleton_map R ≠ 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).
Apply (ReplE_impred (finite_subcollections S) (λF0 : set ⇒ intersection_of_family X F0) b Hbfin (b ∩ image_of Romega_singleton_map R ≠ 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 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).
We prove the intermediate claim Hx0prop: ∀i : set, i ∈ ω → 0 ∈ i → apply_fun x i = 0.
An exact proof term for the current goal is (SepE2 X (λf0 : set ⇒ ∀i : set, i ∈ ω → 0 ∈ i → apply_fun f0 i = 0) x Hx0).
Set r to be the term apply_fun x 0.
We prove the intermediate claim H0o: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R x 0 HxX H0o).
Set f to be the term apply_fun Romega_singleton_map r.
We prove the intermediate claim HfX: f ∈ X.
rewrite the current goal using (Romega_singleton_map_apply r HrR) (from left to right).
An exact proof term for the current goal is (Romega_singleton_seq_in_Romega_space r HrR).
We prove the intermediate claim HfImg: f ∈ image_of Romega_singleton_map R.
We prove the intermediate claim Hfeq: f = apply_fun Romega_singleton_map r.
Use reflexivity.
rewrite the current goal using Hfeq (from left to right).
An exact proof term for the current goal is (ReplI R (λa : set ⇒ apply_fun Romega_singleton_map a) r HrR).
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 HsS: s ∈ S.
An exact proof term for the current goal is (HFsubS s HsF).
Set CylFam to be the term (λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}).
We prove the intermediate claim HsCyl: s ∈ (⋃i ∈ ωCylFam i).
An exact proof term for the current goal is HsS.
Apply (famunionE_impred ω CylFam s HsCyl (f ∈ s)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
Assume HsFi: s ∈ CylFam i.
Apply (ReplE_impred (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder ω Xi i U0) s HsFi (f ∈ s)) to the current goal.
Let U be given.
Assume HU: U ∈ space_family_topology Xi i.
Assume Hseq: s = product_cylinder ω Xi i U.
rewrite the current goal using Hseq (from left to right).
We will prove f ∈ product_cylinder ω Xi i U.
We will prove f ∈ {f0 ∈ product_space ω Xi|i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ 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: i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hi.
An exact proof term for the current goal is HU.
We will prove apply_fun f i ∈ U.
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 i 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: (i ∈ ω ∧ U ∈ space_family_topology Xi i) ∧ apply_fun x i ∈ U.
An exact proof term for the current goal is (SepE2 (product_space ω Xi) (λf0 : set ⇒ (i ∈ ω ∧ U ∈ space_family_topology Xi i) ∧ apply_fun f0 i ∈ U) x HxCyl).
We prove the intermediate claim HxUi: apply_fun x i ∈ U.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U ∈ space_family_topology Xi i) (apply_fun x i ∈ U) Hxcylprop).
rewrite the current goal using (Romega_singleton_map_apply r HrR) (from left to right).
rewrite the current goal using (Romega_singleton_seq_apply r i HrR Hi) (from left to right).
We prove the intermediate claim Hnat: nat_p i.
An exact proof term for the current goal is (omega_nat_p i Hi).
Apply (nat_inv i Hnat) to the current goal.
Assume Hieq0: i = 0.
rewrite the current goal using Hieq0 (from left to right).
We prove the intermediate claim Hnot0in0: ¬ (0 ∈ 0).
Assume H0in0: 0 ∈ 0.
We will prove False.
An exact proof term for the current goal is (EmptyE 0 H0in0).
rewrite the current goal using (If_i_0 (0 ∈ 0) 0 r Hnot0in0) (from left to right).
We prove the intermediate claim HxUi0: apply_fun x 0 ∈ U.
rewrite the current goal using Hieq0 (from right to left).
An exact proof term for the current goal is HxUi.
We prove the intermediate claim Hreq: r = apply_fun x 0.
Use reflexivity.
rewrite the current goal using Hreq (from left to right).
An exact proof term for the current goal is HxUi0.
Assume Hexk: ∃k : set, nat_p k ∧ i = ordsucc k.
Apply Hexk to the current goal.
Let k be given.
Assume Hkconj: nat_p k ∧ i = ordsucc k.
We prove the intermediate claim HkNat: nat_p k.
An exact proof term for the current goal is (andEL (nat_p k) (i = ordsucc k) Hkconj).
We prove the intermediate claim Hieq: i = ordsucc k.
An exact proof term for the current goal is (andER (nat_p k) (i = ordsucc k) Hkconj).
We prove the intermediate claim H0in: 0 ∈ i.
rewrite the current goal using Hieq (from left to right).
An exact proof term for the current goal is (nat_0_in_ordsucc k HkNat).
rewrite the current goal using (If_i_1 (0 ∈ i) 0 r H0in) (from left to right).
We prove the intermediate claim Hxcoord0: apply_fun x i = 0.
An exact proof term for the current goal is (Hx0prop i Hi H0in).
rewrite the current goal using Hxcoord0 (from right to left).
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 ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) f HfProd Hpropf).
Assume Hempty: (intersection_of_family X F) ∩ image_of Romega_singleton_map R = Empty.
We will prove False.
We prove the intermediate claim HfBA: f ∈ (intersection_of_family X F) ∩ image_of Romega_singleton_map R.
An exact proof term for the current goal is (binintersectI (intersection_of_family X F) (image_of Romega_singleton_map R) f HfInt HfImg).
We prove the intermediate claim HfE: f ∈ Empty.
We prove the intermediate claim HsubE: (intersection_of_family X F) ∩ image_of Romega_singleton_map R ⊆ 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).
∎