Let X and Tx be given.
Assume HTx: topology_on X Tx.
We will prove (∀A : set, A ⊆ X → first_countable_space X Tx → first_countable_space A (subspace_topology X Tx A)) ∧ (∀A : set, A ⊆ X → second_countable_space X Tx → second_countable_space A (subspace_topology X Tx A)) ∧ (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → first_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → first_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi)) ∧ (∀I Xi : set, countable_index_set I → (∀i : set, i ∈ I → second_countable_space (space_family_set Xi i) (space_family_topology Xi i)) → second_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi)).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let A be given.
Assume HA: A ⊆ X.
Assume Hfc: first_countable_space X Tx.
We will prove first_countable_space A (subspace_topology X Tx A).
We prove the intermediate claim HtopSub: topology_on A (subspace_topology X Tx A).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HA).
We prove the intermediate claim HfcTop: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀x : set, x ∈ X → countable_basis_at X Tx x) Hfc).
We prove the intermediate claim HfcAt: ∀x : set, x ∈ X → countable_basis_at X Tx x.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀x : set, x ∈ X → countable_basis_at X Tx x) Hfc).
We will prove topology_on A (subspace_topology X Tx A) ∧ ∀x : set, x ∈ A → countable_basis_at A (subspace_topology X Tx A) x.
Apply andI to the current goal.
An exact proof term for the current goal is HtopSub.
Let x be given.
Assume HxA: x ∈ A.
We will prove countable_basis_at A (subspace_topology X Tx A) x.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim Hcbx: countable_basis_at X Tx x.
An exact proof term for the current goal is (HfcAt x HxX).
We prove the intermediate claim Hcbx_left: (topology_on X Tx ∧ x ∈ X) ∧ ∃Bx : set, Bx ⊆ Tx ∧ countable_set Bx ∧ (∀b : set, b ∈ Bx → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U).
An exact proof term for the current goal is Hcbx.
We prove the intermediate claim HexBx: ∃Bx : set, Bx ⊆ Tx ∧ countable_set Bx ∧ (∀b : set, b ∈ Bx → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U).
An exact proof term for the current goal is (andER (topology_on X Tx ∧ x ∈ X) (∃Bx : set, Bx ⊆ Tx ∧ countable_set Bx ∧ (∀b : set, b ∈ Bx → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U)) Hcbx_left).
We will prove topology_on A (subspace_topology X Tx A) ∧ x ∈ A ∧ ∃BxA : set, BxA ⊆ subspace_topology X Tx A ∧ countable_set BxA ∧ (∀b : set, b ∈ BxA → x ∈ b) ∧ (∀U0 : set, U0 ∈ subspace_topology X Tx A → x ∈ U0 → ∃b : set, b ∈ BxA ∧ b ⊆ U0).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HtopSub.
An exact proof term for the current goal is HxA.
Apply HexBx to the current goal.
Let Bx be given.
Assume HBxpair.
We prove the intermediate claim Htmp1: (Bx ⊆ Tx ∧ countable_set Bx) ∧ (∀b : set, b ∈ Bx → x ∈ b).
An exact proof term for the current goal is (andEL ((Bx ⊆ Tx ∧ countable_set Bx) ∧ (∀b : set, b ∈ Bx → x ∈ b)) (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U) HBxpair).
We prove the intermediate claim HBxref: ∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U.
An exact proof term for the current goal is (andER ((Bx ⊆ Tx ∧ countable_set Bx) ∧ (∀b : set, b ∈ Bx → x ∈ b)) (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ Bx ∧ b ⊆ U) HBxpair).
We prove the intermediate claim Htmp2: Bx ⊆ Tx ∧ countable_set Bx.
An exact proof term for the current goal is (andEL (Bx ⊆ Tx ∧ countable_set Bx) (∀b : set, b ∈ Bx → x ∈ b) Htmp1).
We prove the intermediate claim HBxmem: ∀b : set, b ∈ Bx → x ∈ b.
An exact proof term for the current goal is (andER (Bx ⊆ Tx ∧ countable_set Bx) (∀b : set, b ∈ Bx → x ∈ b) Htmp1).
We prove the intermediate claim HBxsub: Bx ⊆ Tx.
An exact proof term for the current goal is (andEL (Bx ⊆ Tx) (countable_set Bx) Htmp2).
We prove the intermediate claim HBxcount: countable_set Bx.
An exact proof term for the current goal is (andER (Bx ⊆ Tx) (countable_set Bx) Htmp2).
Set BxA to be the term {b ∩ A|b ∈ Bx}.
We use BxA to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We will prove BxA ⊆ subspace_topology X Tx A.
Let c be given.
Assume Hc: c ∈ BxA.
We will prove c ∈ subspace_topology X Tx A.
Apply (ReplE_impred Bx (λb0 : set ⇒ b0 ∩ A) c Hc) to the current goal.
Let b be given.
Assume HbBx: b ∈ Bx.
Assume Hceq: c = b ∩ A.
We prove the intermediate claim HbTx: b ∈ Tx.
An exact proof term for the current goal is (HBxsub b HbBx).
We prove the intermediate claim HcPowA: c ∈ 𝒫 A.
Apply PowerI A c to the current goal.
Let y be given.
Assume Hyc: y ∈ c.
We prove the intermediate claim HybA: y ∈ b ∩ A.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is Hyc.
An exact proof term for the current goal is (binintersectE2 b A y HybA).
We prove the intermediate claim HcProp: ∃V ∈ Tx, c = V ∩ A.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbTx.
An exact proof term for the current goal is Hceq.
An exact proof term for the current goal is (SepI (𝒫 A) (λU0 : set ⇒ ∃V ∈ Tx, U0 = V ∩ A) c HcPowA HcProp).
An exact proof term for the current goal is (countable_image Bx HBxcount (λb0 : set ⇒ b0 ∩ A)).
Let c be given.
Assume Hc: c ∈ BxA.
We will prove x ∈ c.
Apply (ReplE_impred Bx (λb0 : set ⇒ b0 ∩ A) c Hc) to the current goal.
Let b be given.
Assume HbBx: b ∈ Bx.
Assume Hceq: c = b ∩ A.
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (HBxmem b HbBx).
We prove the intermediate claim HxBA: x ∈ b ∩ A.
An exact proof term for the current goal is (binintersectI b A x Hxb HxA).
rewrite the current goal using Hceq (from left to right).
An exact proof term for the current goal is HxBA.
Let U0 be given.
Assume HU0: U0 ∈ subspace_topology X Tx A.
Assume HxU0: x ∈ U0.
We prove the intermediate claim HU0prop: ∃V ∈ Tx, U0 = V ∩ A.
An exact proof term for the current goal is (SepE2 (𝒫 A) (λU1 : set ⇒ ∃V ∈ Tx, U1 = V ∩ A) U0 HU0).
Apply HU0prop to the current goal.
Let V be given.
Assume HVpair.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (andEL (V ∈ Tx) (U0 = V ∩ A) HVpair).
We prove the intermediate claim HU0eq: U0 = V ∩ A.
An exact proof term for the current goal is (andER (V ∈ Tx) (U0 = V ∩ A) HVpair).
We prove the intermediate claim HxVA: x ∈ V ∩ A.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HxU0.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE1 V A x HxVA).
We prove the intermediate claim Hexb: ∃b : set, b ∈ Bx ∧ b ⊆ V.
An exact proof term for the current goal is (HBxref V HVTx HxV).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair3.
We prove the intermediate claim HbBx: b ∈ Bx.
An exact proof term for the current goal is (andEL (b ∈ Bx) (b ⊆ V) Hbpair3).
We prove the intermediate claim HbsubV: b ⊆ V.
An exact proof term for the current goal is (andER (b ∈ Bx) (b ⊆ V) Hbpair3).
Set c to be the term b ∩ A.
We use c to witness the existential quantifier.
Apply andI to the current goal.
We will prove c ∈ BxA.
An exact proof term for the current goal is (ReplI Bx (λb0 : set ⇒ b0 ∩ A) b HbBx).
We will prove c ⊆ U0.
Let y be given.
Assume Hyc: y ∈ c.
We prove the intermediate claim Hyb: y ∈ b.
An exact proof term for the current goal is (binintersectE1 b A y Hyc).
We prove the intermediate claim HyA: y ∈ A.
An exact proof term for the current goal is (binintersectE2 b A y Hyc).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (HbsubV y Hyb).
We prove the intermediate claim HyVA: y ∈ V ∩ A.
An exact proof term for the current goal is (binintersectI V A y HyV HyA).
rewrite the current goal using HU0eq (from left to right).
An exact proof term for the current goal is HyVA.
Let A be given.
Assume HA: A ⊆ X.
Assume Hsc: second_countable_space X Tx.
We will prove second_countable_space A (subspace_topology X Tx A).
We prove the intermediate claim HtopSub: topology_on A (subspace_topology X Tx A).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HA).
We prove the intermediate claim HexB: ∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx.
An exact proof term for the current goal is (andER (topology_on X Tx) (∃B : set, basis_on X B ∧ countable_set B ∧ basis_generates X B Tx) Hsc).
Apply HexB to the current goal.
Let B be given.
Assume HBpair.
We prove the intermediate claim HBmid: (basis_on X B ∧ countable_set B) ∧ basis_generates X B Tx.
An exact proof term for the current goal is HBpair.
We prove the intermediate claim HBasisCount: basis_on X B ∧ countable_set B.
An exact proof term for the current goal is (andEL (basis_on X B ∧ countable_set B) (basis_generates X B Tx) HBmid).
We prove the intermediate claim HBgener: basis_generates X B Tx.
An exact proof term for the current goal is (andER (basis_on X B ∧ countable_set B) (basis_generates X B Tx) HBmid).
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (andEL (basis_on X B) (countable_set B) HBasisCount).
We prove the intermediate claim HBcount: countable_set B.
An exact proof term for the current goal is (andER (basis_on X B) (countable_set B) HBasisCount).
We prove the intermediate claim HgenEq: generated_topology X B = Tx.
An exact proof term for the current goal is (andER (basis_on X B) (generated_topology X B = Tx) HBgener).
We prove the intermediate claim HBgen: basis_on X B ∧ generated_topology X B = Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HBasis.
An exact proof term for the current goal is HgenEq.
We prove the intermediate claim HsubB: basis_on A {b ∩ A|b ∈ B} ∧ generated_topology A {b ∩ A|b ∈ B} = subspace_topology X Tx A.
An exact proof term for the current goal is (subspace_basis X Tx A B HTx HA HBgen).
We prove the intermediate claim HBsubA: basis_on A {b ∩ A|b ∈ B}.
An exact proof term for the current goal is (andEL (basis_on A {b ∩ A|b ∈ B}) (generated_topology A {b ∩ A|b ∈ B} = subspace_topology X Tx A) HsubB).
We prove the intermediate claim HgenSubEq: generated_topology A {b ∩ A|b ∈ B} = subspace_topology X Tx A.
An exact proof term for the current goal is (andER (basis_on A {b ∩ A|b ∈ B}) (generated_topology A {b ∩ A|b ∈ B} = subspace_topology X Tx A) HsubB).
We will prove topology_on A (subspace_topology X Tx A) ∧ ∃B0 : set, basis_on A B0 ∧ countable_set B0 ∧ basis_generates A B0 (subspace_topology X Tx A).
Apply andI to the current goal.
An exact proof term for the current goal is HtopSub.
We use {b ∩ A|b ∈ B} 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 HBsubA.
An exact proof term for the current goal is (countable_image B HBcount (λb0 : set ⇒ b0 ∩ A)).
We will prove basis_on A {b ∩ A|b ∈ B} ∧ generated_topology A {b ∩ A|b ∈ B} = subspace_topology X Tx A.
Apply andI to the current goal.
An exact proof term for the current goal is HBsubA.
An exact proof term for the current goal is HgenSubEq.
Let I and Xi be given.
Assume HIcount: countable_index_set I.
Assume Hcomp: ∀i : set, i ∈ I → first_countable_space (space_family_set Xi i) (space_family_topology Xi i).
We will prove first_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi).
We will prove topology_on (countable_product_space I Xi) (countable_product_topology_subbasis I Xi) ∧ ∀f : set, f ∈ countable_product_space I Xi → countable_basis_at (countable_product_space I Xi) (countable_product_topology_subbasis I Xi) f.
Apply andI to the current goal.
Apply (xm (I = Empty)) to the current goal.
Assume HI0: I = Empty.
rewrite the current goal using HI0 (from left to right).
An exact proof term for the current goal is (countable_product_topology_subbasis_empty_is_topology Xi).
Assume HIn0: ¬ (I = Empty).
We prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiI: i ∈ I.
An exact proof term for the current goal is (andEL (topology_on (space_family_set Xi i) (space_family_topology Xi i)) (∀x : set, x ∈ space_family_set Xi i → countable_basis_at (space_family_set Xi i) (space_family_topology Xi i) x) (Hcomp i HiI)).
We prove the intermediate claim HS: subbasis_on (product_space I Xi) (product_subbasis_full I Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIn0 HcompTop).
We prove the intermediate claim HB: basis_on (product_space I Xi) (basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi)).
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi) HS).
An exact proof term for the current goal is (lemma_topology_from_basis (product_space I Xi) (basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi)) HB).
Let f be given.
Assume Hf: f ∈ countable_product_space I Xi.
We will prove countable_basis_at (countable_product_space I Xi) (countable_product_topology_subbasis I Xi) f.
Apply (xm (I = Empty)) to the current goal.
Assume HI0: I = Empty.
We prove the intermediate claim Hf0: f ∈ product_space Empty Xi.
rewrite the current goal using HI0 (from right to left).
An exact proof term for the current goal is Hf.
rewrite the current goal using HI0 (from left to right).
We will prove countable_basis_at (product_space Empty Xi) (countable_product_topology_subbasis Empty Xi) f.
We prove the intermediate claim HT0: topology_on (product_space Empty Xi) (countable_product_topology_subbasis Empty Xi).
An exact proof term for the current goal is (countable_product_topology_subbasis_empty_is_topology Xi).
We will prove topology_on (product_space Empty Xi) (countable_product_topology_subbasis Empty Xi) ∧ f ∈ product_space Empty Xi ∧ ∃B : set, B ⊆ countable_product_topology_subbasis Empty Xi ∧ countable_set B ∧ (∀b : set, b ∈ B → f ∈ b) ∧ (∀U : set, U ∈ countable_product_topology_subbasis Empty Xi → f ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HT0.
An exact proof term for the current goal is Hf0.
We use (Sing (product_space Empty Xi)) to witness the existential quantifier.
We will prove ((Sing (product_space Empty Xi) ⊆ countable_product_topology_subbasis Empty Xi ∧ countable_set (Sing (product_space Empty Xi))) ∧ (∀b : set, b ∈ Sing (product_space Empty Xi) → f ∈ b)) ∧ (∀U : set, U ∈ countable_product_topology_subbasis Empty Xi → f ∈ U → ∃b : set, b ∈ Sing (product_space Empty Xi) ∧ b ⊆ U).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let b be given.
Assume Hb: b ∈ Sing (product_space Empty Xi).
We will prove b ∈ countable_product_topology_subbasis Empty Xi.
We prove the intermediate claim HbX0: b = product_space Empty Xi.
An exact proof term for the current goal is (SingE (product_space Empty Xi) b Hb).
rewrite the current goal using HbX0 (from left to right).
An exact proof term for the current goal is (topology_has_X (product_space Empty Xi) (countable_product_topology_subbasis Empty Xi) HT0).
An exact proof term for the current goal is (finite_countable (Sing (product_space Empty Xi)) (Sing_finite (product_space Empty Xi))).
Let b be given.
Assume Hb: b ∈ Sing (product_space Empty Xi).
We will prove f ∈ b.
We prove the intermediate claim HbX0: b = product_space Empty Xi.
An exact proof term for the current goal is (SingE (product_space Empty Xi) b Hb).
rewrite the current goal using HbX0 (from left to right).
An exact proof term for the current goal is Hf0.
Let U be given.
Assume HU: U ∈ countable_product_topology_subbasis Empty Xi.
Assume HfU: f ∈ U.
We will prove ∃b : set, b ∈ Sing (product_space Empty Xi) ∧ b ⊆ U.
We use (product_space Empty Xi) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (SingI (product_space Empty Xi)).
We prove the intermediate claim HX0eq: product_space Empty Xi = {Empty}.
An exact proof term for the current goal is (product_space_empty_index Xi).
We prove the intermediate claim Hf0eq: f = Empty.
Apply (SingE Empty f) to the current goal.
rewrite the current goal using HX0eq (from right to left).
An exact proof term for the current goal is Hf0.
Let y be given.
Assume HyX0: y ∈ product_space Empty Xi.
We will prove y ∈ U.
We prove the intermediate claim Hy0: y = Empty.
Apply (SingE Empty y) to the current goal.
rewrite the current goal using HX0eq (from right to left).
An exact proof term for the current goal is HyX0.
rewrite the current goal using Hy0 (from left to right).
rewrite the current goal using Hf0eq (from right to left).
An exact proof term for the current goal is HfU.
Assume HIn0: ¬ (I = Empty).
We will prove countable_basis_at (countable_product_space I Xi) (countable_product_topology_subbasis I Xi) f.
We prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiI: i ∈ I.
An exact proof term for the current goal is (andEL (topology_on (space_family_set Xi i) (space_family_topology Xi i)) (∀x : set, x ∈ space_family_set Xi i → countable_basis_at (space_family_set Xi i) (space_family_topology Xi i) x) (Hcomp i HiI)).
We prove the intermediate claim HS: subbasis_on (product_space I Xi) (product_subbasis_full I Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIn0 HcompTop).
We prove the intermediate claim HB: basis_on (product_space I Xi) (basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi)).
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi) HS).
We prove the intermediate claim HTprod: topology_on (product_space I Xi) (countable_product_topology_subbasis I Xi).
An exact proof term for the current goal is (lemma_topology_from_basis (product_space I Xi) (basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi)) HB).
We will prove topology_on (product_space I Xi) (countable_product_topology_subbasis I Xi) ∧ f ∈ product_space I Xi ∧ ∃B : set, B ⊆ countable_product_topology_subbasis I Xi ∧ countable_set B ∧ (∀b : set, b ∈ B → f ∈ b) ∧ (∀U : set, U ∈ countable_product_topology_subbasis I Xi → f ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U).
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTprod.
An exact proof term for the current goal is Hf.
We prove the intermediate claim Hcb: countable_basis_at (product_space I Xi) (countable_product_topology_subbasis I Xi) f.
An exact proof term for the current goal is (product_countable_basis_at_point_if_components_first_countable I Xi f HIcount HIn0 Hcomp Hf).
An exact proof term for the current goal is (andER (topology_on (product_space I Xi) (countable_product_topology_subbasis I Xi) ∧ f ∈ product_space I Xi) (∃B : set, B ⊆ countable_product_topology_subbasis I Xi ∧ countable_set B ∧ (∀b : set, b ∈ B → f ∈ b) ∧ (∀U : set, U ∈ countable_product_topology_subbasis I Xi → f ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U)) Hcb).
Let I and Xi be given.
Assume HIcount: countable_index_set I.
Assume Hcomp: ∀i : set, i ∈ I → second_countable_space (space_family_set Xi i) (space_family_topology Xi i).
We will prove second_countable_space (countable_product_space I Xi) (countable_product_topology_subbasis I Xi).
We will prove topology_on (countable_product_space I Xi) (countable_product_topology_subbasis I Xi) ∧ ∃B : set, basis_on (countable_product_space I Xi) B ∧ countable_set B ∧ basis_generates (countable_product_space I Xi) B (countable_product_topology_subbasis I Xi).
Apply andI to the current goal.
Apply (xm (I = Empty)) to the current goal.
Assume HI0: I = Empty.
rewrite the current goal using HI0 (from left to right).
An exact proof term for the current goal is (countable_product_topology_subbasis_empty_is_topology Xi).
Assume HIn0: ¬ (I = Empty).
We prove the intermediate claim HcompTop: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiI: i ∈ I.
An exact proof term for the current goal is (andEL (topology_on (space_family_set Xi i) (space_family_topology Xi i)) (∃B0 : set, basis_on (space_family_set Xi i) B0 ∧ countable_set B0 ∧ basis_generates (space_family_set Xi i) B0 (space_family_topology Xi i)) (Hcomp i HiI)).
We prove the intermediate claim HS: subbasis_on (product_space I Xi) (product_subbasis_full I Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIn0 HcompTop).
We prove the intermediate claim HB: basis_on (product_space I Xi) (basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi)).
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi) HS).
An exact proof term for the current goal is (lemma_topology_from_basis (product_space I Xi) (basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi)) HB).
Apply (xm (I = Empty)) to the current goal.
Assume HI0: I = Empty.
rewrite the current goal using HI0 (from left to right).
We use (Sing (product_space Empty Xi)) 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 (basis_on_singleton (product_space Empty Xi)).
An exact proof term for the current goal is (finite_countable (Sing (product_space Empty Xi)) (Sing_finite (product_space Empty Xi))).
We will prove basis_on (product_space Empty Xi) {product_space Empty Xi} ∧ generated_topology (product_space Empty Xi) {product_space Empty Xi} = countable_product_topology_subbasis Empty Xi.
Apply andI to the current goal.
An exact proof term for the current goal is (basis_on_singleton (product_space Empty Xi)).
We prove the intermediate claim HTdef: countable_product_topology_subbasis Empty Xi = generated_topology_from_subbasis (product_space Empty Xi) (product_subbasis_full Empty Xi).
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We prove the intermediate claim HS0: product_subbasis_full Empty Xi = Empty.
An exact proof term for the current goal is (famunion_Empty (λi : set ⇒ {product_cylinder Empty Xi i U|U ∈ space_family_topology Xi i})).
rewrite the current goal using HS0 (from left to right).
We prove the intermediate claim HGTS0: generated_topology_from_subbasis (product_space Empty Xi) Empty = generated_topology (product_space Empty Xi) (basis_of_subbasis (product_space Empty Xi) Empty).
Use reflexivity.
rewrite the current goal using HGTS0 (from left to right).
We prove the intermediate claim HX0ne: product_space Empty Xi ≠ Empty.
Assume HX0E: product_space Empty Xi = Empty.
We prove the intermediate claim Hem: Empty ∈ product_space Empty Xi.
rewrite the current goal using (product_space_empty_index Xi) (from left to right).
An exact proof term for the current goal is (SingI Empty).
We prove the intermediate claim HemE: Empty ∈ Empty.
rewrite the current goal using HX0E (from right to left) at position 2.
An exact proof term for the current goal is Hem.
An exact proof term for the current goal is (EmptyE Empty HemE False).
We prove the intermediate claim HB0eq: basis_of_subbasis (product_space Empty Xi) Empty = {product_space Empty Xi}.
An exact proof term for the current goal is (basis_of_subbasis_empty_eq (product_space Empty Xi) HX0ne).
rewrite the current goal using HB0eq (from left to right).
Use reflexivity.
Assume HIn0: ¬ (I = Empty).
Set Bsel to be the term λi ⇒ Eps_i (λB0 : set ⇒ basis_on (space_family_set Xi i) B0 ∧ countable_set B0 ∧ basis_generates (space_family_set Xi i) B0 (space_family_topology Xi i)) of type set → set.
Set Ssmall to be the term ⋃i ∈ I{product_cylinder I Xi i U|U ∈ Bsel i} of type set.
We prove the intermediate claim HBsel: ∀i : set, i ∈ I → basis_on (space_family_set Xi i) (Bsel i) ∧ countable_set (Bsel i) ∧ basis_generates (space_family_set Xi i) (Bsel i) (space_family_topology Xi i).
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim HexB0: ∃B0 : set, basis_on (space_family_set Xi i) B0 ∧ countable_set B0 ∧ basis_generates (space_family_set Xi i) B0 (space_family_topology Xi i).
An exact proof term for the current goal is (andER (topology_on (space_family_set Xi i) (space_family_topology Xi i)) (∃B0 : set, basis_on (space_family_set Xi i) B0 ∧ countable_set B0 ∧ basis_generates (space_family_set Xi i) B0 (space_family_topology Xi i)) (Hcomp i HiI)).
Apply HexB0 to the current goal.
Let B0 be given.
Assume HB0: basis_on (space_family_set Xi i) B0 ∧ countable_set B0 ∧ basis_generates (space_family_set Xi i) B0 (space_family_topology Xi i).
An exact proof term for the current goal is (Eps_i_ax (λB1 : set ⇒ basis_on (space_family_set Xi i) B1 ∧ countable_set B1 ∧ basis_generates (space_family_set Xi i) B1 (space_family_topology Xi i)) B0 HB0).
We prove the intermediate claim HSsmall: subbasis_on (product_space I Xi) Ssmall.
We will prove Ssmall ⊆ 𝒫 (product_space I Xi) ∧ ⋃ Ssmall = product_space I Xi.
Apply andI to the current goal.
Let s be given.
Assume Hs: s ∈ Ssmall.
We will prove s ∈ 𝒫 (product_space I Xi).
Apply (famunionE_impred I (λi0 : set ⇒ {product_cylinder I Xi i0 U|U ∈ Bsel i0}) s Hs) to the current goal.
Let i0 be given.
Assume Hi0I.
Assume HsFi0: s ∈ {product_cylinder I Xi i0 U|U ∈ Bsel i0}.
Apply (ReplE_impred (Bsel i0) (λU0 : set ⇒ product_cylinder I Xi i0 U0) s HsFi0) to the current goal.
Let U0 be given.
Assume HU0B: U0 ∈ Bsel i0.
Assume HsEq: s = product_cylinder I Xi i0 U0.
rewrite the current goal using HsEq (from left to right).
Apply PowerI to the current goal.
Let f0 be given.
Assume Hf0: f0 ∈ product_cylinder I Xi i0 U0.
An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ U0) f0 Hf0).
Apply set_ext to the current goal.
Let f0 be given.
Assume Hf0: f0 ∈ ⋃ Ssmall.
We will prove f0 ∈ product_space I Xi.
Apply UnionE_impred Ssmall f0 Hf0 to the current goal.
Let s be given.
Assume Hf0s: f0 ∈ s.
Assume Hs: s ∈ Ssmall.
Apply (famunionE_impred I (λi0 : set ⇒ {product_cylinder I Xi i0 U|U ∈ Bsel i0}) s Hs) to the current goal.
Let i0 be given.
Assume Hi0I.
Assume HsFi0: s ∈ {product_cylinder I Xi i0 U|U ∈ Bsel i0}.
Apply (ReplE_impred (Bsel i0) (λU0 : set ⇒ product_cylinder I Xi i0 U0) s HsFi0) to the current goal.
Let U0 be given.
Assume HU0B: U0 ∈ Bsel i0.
Assume HsEq: s = product_cylinder I Xi i0 U0.
We prove the intermediate claim HsPow: s ∈ 𝒫 (product_space I Xi).
rewrite the current goal using HsEq (from left to right).
Apply PowerI to the current goal.
Let f1 be given.
Assume Hf1: f1 ∈ product_cylinder I Xi i0 U0.
An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf2 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f2 i0 ∈ U0) f1 Hf1).
We prove the intermediate claim HsSub: s ⊆ product_space I Xi.
An exact proof term for the current goal is (PowerE (product_space I Xi) s HsPow).
An exact proof term for the current goal is (HsSub f0 Hf0s).
Let f0 be given.
Assume Hf0: f0 ∈ product_space I Xi.
We will prove f0 ∈ ⋃ Ssmall.
We prove the intermediate claim Hexi: ∃i0 : set, i0 ∈ I.
An exact proof term for the current goal is (nonempty_has_element I HIn0).
Apply Hexi to the current goal.
Let i0 be given.
Assume Hi0I: i0 ∈ I.
We prove the intermediate claim HBsel_i0c: basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0).
An exact proof term for the current goal is (andEL (basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0)) (basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0)) (HBsel i0 Hi0I)).
We prove the intermediate claim HBsel_i0: basis_on (space_family_set Xi i0) (Bsel i0).
An exact proof term for the current goal is (andEL (basis_on (space_family_set Xi i0) (Bsel i0)) (countable_set (Bsel i0)) HBsel_i0c).
We prove the intermediate claim HBcover: ∀x ∈ space_family_set Xi i0, ∃b ∈ Bsel i0, x ∈ b.
An exact proof term for the current goal is (andER (Bsel i0 ⊆ 𝒫 (space_family_set Xi i0)) (∀x ∈ space_family_set Xi i0, ∃b ∈ Bsel i0, x ∈ b) (andEL (Bsel i0 ⊆ 𝒫 (space_family_set Xi i0) ∧ (∀x ∈ space_family_set Xi i0, ∃b ∈ Bsel i0, x ∈ b)) (∀b1 ∈ Bsel i0, ∀b2 ∈ Bsel i0, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ Bsel i0, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBsel_i0)).
We prove the intermediate claim Hf0prop: total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀i : set, i ∈ I → apply_fun f0 i ∈ space_family_set Xi i.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf1 : set ⇒ total_function_on f1 I (space_family_union I Xi) ∧ functional_graph f1 ∧ ∀i : set, i ∈ I → apply_fun f1 i ∈ space_family_set Xi i) f0 Hf0).
We prove the intermediate claim Hcompf0: ∀i : set, i ∈ I → apply_fun f0 i ∈ space_family_set Xi i.
An exact proof term for the current goal is (andER (total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0) (∀i : set, i ∈ I → apply_fun f0 i ∈ space_family_set Xi i) Hf0prop).
We prove the intermediate claim Hfi0: apply_fun f0 i0 ∈ space_family_set Xi i0.
An exact proof term for the current goal is (Hcompf0 i0 Hi0I).
Apply (HBcover (apply_fun f0 i0) Hfi0) to the current goal.
Let U0 be given.
Assume HU0pair.
We prove the intermediate claim HU0B: U0 ∈ Bsel i0.
An exact proof term for the current goal is (andEL (U0 ∈ Bsel i0) (apply_fun f0 i0 ∈ U0) HU0pair).
We prove the intermediate claim Hfi0U0: apply_fun f0 i0 ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ Bsel i0) (apply_fun f0 i0 ∈ U0) HU0pair).
We prove the intermediate claim HBgen_i0: basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0).
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0)) (basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0)) (HBsel i0 Hi0I)).
We prove the intermediate claim HTeq: generated_topology (space_family_set Xi i0) (Bsel i0) = space_family_topology Xi i0.
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i0) (Bsel i0)) (generated_topology (space_family_set Xi i0) (Bsel i0) = space_family_topology Xi i0) HBgen_i0).
We prove the intermediate claim HU0Gen: U0 ∈ generated_topology (space_family_set Xi i0) (Bsel i0).
An exact proof term for the current goal is (generated_topology_contains_basis (space_family_set Xi i0) (Bsel i0) HBsel_i0 U0 HU0B).
We prove the intermediate claim HU0Top: U0 ∈ space_family_topology Xi i0.
rewrite the current goal using HTeq (from right to left).
An exact proof term for the current goal is HU0Gen.
Set C0 to be the term product_cylinder I Xi i0 U0 of type set.
We prove the intermediate claim Hf0C0: f0 ∈ C0.
An exact proof term for the current goal is (SepI (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ U0) f0 Hf0 (andI (i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0) (apply_fun f0 i0 ∈ U0) (andI (i0 ∈ I) (U0 ∈ space_family_topology Xi i0) Hi0I HU0Top) Hfi0U0)).
We prove the intermediate claim HC0in: C0 ∈ Ssmall.
An exact proof term for the current goal is (famunionI I (λi1 : set ⇒ {product_cylinder I Xi i1 U|U ∈ Bsel i1}) i0 C0 Hi0I (ReplI (Bsel i0) (λU : set ⇒ product_cylinder I Xi i0 U) U0 HU0B)).
An exact proof term for the current goal is (UnionI Ssmall f0 C0 Hf0C0 HC0in).
We use (basis_of_subbasis (product_space I Xi) Ssmall) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HS: subbasis_on (product_space I Xi) Ssmall.
An exact proof term for the current goal is HSsmall.
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis (product_space I Xi) Ssmall HS).
We prove the intermediate claim HSsmall_count: countable_set Ssmall.
We prove the intermediate claim HIc: countable I.
An exact proof term for the current goal is HIcount.
We prove the intermediate claim HBsel_count: ∀i : set, i ∈ I → countable (Bsel i).
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim HBi: basis_on (space_family_set Xi i) (Bsel i) ∧ countable_set (Bsel i).
An exact proof term for the current goal is (andEL (basis_on (space_family_set Xi i) (Bsel i) ∧ countable_set (Bsel i)) (basis_generates (space_family_set Xi i) (Bsel i) (space_family_topology Xi i)) (HBsel i HiI)).
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i) (Bsel i)) (countable_set (Bsel i)) HBi).
We prove the intermediate claim HSig: countable (∑i ∈ I, Bsel i).
An exact proof term for the current goal is (Sigma_countable I HIc Bsel HBsel_count).
We prove the intermediate claim HSig_set: countable_set (∑i ∈ I, Bsel i).
An exact proof term for the current goal is HSig.
Set F to be the term λp ⇒ product_cylinder I Xi (p 0) (p 1) of type set → set.
Set Img to be the term {F p|p ∈ ∑i ∈ I, Bsel i}.
We prove the intermediate claim HImg_count: countable_set Img.
An exact proof term for the current goal is (countable_image (∑i ∈ I, Bsel i) HSig_set F).
Apply (Subq_countable Ssmall Img) to the current goal.
An exact proof term for the current goal is HImg_count.
Let s be given.
Assume Hs: s ∈ Ssmall.
We will prove s ∈ Img.
Apply (famunionE_impred I (λi0 : set ⇒ {product_cylinder I Xi i0 U|U ∈ Bsel i0}) s Hs) to the current goal.
Let i0 be given.
Assume Hi0I: i0 ∈ I.
Assume HsFi0: s ∈ {product_cylinder I Xi i0 U|U ∈ Bsel i0}.
Apply (ReplE_impred (Bsel i0) (λU0 : set ⇒ product_cylinder I Xi i0 U0) s HsFi0) to the current goal.
Let U0 be given.
Assume HU0B: U0 ∈ Bsel i0.
Assume HsEq: s = product_cylinder I Xi i0 U0.
We prove the intermediate claim HpSig: (i0,U0) ∈ ∑i ∈ I, Bsel i.
An exact proof term for the current goal is (tuple_2_Sigma I Bsel i0 Hi0I U0 HU0B).
We prove the intermediate claim HFp: F (i0,U0) = product_cylinder I Xi i0 U0.
We prove the intermediate claim HFdef: F (i0,U0) = product_cylinder I Xi ((i0,U0) 0) ((i0,U0) 1).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (tuple_2_0_eq i0 U0) (from left to right).
rewrite the current goal using (tuple_2_1_eq i0 U0) (from left to right).
Use reflexivity.
rewrite the current goal using HsEq (from left to right).
rewrite the current goal using HFp (from right to left).
An exact proof term for the current goal is (ReplI (∑i ∈ I, Bsel i) F (i0,U0) HpSig).
An exact proof term for the current goal is (basis_of_subbasis_countable (product_space I Xi) Ssmall HSsmall_count).
We will prove basis_on (product_space I Xi) (basis_of_subbasis (product_space I Xi) Ssmall) ∧ generated_topology (product_space I Xi) (basis_of_subbasis (product_space I Xi) Ssmall) = countable_product_topology_subbasis I Xi.
Apply andI to the current goal.
We prove the intermediate claim HS: subbasis_on (product_space I Xi) Ssmall.
An exact proof term for the current goal is HSsmall.
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis (product_space I Xi) Ssmall HS).
We prove the intermediate claim HGTSsmall: generated_topology_from_subbasis (product_space I Xi) Ssmall = generated_topology (product_space I Xi) (basis_of_subbasis (product_space I Xi) Ssmall).
Use reflexivity.
rewrite the current goal using HGTSsmall (from right to left).
We prove the intermediate claim HcompTop2: ∀i : set, i ∈ I → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiI: i ∈ I.
An exact proof term for the current goal is (andEL (topology_on (space_family_set Xi i) (space_family_topology Xi i)) (∃B0 : set, basis_on (space_family_set Xi i) B0 ∧ countable_set B0 ∧ basis_generates (space_family_set Xi i) B0 (space_family_topology Xi i)) (Hcomp i HiI)).
We prove the intermediate claim HSfull: subbasis_on (product_space I Xi) (product_subbasis_full I Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIn0 HcompTop2).
We prove the intermediate claim HTdef: countable_product_topology_subbasis I Xi = generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi).
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ generated_topology_from_subbasis (product_space I Xi) Ssmall.
We will prove U ∈ generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi).
We prove the intermediate claim HTfull: topology_on (product_space I Xi) (generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi)).
An exact proof term for the current goal is (topology_from_subbasis_is_topology (product_space I Xi) (product_subbasis_full I Xi) HSfull).
We prove the intermediate claim HBfull: basis_on (product_space I Xi) (basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi)).
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi) HSfull).
We prove the intermediate claim HSsmall_sub_Tfull: Ssmall ⊆ generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi).
Let s be given.
Assume Hs: s ∈ Ssmall.
We will prove s ∈ generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi).
Apply (famunionE_impred I (λi0 : set ⇒ {product_cylinder I Xi i0 U0|U0 ∈ Bsel i0}) s Hs) to the current goal.
Let i0 be given.
Assume Hi0I.
Assume HsFi0: s ∈ {product_cylinder I Xi i0 U0|U0 ∈ Bsel i0}.
Apply (ReplE_impred (Bsel i0) (λU0 : set ⇒ product_cylinder I Xi i0 U0) s HsFi0) to the current goal.
Let U0 be given.
Assume HU0B: U0 ∈ Bsel i0.
Assume HsEq: s = product_cylinder I Xi i0 U0.
We prove the intermediate claim HBsel_i0c: basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0).
An exact proof term for the current goal is (andEL (basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0)) (basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0)) (HBsel i0 Hi0I)).
We prove the intermediate claim HBsel_i0: basis_on (space_family_set Xi i0) (Bsel i0).
An exact proof term for the current goal is (andEL (basis_on (space_family_set Xi i0) (Bsel i0)) (countable_set (Bsel i0)) HBsel_i0c).
We prove the intermediate claim HBgen_i0: basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0).
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0)) (basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0)) (HBsel i0 Hi0I)).
We prove the intermediate claim HTeq_i0: generated_topology (space_family_set Xi i0) (Bsel i0) = space_family_topology Xi i0.
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i0) (Bsel i0)) (generated_topology (space_family_set Xi i0) (Bsel i0) = space_family_topology Xi i0) HBgen_i0).
We prove the intermediate claim HU0Gen: U0 ∈ generated_topology (space_family_set Xi i0) (Bsel i0).
An exact proof term for the current goal is (generated_topology_contains_basis (space_family_set Xi i0) (Bsel i0) HBsel_i0 U0 HU0B).
We prove the intermediate claim HU0Top: U0 ∈ space_family_topology Xi i0.
rewrite the current goal using HTeq_i0 (from right to left).
An exact proof term for the current goal is HU0Gen.
We prove the intermediate claim HsSfull: s ∈ product_subbasis_full I Xi.
rewrite the current goal using HsEq (from left to right).
An exact proof term for the current goal is (famunionI I (λi1 : set ⇒ {product_cylinder I Xi i1 U|U ∈ space_family_topology Xi i1}) i0 (product_cylinder I Xi i0 U0) Hi0I (ReplI (space_family_topology Xi i0) (λU : set ⇒ product_cylinder I Xi i0 U) U0 HU0Top)).
Apply (xm (s = Empty)) to the current goal.
Assume HsE: s = Empty.
rewrite the current goal using HsE (from left to right).
An exact proof term for the current goal is (topology_has_empty (product_space I Xi) (generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi)) HTfull).
Assume HsNE: ¬ (s = Empty).
We prove the intermediate claim HsBasis: s ∈ basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi).
An exact proof term for the current goal is (subbasis_elem_in_basis (product_space I Xi) (product_subbasis_full I Xi) s HSfull HsSfull HsNE).
An exact proof term for the current goal is (basis_in_generated (product_space I Xi) (basis_of_subbasis (product_space I Xi) (product_subbasis_full I Xi)) s HBfull HsBasis).
We prove the intermediate claim Hinc: generated_topology_from_subbasis (product_space I Xi) Ssmall ⊆ generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi).
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal (product_space I Xi) Ssmall (generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi)) HSsmall HTfull HSsmall_sub_Tfull).
An exact proof term for the current goal is (Hinc U HU).
Let U be given.
Assume HU: U ∈ generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi).
We will prove U ∈ generated_topology_from_subbasis (product_space I Xi) Ssmall.
We prove the intermediate claim HTsmall: topology_on (product_space I Xi) (generated_topology_from_subbasis (product_space I Xi) Ssmall).
An exact proof term for the current goal is (topology_from_subbasis_is_topology (product_space I Xi) Ssmall HSsmall).
We prove the intermediate claim HSfull_sub_Tsmall: product_subbasis_full I Xi ⊆ generated_topology_from_subbasis (product_space I Xi) Ssmall.
Let s be given.
Assume HsSfull: s ∈ product_subbasis_full I Xi.
We will prove s ∈ generated_topology_from_subbasis (product_space I Xi) Ssmall.
Set Bsm to be the term basis_of_subbasis (product_space I Xi) Ssmall.
We prove the intermediate claim HBsmBasis: basis_on (product_space I Xi) Bsm.
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis (product_space I Xi) Ssmall HSsmall).
We prove the intermediate claim HGTS: generated_topology_from_subbasis (product_space I Xi) Ssmall = generated_topology (product_space I Xi) Bsm.
Use reflexivity.
rewrite the current goal using HGTS (from left to right).
Apply (famunionE_impred I (λi0 : set ⇒ {product_cylinder I Xi i0 U0|U0 ∈ space_family_topology Xi i0}) s HsSfull) to the current goal.
Let i0 be given.
Assume Hi0I.
Assume HsFi0: s ∈ {product_cylinder I Xi i0 U0|U0 ∈ space_family_topology Xi i0}.
Apply (ReplE_impred (space_family_topology Xi i0) (λU0 : set ⇒ product_cylinder I Xi i0 U0) s HsFi0) to the current goal.
Let U0 be given.
Assume HU0Top: U0 ∈ space_family_topology Xi i0.
Assume HsEq: s = product_cylinder I Xi i0 U0.
We prove the intermediate claim HBsel_i0c: basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0).
An exact proof term for the current goal is (andEL (basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0)) (basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0)) (HBsel i0 Hi0I)).
We prove the intermediate claim HBsel_i0: basis_on (space_family_set Xi i0) (Bsel i0).
An exact proof term for the current goal is (andEL (basis_on (space_family_set Xi i0) (Bsel i0)) (countable_set (Bsel i0)) HBsel_i0c).
We prove the intermediate claim HBgen_i0: basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0).
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0)) (basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0)) (HBsel i0 Hi0I)).
We prove the intermediate claim HTeq_i0: generated_topology (space_family_set Xi i0) (Bsel i0) = space_family_topology Xi i0.
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i0) (Bsel i0)) (generated_topology (space_family_set Xi i0) (Bsel i0) = space_family_topology Xi i0) HBgen_i0).
We prove the intermediate claim HU0Gen: U0 ∈ generated_topology (space_family_set Xi i0) (Bsel i0).
rewrite the current goal using HTeq_i0 (from left to right).
An exact proof term for the current goal is HU0Top.
We prove the intermediate claim HTgen: topology_on (space_family_set Xi i0) (generated_topology (space_family_set Xi i0) (Bsel i0)).
An exact proof term for the current goal is (lemma_topology_from_basis (space_family_set Xi i0) (Bsel i0) HBsel_i0).
We prove the intermediate claim HU0open: open_in (space_family_set Xi i0) (generated_topology (space_family_set Xi i0) (Bsel i0)) U0.
An exact proof term for the current goal is (andI (topology_on (space_family_set Xi i0) (generated_topology (space_family_set Xi i0) (Bsel i0))) (U0 ∈ generated_topology (space_family_set Xi i0) (Bsel i0)) HTgen HU0Gen).
We prove the intermediate claim HexFam: ∃Fam ∈ 𝒫 (Bsel i0), ⋃ Fam = U0.
An exact proof term for the current goal is (open_sets_as_unions_of_basis (space_family_set Xi i0) (Bsel i0) HBsel_i0 U0 HU0open).
Apply HexFam to the current goal.
Let Fam be given.
Assume HFampair.
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 (Bsel i0).
An exact proof term for the current goal is (andEL (Fam ∈ 𝒫 (Bsel i0)) (⋃ Fam = U0) HFampair).
We prove the intermediate claim HUnionFam: ⋃ Fam = U0.
An exact proof term for the current goal is (andER (Fam ∈ 𝒫 (Bsel i0)) (⋃ Fam = U0) HFampair).
We prove the intermediate claim HFamSub: Fam ⊆ Bsel i0.
An exact proof term for the current goal is (PowerE (Bsel i0) Fam HFamPow).
Set FamCyl to be the term {product_cylinder I Xi i0 V|V ∈ Fam}.
We prove the intermediate claim HUnionCyl: ⋃ FamCyl = product_cylinder I Xi i0 U0.
Apply set_ext to the current goal.
Let f be given.
Assume HfU: f ∈ ⋃ FamCyl.
We will prove f ∈ product_cylinder I Xi i0 U0.
Apply (UnionE_impred FamCyl f HfU) to the current goal.
Let c be given.
Assume Hfc: f ∈ c.
Assume Hc: c ∈ FamCyl.
Apply (ReplE_impred Fam (λV0 : set ⇒ product_cylinder I Xi i0 V0) c Hc) to the current goal.
Let V0 be given.
Assume HV0Fam: V0 ∈ Fam.
Assume HcEq: c = product_cylinder I Xi i0 V0.
We prove the intermediate claim HV0B: V0 ∈ Bsel i0.
An exact proof term for the current goal is (HFamSub V0 HV0Fam).
We prove the intermediate claim HV0subU0: V0 ⊆ U0.
Let x be given.
Assume HxV0: x ∈ V0.
We prove the intermediate claim HxUF: x ∈ ⋃ Fam.
An exact proof term for the current goal is (UnionI Fam x V0 HxV0 HV0Fam).
rewrite the current goal using HUnionFam (from right to left).
An exact proof term for the current goal is HxUF.
We prove the intermediate claim HfCylV0: f ∈ product_cylinder I Xi i0 V0.
rewrite the current goal using HcEq (from right to left).
An exact proof term for the current goal is Hfc.
We prove the intermediate claim HfX: f ∈ product_space I Xi.
An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ V0) f HfCylV0).
We prove the intermediate claim Hfcond: (i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0) ∧ apply_fun f i0 ∈ V0.
An exact proof term for the current goal is (SepE2 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ V0) f HfCylV0).
We prove the intermediate claim Hfi0V0: apply_fun f i0 ∈ V0.
An exact proof term for the current goal is (andER (i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0) (apply_fun f i0 ∈ V0) Hfcond).
We prove the intermediate claim Hfi0U0: apply_fun f i0 ∈ U0.
An exact proof term for the current goal is (HV0subU0 (apply_fun f i0) Hfi0V0).
We prove the intermediate claim HpredU0: (i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0) ∧ apply_fun f i0 ∈ U0.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0I.
An exact proof term for the current goal is HU0Top.
An exact proof term for the current goal is Hfi0U0.
An exact proof term for the current goal is (SepI (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ U0) f HfX HpredU0).
Let f be given.
Assume HfC: f ∈ product_cylinder I Xi i0 U0.
We will prove f ∈ ⋃ FamCyl.
We prove the intermediate claim Hfcond: (i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0) ∧ apply_fun f i0 ∈ U0.
An exact proof term for the current goal is (SepE2 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ U0) f HfC).
We prove the intermediate claim Hfi0U0: apply_fun f i0 ∈ U0.
An exact proof term for the current goal is (andER (i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0) (apply_fun f i0 ∈ U0) Hfcond).
We prove the intermediate claim Hfi0UF: apply_fun f i0 ∈ ⋃ Fam.
rewrite the current goal using HUnionFam (from left to right).
An exact proof term for the current goal is Hfi0U0.
Apply (UnionE_impred Fam (apply_fun f i0) Hfi0UF) to the current goal.
Let V0 be given.
Assume Hfi0V0: apply_fun f i0 ∈ V0.
Assume HV0Fam: V0 ∈ Fam.
Set C0 to be the term product_cylinder I Xi i0 V0.
We prove the intermediate claim HC0Fam: C0 ∈ FamCyl.
An exact proof term for the current goal is (ReplI Fam (λV1 : set ⇒ product_cylinder I Xi i0 V1) V0 HV0Fam).
We prove the intermediate claim HfC0: f ∈ C0.
We prove the intermediate claim HfX: f ∈ product_space I Xi.
An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ U0) f HfC).
We prove the intermediate claim HV0B: V0 ∈ Bsel i0.
An exact proof term for the current goal is (HFamSub V0 HV0Fam).
We prove the intermediate claim HBgen_i0T: basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0).
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i0) (Bsel i0) ∧ countable_set (Bsel i0)) (basis_generates (space_family_set Xi i0) (Bsel i0) (space_family_topology Xi i0)) (HBsel i0 Hi0I)).
We prove the intermediate claim HTeq2: generated_topology (space_family_set Xi i0) (Bsel i0) = space_family_topology Xi i0.
An exact proof term for the current goal is (andER (basis_on (space_family_set Xi i0) (Bsel i0)) (generated_topology (space_family_set Xi i0) (Bsel i0) = space_family_topology Xi i0) HBgen_i0T).
We prove the intermediate claim HV0Gen: V0 ∈ generated_topology (space_family_set Xi i0) (Bsel i0).
An exact proof term for the current goal is (generated_topology_contains_basis (space_family_set Xi i0) (Bsel i0) HBsel_i0 V0 HV0B).
We prove the intermediate claim HV0Top: V0 ∈ space_family_topology Xi i0.
rewrite the current goal using HTeq2 (from right to left).
An exact proof term for the current goal is HV0Gen.
We prove the intermediate claim HpredV0: (i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0) ∧ apply_fun f i0 ∈ V0.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0I.
An exact proof term for the current goal is HV0Top.
An exact proof term for the current goal is Hfi0V0.
An exact proof term for the current goal is (SepI (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ V0) f HfX HpredV0).
An exact proof term for the current goal is (UnionI FamCyl f C0 HfC0 HC0Fam).
Set FamCylN to be the term {c ∈ FamCyl|c ≠ Empty}.
We prove the intermediate claim HFamCylNPow: FamCylN ∈ 𝒫 Bsm.
We prove the intermediate claim HFamCylNsub: FamCylN ⊆ Bsm.
Let c be given.
Assume HcN: c ∈ FamCylN.
We will prove c ∈ Bsm.
We prove the intermediate claim HcFam: c ∈ FamCyl.
An exact proof term for the current goal is (SepE1 FamCyl (λc0 : set ⇒ c0 ≠ Empty) c HcN).
We prove the intermediate claim HcNe: c ≠ Empty.
An exact proof term for the current goal is (SepE2 FamCyl (λc0 : set ⇒ c0 ≠ Empty) c HcN).
Apply (ReplE_impred Fam (λV0 : set ⇒ product_cylinder I Xi i0 V0) c HcFam) to the current goal.
Let V0 be given.
Assume HV0Fam: V0 ∈ Fam.
Assume HcEq: c = product_cylinder I Xi i0 V0.
We prove the intermediate claim HV0B: V0 ∈ Bsel i0.
An exact proof term for the current goal is (HFamSub V0 HV0Fam).
We prove the intermediate claim HC0in: product_cylinder I Xi i0 V0 ∈ Ssmall.
An exact proof term for the current goal is (famunionI I (λi1 : set ⇒ {product_cylinder I Xi i1 U|U ∈ Bsel i1}) i0 (product_cylinder I Xi i0 V0) Hi0I (ReplI (Bsel i0) (λU : set ⇒ product_cylinder I Xi i0 U) V0 HV0B)).
We prove the intermediate claim HC0S: c ∈ Ssmall.
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is HC0in.
An exact proof term for the current goal is (subbasis_elem_in_basis (product_space I Xi) Ssmall c HSsmall HC0S HcNe).
An exact proof term for the current goal is (PowerI Bsm FamCylN HFamCylNsub).
We prove the intermediate claim HUnionN: ⋃ FamCylN = ⋃ FamCyl.
Apply set_ext to the current goal.
Let f be given.
Assume HfUN: f ∈ ⋃ FamCylN.
We will prove f ∈ ⋃ FamCyl.
Apply (UnionE_impred FamCylN f HfUN) to the current goal.
Let c be given.
Assume Hfc: f ∈ c.
Assume HcN: c ∈ FamCylN.
We prove the intermediate claim HcFam: c ∈ FamCyl.
An exact proof term for the current goal is (SepE1 FamCyl (λc0 : set ⇒ c0 ≠ Empty) c HcN).
An exact proof term for the current goal is (UnionI FamCyl f c Hfc HcFam).
Let f be given.
Assume HfU: f ∈ ⋃ FamCyl.
We will prove f ∈ ⋃ FamCylN.
Apply (UnionE_impred FamCyl f HfU) to the current goal.
Let c be given.
Assume Hfc: f ∈ c.
Assume HcFam: c ∈ FamCyl.
We prove the intermediate claim HcNe: c ≠ Empty.
Assume HcE: c = Empty.
We prove the intermediate claim Hbad: f ∈ Empty.
rewrite the current goal using HcE (from right to left).
An exact proof term for the current goal is Hfc.
An exact proof term for the current goal is (EmptyE f Hbad False).
We prove the intermediate claim HcN: c ∈ FamCylN.
An exact proof term for the current goal is (SepI FamCyl (λc0 : set ⇒ c0 ≠ Empty) c HcFam HcNe).
An exact proof term for the current goal is (UnionI FamCylN f c Hfc HcN).
We prove the intermediate claim HopenS: open_in (product_space I Xi) (generated_topology (product_space I Xi) Bsm) s.
Apply (basis_generates_open_sets (product_space I Xi) Bsm HBsmBasis s) to the current goal.
We use FamCylN to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HFamCylNPow.
Apply set_ext to the current goal.
Let f be given.
Assume HfU: f ∈ ⋃ FamCylN.
We will prove f ∈ s.
Apply (UnionE_impred FamCylN f HfU) to the current goal.
Let c be given.
Assume Hfc: f ∈ c.
Assume HcN: c ∈ FamCylN.
We prove the intermediate claim HcFam: c ∈ FamCyl.
An exact proof term for the current goal is (SepE1 FamCyl (λc0 : set ⇒ c0 ≠ Empty) c HcN).
Apply (ReplE_impred Fam (λV0 : set ⇒ product_cylinder I Xi i0 V0) c HcFam) to the current goal.
Let V0 be given.
Assume HV0Fam: V0 ∈ Fam.
Assume HcEq: c = product_cylinder I Xi i0 V0.
We prove the intermediate claim HV0subU0: V0 ⊆ U0.
Let x be given.
Assume HxV0: x ∈ V0.
We prove the intermediate claim HxUF: x ∈ ⋃ Fam.
An exact proof term for the current goal is (UnionI Fam x V0 HxV0 HV0Fam).
rewrite the current goal using HUnionFam (from right to left).
An exact proof term for the current goal is HxUF.
We prove the intermediate claim HfCylV0: f ∈ product_cylinder I Xi i0 V0.
rewrite the current goal using HcEq (from right to left).
An exact proof term for the current goal is Hfc.
We prove the intermediate claim HfX: f ∈ product_space I Xi.
An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ V0) f HfCylV0).
We prove the intermediate claim Hfcond: (i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0) ∧ apply_fun f i0 ∈ V0.
An exact proof term for the current goal is (SepE2 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ V0) f HfCylV0).
We prove the intermediate claim Hfi0V0: apply_fun f i0 ∈ V0.
An exact proof term for the current goal is (andER (i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0) (apply_fun f i0 ∈ V0) Hfcond).
We prove the intermediate claim Hfi0U0: apply_fun f i0 ∈ U0.
An exact proof term for the current goal is (HV0subU0 (apply_fun f i0) Hfi0V0).
We prove the intermediate claim HpredU0: (i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0) ∧ apply_fun f i0 ∈ U0.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0I.
An exact proof term for the current goal is HU0Top.
An exact proof term for the current goal is Hfi0U0.
rewrite the current goal using HsEq (from left to right).
An exact proof term for the current goal is (SepI (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ U0) f HfX HpredU0).
Let f be given.
Assume HfS: f ∈ s.
We will prove f ∈ ⋃ FamCylN.
We prove the intermediate claim HfCylU0: f ∈ product_cylinder I Xi i0 U0.
rewrite the current goal using HsEq (from right to left).
An exact proof term for the current goal is HfS.
We prove the intermediate claim Hfcond: (i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0) ∧ apply_fun f i0 ∈ U0.
An exact proof term for the current goal is (SepE2 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ U0) f HfCylU0).
We prove the intermediate claim Hfi0U0: apply_fun f i0 ∈ U0.
An exact proof term for the current goal is (andER (i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0) (apply_fun f i0 ∈ U0) Hfcond).
We prove the intermediate claim Hfi0UF: apply_fun f i0 ∈ ⋃ Fam.
rewrite the current goal using HUnionFam (from left to right).
An exact proof term for the current goal is Hfi0U0.
Apply (UnionE_impred Fam (apply_fun f i0) Hfi0UF) to the current goal.
Let V0 be given.
Assume Hfi0V0: apply_fun f i0 ∈ V0.
Assume HV0Fam: V0 ∈ Fam.
Set C0 to be the term product_cylinder I Xi i0 V0.
We prove the intermediate claim HC0Fam: C0 ∈ FamCyl.
An exact proof term for the current goal is (ReplI Fam (λV1 : set ⇒ product_cylinder I Xi i0 V1) V0 HV0Fam).
We prove the intermediate claim HfC0: f ∈ C0.
We prove the intermediate claim HfX: f ∈ product_space I Xi.
An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ U0) f HfCylU0).
We prove the intermediate claim HpredV0: (i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0) ∧ apply_fun f i0 ∈ V0.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0I.
We prove the intermediate claim HV0B: V0 ∈ Bsel i0.
An exact proof term for the current goal is (HFamSub V0 HV0Fam).
We prove the intermediate claim HV0Gen: V0 ∈ generated_topology (space_family_set Xi i0) (Bsel i0).
An exact proof term for the current goal is (generated_topology_contains_basis (space_family_set Xi i0) (Bsel i0) HBsel_i0 V0 HV0B).
We prove the intermediate claim HV0Top: V0 ∈ space_family_topology Xi i0.
rewrite the current goal using HTeq_i0 (from right to left).
An exact proof term for the current goal is HV0Gen.
An exact proof term for the current goal is HV0Top.
An exact proof term for the current goal is Hfi0V0.
An exact proof term for the current goal is (SepI (product_space I Xi) (λf1 : set ⇒ i0 ∈ I ∧ V0 ∈ space_family_topology Xi i0 ∧ apply_fun f1 i0 ∈ V0) f HfX HpredV0).
We prove the intermediate claim HC0ne: C0 ≠ Empty.
Assume HC0E: C0 = Empty.
We prove the intermediate claim Hbad: f ∈ Empty.
rewrite the current goal using HC0E (from right to left).
An exact proof term for the current goal is HfC0.
An exact proof term for the current goal is (EmptyE f Hbad False).
We prove the intermediate claim HC0N: C0 ∈ FamCylN.
An exact proof term for the current goal is (SepI FamCyl (λc0 : set ⇒ c0 ≠ Empty) C0 HC0Fam HC0ne).
An exact proof term for the current goal is (UnionI FamCylN f C0 HfC0 HC0N).
An exact proof term for the current goal is (andER (topology_on (product_space I Xi) (generated_topology (product_space I Xi) Bsm)) (s ∈ generated_topology (product_space I Xi) Bsm) HopenS).
We prove the intermediate claim Hinc: generated_topology_from_subbasis (product_space I Xi) (product_subbasis_full I Xi) ⊆ generated_topology_from_subbasis (product_space I Xi) Ssmall.
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal (product_space I Xi) (product_subbasis_full I Xi) (generated_topology_from_subbasis (product_space I Xi) Ssmall) HSfull HTsmall HSfull_sub_Tsmall).
An exact proof term for the current goal is (Hinc U HU).
∎