Let s be given.

Assume Hs: s ∈ product_subbasis_full I Xi.

We will prove s ∈ 𝒫 (product_space I Xi).

Apply PowerI to the current goal.

Let f be given.

Assume Hf: f ∈ s.

We will prove f ∈ product_space I Xi.

Set F to be the term (λi : set ⇒ {product_cylinder I Xi i U|U ∈ space_family_topology Xi i}).

We prove the intermediate claim HsF: s ∈ (⋃_{i ∈ I}F i).

An exact proof term for the current goal is Hs.

Apply (famunionE_impred I F s HsF (f ∈ product_space I Xi)) to the current goal.

Let i be given.

Assume HiI: i ∈ I.

Assume HsFi: s ∈ F i.

We prove the intermediate claim HexU: ∃U ∈ space_family_topology Xi i, s = product_cylinder I Xi i U.

An exact proof term for the current goal is (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder I Xi i U0) s HsFi).

Apply HexU to the current goal.

Let U be given.

Assume HUand: U ∈ space_family_topology Xi i ∧ s = product_cylinder I Xi i U.

We prove the intermediate claim Hseq: s = product_cylinder I Xi i U.

An exact proof term for the current goal is (andER (U ∈ space_family_topology Xi i) (s = product_cylinder I Xi i U) HUand).

We prove the intermediate claim HfCyl: f ∈ product_cylinder I Xi i U.

rewrite the current goal using Hseq (from right to left).

An exact proof term for the current goal is Hf.

An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf0 : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) f HfCyl).

Apply set_ext to the current goal.

Let f be given.

Assume HfU: f ∈ ⋃ (product_subbasis_full I Xi).

We will prove f ∈ product_space I Xi.

Apply (UnionE_impred (product_subbasis_full I Xi) f HfU (f ∈ product_space I Xi)) to the current goal.

Let s be given.

Assume Hfs: f ∈ s.

Assume Hs: s ∈ product_subbasis_full I Xi.

We prove the intermediate claim HsPow: s ∈ 𝒫 (product_space I Xi).

Apply PowerI to the current goal.

Let g be given.

Assume Hg: g ∈ s.

We will prove g ∈ product_space I Xi.

Set F to be the term (λi : set ⇒ {product_cylinder I Xi i U|U ∈ space_family_topology Xi i}).

We prove the intermediate claim HsF: s ∈ (⋃_{i ∈ I}F i).

An exact proof term for the current goal is Hs.

Apply (famunionE_impred I F s HsF (g ∈ product_space I Xi)) to the current goal.

Let i be given.

Assume HiI: i ∈ I.

Assume HsFi: s ∈ F i.

We prove the intermediate claim HexU: ∃U ∈ space_family_topology Xi i, s = product_cylinder I Xi i U.

An exact proof term for the current goal is (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder I Xi i U0) s HsFi).

Apply HexU to the current goal.

Let U be given.

Assume HUand: U ∈ space_family_topology Xi i ∧ s = product_cylinder I Xi i U.

We prove the intermediate claim Hseq: s = product_cylinder I Xi i U.

An exact proof term for the current goal is (andER (U ∈ space_family_topology Xi i) (s = product_cylinder I Xi i U) HUand).

We prove the intermediate claim HgCyl: g ∈ product_cylinder I Xi i U.

rewrite the current goal using Hseq (from right to left).

An exact proof term for the current goal is Hg.

An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf0 : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) g HgCyl).

An exact proof term for the current goal is (PowerE (product_space I Xi) s HsPow f Hfs).

Let f be given.

Assume HfX: f ∈ product_space I Xi.

We will prove f ∈ ⋃ (product_subbasis_full I Xi).

Apply (xm (∃i : set, i ∈ I)) to the current goal.

Assume Hexi: ∃i : set, i ∈ I.

Apply Hexi to the current goal.

Let i be given.

Assume HiI: i ∈ I.

We prove the intermediate claim Htopi: topology_on (space_family_set Xi i) (space_family_topology Xi i).

An exact proof term for the current goal is (HcompTop i HiI).

We prove the intermediate claim Ht1: (((space_family_topology Xi i ⊆ 𝒫 (space_family_set Xi i) ∧ Empty ∈ space_family_topology Xi i) ∧ space_family_set Xi i ∈ space_family_topology Xi i) ∧ (∀UFam ∈ 𝒫 (space_family_topology Xi i), ⋃ UFam ∈ space_family_topology Xi i)) ∧ (∀U ∈ space_family_topology Xi i, ∀V ∈ space_family_topology Xi i, U ∩ V ∈ space_family_topology Xi i).

An exact proof term for the current goal is Htopi.

We prove the intermediate claim Ht2: ((space_family_topology Xi i ⊆ 𝒫 (space_family_set Xi i) ∧ Empty ∈ space_family_topology Xi i) ∧ space_family_set Xi i ∈ space_family_topology Xi i) ∧ (∀UFam ∈ 𝒫 (space_family_topology Xi i), ⋃ UFam ∈ space_family_topology Xi i).

An exact proof term for the current goal is (andEL (((space_family_topology Xi i ⊆ 𝒫 (space_family_set Xi i) ∧ Empty ∈ space_family_topology Xi i) ∧ space_family_set Xi i ∈ space_family_topology Xi i) ∧ (∀UFam ∈ 𝒫 (space_family_topology Xi i), ⋃ UFam ∈ space_family_topology Xi i)) (∀U ∈ space_family_topology Xi i, ∀V ∈ space_family_topology Xi i, U ∩ V ∈ space_family_topology Xi i) Ht1).

We prove the intermediate claim Ht3: (space_family_topology Xi i ⊆ 𝒫 (space_family_set Xi i) ∧ Empty ∈ space_family_topology Xi i) ∧ space_family_set Xi i ∈ space_family_topology Xi i.

An exact proof term for the current goal is (andEL ((space_family_topology Xi i ⊆ 𝒫 (space_family_set Xi i) ∧ Empty ∈ space_family_topology Xi i) ∧ space_family_set Xi i ∈ space_family_topology Xi i) (∀UFam ∈ 𝒫 (space_family_topology Xi i), ⋃ UFam ∈ space_family_topology Xi i) Ht2).

We prove the intermediate claim HUopen: space_family_set Xi i ∈ space_family_topology Xi i.

An exact proof term for the current goal is (andER (space_family_topology Xi i ⊆ 𝒫 (space_family_set Xi i) ∧ Empty ∈ space_family_topology Xi i) (space_family_set Xi i ∈ space_family_topology Xi i) Ht3).

Set s to be the term product_cylinder I Xi i (space_family_set Xi i).

We prove the intermediate claim HsRepl: s ∈ {product_cylinder I Xi i U|U ∈ space_family_topology Xi i}.

An exact proof term for the current goal is (ReplI (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder I Xi i U0) (space_family_set Xi i) HUopen).

We prove the intermediate claim HsSub: s ∈ product_subbasis_full I Xi.

An exact proof term for the current goal is (famunionI I (λi0 : set ⇒ {product_cylinder I Xi i0 U|U ∈ space_family_topology Xi i0}) i s HiI HsRepl).

We prove the intermediate claim HfProp: total_function_on f I (space_family_union I Xi) ∧ functional_graph f ∧ ∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀j : set, j ∈ I → apply_fun f0 j ∈ space_family_set Xi j) f HfX).

We prove the intermediate claim HfCoord: ∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j.

An exact proof term for the current goal is (andER (total_function_on f I (space_family_union I Xi) ∧ functional_graph f) (∀j : set, j ∈ I → apply_fun f j ∈ space_family_set Xi j) HfProp).

We prove the intermediate claim Hfi: apply_fun f i ∈ space_family_set Xi i.

An exact proof term for the current goal is (HfCoord i HiI).

We prove the intermediate claim HfInS: f ∈ s.

An exact proof term for the current goal is (SepI (product_space I Xi) (λf0 : set ⇒ i ∈ I ∧ space_family_set Xi i ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ space_family_set Xi i) f HfX (andI (i ∈ I ∧ space_family_set Xi i ∈ space_family_topology Xi i) (apply_fun f i ∈ space_family_set Xi i) (andI (i ∈ I) (space_family_set Xi i ∈ space_family_topology Xi i) HiI HUopen) Hfi)).

An exact proof term for the current goal is (UnionI (product_subbasis_full I Xi) f s HfInS HsSub).

Assume Hnex: ¬ (∃i : set, i ∈ I).

We will prove f ∈ ⋃ (product_subbasis_full I Xi).

We prove the intermediate claim Hall: ∀i : set, i ∉ I.

Let i be given.

Assume HiI: i ∈ I.

We will prove False.

Apply Hnex to the current goal.

We use i to witness the existential quantifier.

An exact proof term for the current goal is HiI.

We prove the intermediate claim HIeq: I = Empty.

An exact proof term for the current goal is (Empty_eq I Hall).

We prove the intermediate claim Hfalse: False.

Apply HIne to the current goal.

An exact proof term for the current goal is HIeq.

An exact proof term for the current goal is (FalseE Hfalse (f ∈ ⋃ (product_subbasis_full I Xi))).