Let X, Tx, Y and Ty be given.
Assume HcrX: completely_regular_space X Tx.
Assume HcrY: completely_regular_space Y Ty.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (completely_regular_space_topology_on X Tx HcrX).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (completely_regular_space_topology_on Y Ty HcrY).
Set X0 to be the term setprod X Y.
Set B0 to be the term product_subbasis X Tx Y Ty.
Set T0 to be the term product_topology X Tx Y Ty.
We prove the intermediate claim HB0: basis_on X0 B0.
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim HT0: topology_on X0 T0.
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
Set I to be the term 2.
Set Xi to be the term graph I (λi : set ⇒ If_i (i = 0) (X,Tx) (Y,Ty)).
Set X1 to be the term product_space I Xi.
Set T1 to be the term product_topology_full I Xi.
We prove the intermediate claim HXi0: apply_fun Xi 0 = (X,Tx).
We prove the intermediate claim H0I: 0 ∈ I.
An exact proof term for the current goal is In_0_2.
rewrite the current goal using (apply_fun_graph I (λi0 : set ⇒ If_i (i0 = 0) (X,Tx) (Y,Ty)) 0 H0I) (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (X,Tx) (Y,Ty) H00) (from left to right).
Use reflexivity.
We prove the intermediate claim HXi1: apply_fun Xi 1 = (Y,Ty).
We prove the intermediate claim H1I: 1 ∈ I.
An exact proof term for the current goal is In_1_2.
rewrite the current goal using (apply_fun_graph I (λi0 : set ⇒ If_i (i0 = 0) (X,Tx) (Y,Ty)) 1 H1I) (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (X,Tx) (Y,Ty) H10) (from left to right).
Use reflexivity.
We prove the intermediate claim HXset0: space_family_set Xi 0 = X.
We prove the intermediate claim Hsf: space_family_set Xi 0 = (apply_fun Xi 0) 0.
Use reflexivity.
rewrite the current goal using Hsf (from left to right).
rewrite the current goal using HXi0 (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq X Tx).
We prove the intermediate claim HXtop0: space_family_topology Xi 0 = Tx.
We prove the intermediate claim Hsf: space_family_topology Xi 0 = (apply_fun Xi 0) 1.
Use reflexivity.
rewrite the current goal using Hsf (from left to right).
rewrite the current goal using HXi0 (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq X Tx).
We prove the intermediate claim HXset1: space_family_set Xi 1 = Y.
We prove the intermediate claim Hsf: space_family_set Xi 1 = (apply_fun Xi 1) 0.
Use reflexivity.
rewrite the current goal using Hsf (from left to right).
rewrite the current goal using HXi1 (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq Y Ty).
We prove the intermediate claim HXtop1: space_family_topology Xi 1 = Ty.
We prove the intermediate claim Hsf: space_family_topology Xi 1 = (apply_fun Xi 1) 1.
Use reflexivity.
rewrite the current goal using Hsf (from left to right).
rewrite the current goal using HXi1 (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq Y Ty).
We prove the intermediate claim HIne: I ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty I 0 In_0_2).
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.
We prove the intermediate claim Hi01: i ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 i HiI).
Apply (UPairE i 0 1 Hi01 (topology_on (space_family_set Xi i) (space_family_topology Xi i))) to the current goal.
Assume Hi0: i = 0.
rewrite the current goal using Hi0 (from left to right).
rewrite the current goal using HXset0 (from left to right).
rewrite the current goal using HXtop0 (from left to right).
An exact proof term for the current goal is HTx.
Assume Hi1: i = 1.
rewrite the current goal using Hi1 (from left to right).
rewrite the current goal using HXset1 (from left to right).
rewrite the current goal using HXtop1 (from left to right).
An exact proof term for the current goal is HTy.
We prove the intermediate claim HSsub: subbasis_on X1 (product_subbasis_full I Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIne HcompTop).
Set pair_fun to be the term graph X0 (λp : set ⇒ graph I (λi : set ⇒ If_i (i = 0) (p 0) (p 1))).
Set fun_pair to be the term graph X1 (λh : set ⇒ (apply_fun h 0,apply_fun h 1)).
We prove the intermediate claim HprodLemma: ∀J Zeta : set, completely_regular_spaces_family J Zeta → completely_regular_space (product_space J Zeta) (product_topology_full J Zeta).
An exact proof term for the current goal is (andER (∀Y0 : set, Y0 ⊆ R → completely_regular_space R R_standard_topology → completely_regular_space Y0 (subspace_topology R R_standard_topology Y0)) (∀I0 Xi0 : set, completely_regular_spaces_family I0 Xi0 → completely_regular_space (product_space I0 Xi0) (product_topology_full I0 Xi0)) (completely_regular_subspace_product R R_standard_topology R_standard_topology_is_topology)).
We prove the intermediate claim Hfam: completely_regular_spaces_family I Xi.
Let i be given.
Assume HiI: i ∈ I.
We prove the intermediate claim Hi01: i ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 i HiI).
Apply (UPairE i 0 1 Hi01 (completely_regular_space (product_component Xi i) (product_component_topology Xi i))) to the current goal.
Assume Hi0: i = 0.
rewrite the current goal using Hi0 (from left to right).
rewrite the current goal using (product_component_def Xi 0) (from left to right).
rewrite the current goal using (product_component_topology_def Xi 0) (from left to right).
rewrite the current goal using HXi0 (from left to right).
rewrite the current goal using (tuple_2_0_eq X Tx) (from left to right).
rewrite the current goal using (tuple_2_1_eq X Tx) (from left to right).
An exact proof term for the current goal is HcrX.
Assume Hi1: i = 1.
rewrite the current goal using Hi1 (from left to right).
rewrite the current goal using (product_component_def Xi 1) (from left to right).
rewrite the current goal using (product_component_topology_def Xi 1) (from left to right).
rewrite the current goal using HXi1 (from left to right).
rewrite the current goal using (tuple_2_0_eq Y Ty) (from left to right).
rewrite the current goal using (tuple_2_1_eq Y Ty) (from left to right).
An exact proof term for the current goal is HcrY.
We prove the intermediate claim HcrX1: completely_regular_space X1 T1.
An exact proof term for the current goal is (HprodLemma I Xi Hfam).
We prove the intermediate claim Hhom: homeomorphism X0 T0 X1 T1 pair_fun.
We will prove continuous_map X0 T0 X1 T1 pair_fun ∧ ∃g : set, continuous_map X1 T1 X0 T0 g ∧ (∀x : set, x ∈ X0 → apply_fun g (apply_fun pair_fun x) = x) ∧ (∀y : set, y ∈ X1 → apply_fun pair_fun (apply_fun g y) = y).
Apply andI to the current goal.
We prove the intermediate claim Hfun_pair_fun: function_on pair_fun X0 X1.
Let p be given.
Assume Hp: p ∈ X0.
We will prove apply_fun pair_fun p ∈ X1.
rewrite the current goal using (apply_fun_graph X0 (λq : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (q 0) (q 1))) p Hp) (from left to right).
Set h to be the term (λi0 : set ⇒ If_i (i0 = 0) (p 0) (p 1)).
We prove the intermediate claim Hhdef: h = (λi0 : set ⇒ If_i (i0 = 0) (p 0) (p 1)).
Use reflexivity.
rewrite the current goal using Hhdef (from right to left).
Set gp to be the term graph I h.
We prove the intermediate claim Hgpdef: gp = graph I h.
Use reflexivity.
rewrite the current goal using Hgpdef (from right to left).
We prove the intermediate claim Hp0X: p 0 ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ Y) p Hp).
We prove the intermediate claim Hp1Y: p 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ Y) p Hp).
We prove the intermediate claim Hhj_union: ∀j : set, j ∈ I → h j ∈ space_family_union I Xi.
Let j be given.
Assume HjI: j ∈ I.
We prove the intermediate claim Hhj_eq: h j = If_i (j = 0) (p 0) (p 1).
Use reflexivity.
We prove the intermediate claim Hj01: j ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 j HjI).
Apply (UPairE j 0 1 Hj01 (h j ∈ space_family_union I Xi)) to the current goal.
Assume Hj0: j = 0.
rewrite the current goal using Hhj_eq (from left to right).
rewrite the current goal using Hj0 (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (p 0) (p 1) H00) (from left to right).
We prove the intermediate claim Hp0sf: p 0 ∈ space_family_set Xi 0.
rewrite the current goal using HXset0 (from left to right).
An exact proof term for the current goal is Hp0X.
An exact proof term for the current goal is (UnionI {space_family_set Xi i0|i0 ∈ I} (p 0) (space_family_set Xi 0) Hp0sf (ReplI I (λi0 : set ⇒ space_family_set Xi i0) 0 In_0_2)).
Assume Hj1: j = 1.
rewrite the current goal using Hhj_eq (from left to right).
rewrite the current goal using Hj1 (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (p 0) (p 1) H10) (from left to right).
We prove the intermediate claim Hp1sf: p 1 ∈ space_family_set Xi 1.
rewrite the current goal using HXset1 (from left to right).
An exact proof term for the current goal is Hp1Y.
An exact proof term for the current goal is (UnionI {space_family_set Xi i0|i0 ∈ I} (p 1) (space_family_set Xi 1) Hp1sf (ReplI I (λi0 : set ⇒ space_family_set Xi i0) 1 In_1_2)).
We prove the intermediate claim Hgp_sub: gp ⊆ setprod I (space_family_union I Xi).
Let z be given.
Assume Hz: z ∈ gp.
Apply (ReplE_impred I (λj0 : set ⇒ (j0,h j0)) z Hz (z ∈ setprod I (space_family_union I Xi))) to the current goal.
Let j be given.
Assume HjI: j ∈ I.
Assume HzEq: z = (j,h j).
rewrite the current goal using HzEq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma I (space_family_union I Xi) j (h j) HjI (Hhj_union j HjI)).
We prove the intermediate claim Hgp_pow: gp ∈ 𝒫 (setprod I (space_family_union I Xi)).
An exact proof term for the current goal is (PowerI (setprod I (space_family_union I Xi)) gp Hgp_sub).
We prove the intermediate claim Hgp_tot: total_function_on gp I (space_family_union I Xi).
Apply (total_function_on_graph I (space_family_union I Xi) h) to the current goal.
An exact proof term for the current goal is Hhj_union.
We prove the intermediate claim Hgp_fun: functional_graph gp.
An exact proof term for the current goal is (functional_graph_graph I h).
We prove the intermediate claim Hcoords: ∀j : set, j ∈ I → apply_fun gp j ∈ space_family_set Xi j.
Let j be given.
Assume HjI: j ∈ I.
rewrite the current goal using (apply_fun_graph I h j HjI) (from left to right).
We prove the intermediate claim Hhj_eq: h j = If_i (j = 0) (p 0) (p 1).
Use reflexivity.
We prove the intermediate claim Hj01: j ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 j HjI).
Apply (UPairE j 0 1 Hj01 (h j ∈ space_family_set Xi j)) to the current goal.
Assume Hj0: j = 0.
rewrite the current goal using Hhj_eq (from left to right).
rewrite the current goal using Hj0 (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (p 0) (p 1) H00) (from left to right).
rewrite the current goal using HXset0 (from left to right).
An exact proof term for the current goal is Hp0X.
Assume Hj1: j = 1.
rewrite the current goal using Hhj_eq (from left to right).
rewrite the current goal using Hj1 (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (p 0) (p 1) H10) (from left to right).
rewrite the current goal using HXset1 (from left to right).
An exact proof term for the current goal is Hp1Y.
We prove the intermediate claim Hpred: total_function_on gp I (space_family_union I Xi) ∧ functional_graph gp ∧ ∀j : set, j ∈ I → apply_fun gp j ∈ space_family_set Xi j.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hgp_tot.
An exact proof term for the current goal is Hgp_fun.
An exact proof term for the current goal is Hcoords.
An exact proof term for the current goal is (SepI (𝒫 (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) gp Hgp_pow Hpred).
Apply (continuous_map_from_subbasis X0 T0 X1 (product_subbasis_full I Xi) pair_fun HT0 Hfun_pair_fun HSsub) to the current goal.
Let s be given.
Assume HsS: s ∈ product_subbasis_full I Xi.
We prove the intermediate claim Hexi: ∃i : set, i ∈ I ∧ s ∈ {product_cylinder I Xi i U|U ∈ space_family_topology Xi i}.
An exact proof term for the current goal is (famunionE I (λi0 : set ⇒ {product_cylinder I Xi i0 U|U ∈ space_family_topology Xi i0}) s HsS).
Apply Hexi to the current goal.
Let i be given.
Assume Hipair.
We prove the intermediate claim HiI: i ∈ I.
An exact proof term for the current goal is (andEL (i ∈ I) (s ∈ {product_cylinder I Xi i U|U ∈ space_family_topology Xi i}) Hipair).
We prove the intermediate claim HsFi: s ∈ {product_cylinder I Xi i U|U ∈ space_family_topology Xi i}.
An exact proof term for the current goal is (andER (i ∈ I) (s ∈ {product_cylinder I Xi i U|U ∈ space_family_topology Xi i}) Hipair).
Apply (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder I Xi i U0) s HsFi) to the current goal.
Let U be given.
Assume HUpair.
We prove the intermediate claim HUin: U ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (U ∈ space_family_topology Xi i) (s = product_cylinder I Xi i U) HUpair).
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) HUpair).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim Hi01: i ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 i HiI).
Apply (UPairE i 0 1 Hi01 (preimage_of X0 pair_fun (product_cylinder I Xi i U) ∈ T0)) to the current goal.
Assume Hi0: i = 0.
rewrite the current goal using Hi0 (from left to right).
We prove the intermediate claim HU0eq: space_family_topology Xi i = space_family_topology Xi 0.
rewrite the current goal using Hi0 (from left to right).
Use reflexivity.
We prove the intermediate claim HU0: U ∈ space_family_topology Xi 0.
rewrite the current goal using HU0eq (from right to left).
An exact proof term for the current goal is HUin.
We prove the intermediate claim HU: U ∈ Tx.
rewrite the current goal using HXtop0 (from right to left).
An exact proof term for the current goal is HU0.
We prove the intermediate claim HTxSub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
An exact proof term for the current goal is (HTxSub U HU).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HUpow).
Set R0 to be the term rectangle_set U Y.
We prove the intermediate claim HYTy: Y ∈ Ty.
An exact proof term for the current goal is (topology_has_X Y Ty HTy).
We prove the intermediate claim HR0inB: R0 ∈ B0.
We prove the intermediate claim HRfam: R0 ∈ {rectangle_set U V|V ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set U V0) Y HYTy).
An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) U R0 HU HRfam).
We prove the intermediate claim Heq0: preimage_of X0 pair_fun (product_cylinder I Xi 0 U) = R0.
Apply set_ext to the current goal.
Let p0 be given.
Assume Hp0: p0 ∈ preimage_of X0 pair_fun (product_cylinder I Xi 0 U).
We will prove p0 ∈ R0.
We prove the intermediate claim Hp0X0: p0 ∈ X0.
An exact proof term for the current goal is (SepE1 X0 (λx0 : set ⇒ apply_fun pair_fun x0 ∈ product_cylinder I Xi 0 U) p0 Hp0).
We prove the intermediate claim Himg: apply_fun pair_fun p0 ∈ product_cylinder I Xi 0 U.
An exact proof term for the current goal is (SepE2 X0 (λx0 : set ⇒ apply_fun pair_fun x0 ∈ product_cylinder I Xi 0 U) p0 Hp0).
We prove the intermediate claim Hconj: 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun (apply_fun pair_fun p0) 0 ∈ U.
An exact proof term for the current goal is (SepE2 (product_space I Xi) (λf0 : set ⇒ 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun f0 0 ∈ U) (apply_fun pair_fun p0) Himg).
We prove the intermediate claim Hthird: apply_fun (apply_fun pair_fun p0) 0 ∈ U.
An exact proof term for the current goal is (andER (0 ∈ I ∧ U ∈ space_family_topology Xi 0) (apply_fun (apply_fun pair_fun p0) 0 ∈ U) Hconj).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun pair_fun p0) 0 = p0 0.
rewrite the current goal using (apply_fun_graph X0 (λq : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (q 0) (q 1))) p0 Hp0X0) (from left to right).
rewrite the current goal using (apply_fun_graph I (λi0 : set ⇒ If_i (i0 = 0) (p0 0) (p0 1)) 0 In_0_2) (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (p0 0) (p0 1) H00) (from left to right).
Use reflexivity.
We prove the intermediate claim Hp00U: p0 0 ∈ U.
rewrite the current goal using HcoordEq (from right to left).
An exact proof term for the current goal is Hthird.
We prove the intermediate claim Hp01Y: p0 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ Y) p0 Hp0X0).
rewrite the current goal using rectangle_set_def (from left to right).
We prove the intermediate claim HpEta: p0 = (p0 0,p0 1).
An exact proof term for the current goal is (setprod_eta X Y p0 Hp0X0).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U Y (p0 0) (p0 1) Hp00U Hp01Y).
Let p0 be given.
Assume Hp0: p0 ∈ R0.
We will prove p0 ∈ preimage_of X0 pair_fun (product_cylinder I Xi 0 U).
We prove the intermediate claim HpUV: p0 ∈ setprod U Y.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is Hp0.
We prove the intermediate claim Hp00U: p0 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ Y) p0 HpUV).
We prove the intermediate claim Hp01Y: p0 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ Y) p0 HpUV).
We prove the intermediate claim Hp00X: p0 0 ∈ X.
An exact proof term for the current goal is (HUsubX (p0 0) Hp00U).
We prove the intermediate claim Hp0X0: p0 ∈ X0.
We prove the intermediate claim HpEta: p0 = (p0 0,p0 1).
An exact proof term for the current goal is (setprod_eta U Y p0 HpUV).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (p0 0) (p0 1) Hp00X Hp01Y).
We prove the intermediate claim HfX1: apply_fun pair_fun p0 ∈ X1.
An exact proof term for the current goal is (Hfun_pair_fun p0 Hp0X0).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun pair_fun p0) 0 = p0 0.
rewrite the current goal using (apply_fun_graph X0 (λq : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (q 0) (q 1))) p0 Hp0X0) (from left to right).
rewrite the current goal using (apply_fun_graph I (λi0 : set ⇒ If_i (i0 = 0) (p0 0) (p0 1)) 0 In_0_2) (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (p0 0) (p0 1) H00) (from left to right).
Use reflexivity.
We prove the intermediate claim Hf0U: apply_fun (apply_fun pair_fun p0) 0 ∈ U.
rewrite the current goal using HcoordEq (from left to right).
An exact proof term for the current goal is Hp00U.
We prove the intermediate claim Hcyl: apply_fun pair_fun p0 ∈ product_cylinder I Xi 0 U.
We prove the intermediate claim Hpred: 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun (apply_fun pair_fun p0) 0 ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is In_0_2.
An exact proof term for the current goal is HU0.
An exact proof term for the current goal is Hf0U.
An exact proof term for the current goal is (SepI (product_space I Xi) (λf0 : set ⇒ 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun f0 0 ∈ U) (apply_fun pair_fun p0) HfX1 Hpred).
An exact proof term for the current goal is (SepI X0 (λx0 : set ⇒ apply_fun pair_fun x0 ∈ product_cylinder I Xi 0 U) p0 Hp0X0 Hcyl).
rewrite the current goal using Heq0 (from left to right).
An exact proof term for the current goal is (generated_topology_contains_basis X0 B0 HB0 R0 HR0inB).
Assume Hi1: i = 1.
rewrite the current goal using Hi1 (from left to right).
We prove the intermediate claim HU1eq: space_family_topology Xi i = space_family_topology Xi 1.
rewrite the current goal using Hi1 (from left to right).
Use reflexivity.
We prove the intermediate claim HU1: U ∈ space_family_topology Xi 1.
rewrite the current goal using HU1eq (from right to left).
An exact proof term for the current goal is HUin.
We prove the intermediate claim HU: U ∈ Ty.
rewrite the current goal using HXtop1 (from right to left).
An exact proof term for the current goal is HU1.
We prove the intermediate claim HTySub: Ty ⊆ 𝒫 Y.
An exact proof term for the current goal is (topology_subset_axiom Y Ty HTy).
We prove the intermediate claim HUpow: U ∈ 𝒫 Y.
An exact proof term for the current goal is (HTySub U HU).
We prove the intermediate claim HUsubY: U ⊆ Y.
An exact proof term for the current goal is (PowerE Y U HUpow).
Set R1 to be the term rectangle_set X U.
We prove the intermediate claim HXTx: X ∈ Tx.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim HR1inB: R1 ∈ B0.
We prove the intermediate claim HRfam: R1 ∈ {rectangle_set X V|V ∈ Ty}.
An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set X V0) U HU).
An exact proof term for the current goal is (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) X R1 HXTx HRfam).
We prove the intermediate claim Heq1: preimage_of X0 pair_fun (product_cylinder I Xi 1 U) = R1.
Apply set_ext to the current goal.
Let p0 be given.
Assume Hp0: p0 ∈ preimage_of X0 pair_fun (product_cylinder I Xi 1 U).
We will prove p0 ∈ R1.
We prove the intermediate claim Hp0X0: p0 ∈ X0.
An exact proof term for the current goal is (SepE1 X0 (λx0 : set ⇒ apply_fun pair_fun x0 ∈ product_cylinder I Xi 1 U) p0 Hp0).
We prove the intermediate claim Himg: apply_fun pair_fun p0 ∈ product_cylinder I Xi 1 U.
An exact proof term for the current goal is (SepE2 X0 (λx0 : set ⇒ apply_fun pair_fun x0 ∈ product_cylinder I Xi 1 U) p0 Hp0).
We prove the intermediate claim Hconj: 1 ∈ I ∧ U ∈ space_family_topology Xi 1 ∧ apply_fun (apply_fun pair_fun p0) 1 ∈ U.
An exact proof term for the current goal is (SepE2 (product_space I Xi) (λf0 : set ⇒ 1 ∈ I ∧ U ∈ space_family_topology Xi 1 ∧ apply_fun f0 1 ∈ U) (apply_fun pair_fun p0) Himg).
We prove the intermediate claim Hthird: apply_fun (apply_fun pair_fun p0) 1 ∈ U.
An exact proof term for the current goal is (andER (1 ∈ I ∧ U ∈ space_family_topology Xi 1) (apply_fun (apply_fun pair_fun p0) 1 ∈ U) Hconj).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun pair_fun p0) 1 = p0 1.
rewrite the current goal using (apply_fun_graph X0 (λq : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (q 0) (q 1))) p0 Hp0X0) (from left to right).
rewrite the current goal using (apply_fun_graph I (λi0 : set ⇒ If_i (i0 = 0) (p0 0) (p0 1)) 1 In_1_2) (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (p0 0) (p0 1) H10) (from left to right).
Use reflexivity.
We prove the intermediate claim Hp01U: p0 1 ∈ U.
rewrite the current goal using HcoordEq (from right to left).
An exact proof term for the current goal is Hthird.
We prove the intermediate claim Hp00X: p0 0 ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ Y) p0 Hp0X0).
rewrite the current goal using rectangle_set_def (from left to right).
We prove the intermediate claim HpEta: p0 = (p0 0,p0 1).
An exact proof term for the current goal is (setprod_eta X Y p0 Hp0X0).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X U (p0 0) (p0 1) Hp00X Hp01U).
Let p0 be given.
Assume Hp0: p0 ∈ R1.
We will prove p0 ∈ preimage_of X0 pair_fun (product_cylinder I Xi 1 U).
We prove the intermediate claim HpXU: p0 ∈ setprod X U.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is Hp0.
We prove the intermediate claim Hp00X: p0 0 ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ U) p0 HpXU).
We prove the intermediate claim Hp01U: p0 1 ∈ U.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ U) p0 HpXU).
We prove the intermediate claim Hp01Y: p0 1 ∈ Y.
An exact proof term for the current goal is (HUsubY (p0 1) Hp01U).
We prove the intermediate claim Hp0X0: p0 ∈ X0.
We prove the intermediate claim HpEta: p0 = (p0 0,p0 1).
An exact proof term for the current goal is (setprod_eta X U p0 HpXU).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (p0 0) (p0 1) Hp00X Hp01Y).
We prove the intermediate claim HfX1: apply_fun pair_fun p0 ∈ X1.
An exact proof term for the current goal is (Hfun_pair_fun p0 Hp0X0).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun pair_fun p0) 1 = p0 1.
rewrite the current goal using (apply_fun_graph X0 (λq : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (q 0) (q 1))) p0 Hp0X0) (from left to right).
rewrite the current goal using (apply_fun_graph I (λi0 : set ⇒ If_i (i0 = 0) (p0 0) (p0 1)) 1 In_1_2) (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (p0 0) (p0 1) H10) (from left to right).
Use reflexivity.
We prove the intermediate claim Hf1U: apply_fun (apply_fun pair_fun p0) 1 ∈ U.
rewrite the current goal using HcoordEq (from left to right).
An exact proof term for the current goal is Hp01U.
We prove the intermediate claim Hcyl: apply_fun pair_fun p0 ∈ product_cylinder I Xi 1 U.
We prove the intermediate claim Hpred: 1 ∈ I ∧ U ∈ space_family_topology Xi 1 ∧ apply_fun (apply_fun pair_fun p0) 1 ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is In_1_2.
An exact proof term for the current goal is HU1.
An exact proof term for the current goal is Hf1U.
An exact proof term for the current goal is (SepI (product_space I Xi) (λf0 : set ⇒ 1 ∈ I ∧ U ∈ space_family_topology Xi 1 ∧ apply_fun f0 1 ∈ U) (apply_fun pair_fun p0) HfX1 Hpred).
An exact proof term for the current goal is (SepI X0 (λx0 : set ⇒ apply_fun pair_fun x0 ∈ product_cylinder I Xi 1 U) p0 Hp0X0 Hcyl).
rewrite the current goal using Heq1 (from left to right).
An exact proof term for the current goal is (generated_topology_contains_basis X0 B0 HB0 R1 HR1inB).
We use fun_pair to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim Hfun_fun_pair: function_on fun_pair X1 X0.
Let h be given.
Assume Hh: h ∈ X1.
We will prove apply_fun fun_pair h ∈ X0.
rewrite the current goal using (apply_fun_graph X1 (λh0 : set ⇒ (apply_fun h0 0,apply_fun h0 1)) h Hh) (from left to right).
We prove the intermediate claim Hcoords: ∀i0 : set, i0 ∈ I → apply_fun h i0 ∈ space_family_set Xi i0.
An exact proof term for the current goal is (andER (total_function_on h I (space_family_union I Xi) ∧ functional_graph h) (∀i0 : set, i0 ∈ I → apply_fun h i0 ∈ space_family_set Xi i0) (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ I → apply_fun f0 i0 ∈ space_family_set Xi i0) h Hh)).
We prove the intermediate claim Hh0X: apply_fun h 0 ∈ X.
rewrite the current goal using HXset0 (from right to left).
An exact proof term for the current goal is (Hcoords 0 In_0_2).
We prove the intermediate claim Hh1Y: apply_fun h 1 ∈ Y.
rewrite the current goal using HXset1 (from right to left).
An exact proof term for the current goal is (Hcoords 1 In_1_2).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (apply_fun h 0) (apply_fun h 1) Hh0X Hh1Y).
We prove the intermediate claim HB0sub: B0 ⊆ 𝒫 X0.
An exact proof term for the current goal is (andEL (B0 ⊆ 𝒫 X0) (∀x0 ∈ X0, ∃b ∈ B0, x0 ∈ b) (andEL (B0 ⊆ 𝒫 X0 ∧ (∀x0 ∈ X0, ∃b ∈ B0, x0 ∈ b)) (∀b1 ∈ B0, ∀b2 ∈ B0, ∀x0 : set, x0 ∈ b1 → x0 ∈ b2 → ∃b3 ∈ B0, x0 ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HB0)).
We prove the intermediate claim HpreB0: ∀b : set, b ∈ B0 → preimage_of X1 fun_pair b ∈ T1.
Let b be given.
Assume HbB: b ∈ B0.
We prove the intermediate claim HexU: ∃U ∈ Tx, b ∈ {rectangle_set U V|V ∈ Ty}.
An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b HbB).
Apply HexU to the current goal.
Let U be given.
Assume HUpack.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (b ∈ {rectangle_set U V|V ∈ Ty}) HUpack).
We prove the intermediate claim HbFam: b ∈ {rectangle_set U V|V ∈ Ty}.
An exact proof term for the current goal is (andER (U ∈ Tx) (b ∈ {rectangle_set U V|V ∈ Ty}) HUpack).
We prove the intermediate claim HexV: ∃V : set, V ∈ Ty ∧ b = rectangle_set U V.
An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U V0) b HbFam).
Apply HexV to the current goal.
Let V be given.
Assume HVconj.
We prove the intermediate claim HV: V ∈ Ty.
An exact proof term for the current goal is (andEL (V ∈ Ty) (b = rectangle_set U V) HVconj).
We prove the intermediate claim Hbeq: b = rectangle_set U V.
An exact proof term for the current goal is (andER (V ∈ Ty) (b = rectangle_set U V) HVconj).
We prove the intermediate claim HU0: U ∈ space_family_topology Xi 0.
rewrite the current goal using HXtop0 (from left to right).
An exact proof term for the current goal is HU.
We prove the intermediate claim HV1: V ∈ space_family_topology Xi 1.
rewrite the current goal using HXtop1 (from left to right).
An exact proof term for the current goal is HV.
Set C0 to be the term product_cylinder I Xi 0 U.
Set C1 to be the term product_cylinder I Xi 1 V.
We prove the intermediate claim HX1def: X1 = product_space I Xi.
Use reflexivity.
We prove the intermediate claim HC0inS: C0 ∈ product_subbasis_full I Xi.
We prove the intermediate claim HRepl: C0 ∈ {product_cylinder I Xi 0 U0|U0 ∈ space_family_topology Xi 0}.
An exact proof term for the current goal is (ReplI (space_family_topology Xi 0) (λU0 : set ⇒ product_cylinder I Xi 0 U0) U HU0).
An exact proof term for the current goal is (famunionI I (λi0 : set ⇒ {product_cylinder I Xi i0 U0|U0 ∈ space_family_topology Xi i0}) 0 C0 In_0_2 HRepl).
We prove the intermediate claim HC1inS: C1 ∈ product_subbasis_full I Xi.
We prove the intermediate claim HRepl: C1 ∈ {product_cylinder I Xi 1 U0|U0 ∈ space_family_topology Xi 1}.
An exact proof term for the current goal is (ReplI (space_family_topology Xi 1) (λU0 : set ⇒ product_cylinder I Xi 1 U0) V HV1).
An exact proof term for the current goal is (famunionI I (λi0 : set ⇒ {product_cylinder I Xi i0 U0|U0 ∈ space_family_topology Xi i0}) 1 C1 In_1_2 HRepl).
We prove the intermediate claim HC0open: C0 ∈ T1.
An exact proof term for the current goal is (generated_topology_from_subbasis_contains_subbasis_elem X1 (product_subbasis_full I Xi) C0 HSsub HC0inS).
We prove the intermediate claim HC1open: C1 ∈ T1.
An exact proof term for the current goal is (generated_topology_from_subbasis_contains_subbasis_elem X1 (product_subbasis_full I Xi) C1 HSsub HC1inS).
We prove the intermediate claim HT1: topology_on X1 T1.
An exact proof term for the current goal is (topology_from_subbasis_is_topology X1 (product_subbasis_full I Xi) HSsub).
We prove the intermediate claim HinterOpen: C0 ∩ C1 ∈ T1.
An exact proof term for the current goal is (topology_binintersect_closed X1 T1 C0 C1 HT1 HC0open HC1open).
We prove the intermediate claim HpreEq: preimage_of X1 fun_pair b = C0 ∩ C1.
rewrite the current goal using Hbeq (from left to right).
Apply set_ext to the current goal.
Let h be given.
Assume Hh: h ∈ preimage_of X1 fun_pair (rectangle_set U V).
We will prove h ∈ C0 ∩ C1.
We prove the intermediate claim HhX1: h ∈ X1.
An exact proof term for the current goal is (SepE1 X1 (λx0 : set ⇒ apply_fun fun_pair x0 ∈ rectangle_set U V) h Hh).
We prove the intermediate claim Himg: apply_fun fun_pair h ∈ rectangle_set U V.
An exact proof term for the current goal is (SepE2 X1 (λx0 : set ⇒ apply_fun fun_pair x0 ∈ rectangle_set U V) h Hh).
We prove the intermediate claim HimgUV: apply_fun fun_pair h ∈ setprod U V.
rewrite the current goal using rectangle_set_def (from right to left).
An exact proof term for the current goal is Himg.
We prove the intermediate claim H0U0: (apply_fun fun_pair h) 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ V) (apply_fun fun_pair h) HimgUV).
We prove the intermediate claim H1V0: (apply_fun fun_pair h) 1 ∈ V.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ V) (apply_fun fun_pair h) HimgUV).
We prove the intermediate claim HimgEq: apply_fun fun_pair h = (apply_fun h 0,apply_fun h 1).
rewrite the current goal using (apply_fun_graph X1 (λh0 : set ⇒ (apply_fun h0 0,apply_fun h0 1)) h HhX1) (from left to right).
Use reflexivity.
We prove the intermediate claim H0eq: (apply_fun fun_pair h) 0 = apply_fun h 0.
rewrite the current goal using HimgEq (from left to right).
rewrite the current goal using (tuple_pair (apply_fun h 0) (apply_fun h 1)) (from right to left) at position 1.
rewrite the current goal using (pair_ap_0 (apply_fun h 0) (apply_fun h 1)) (from left to right).
Use reflexivity.
We prove the intermediate claim H1eq: (apply_fun fun_pair h) 1 = apply_fun h 1.
rewrite the current goal using HimgEq (from left to right).
rewrite the current goal using (tuple_pair (apply_fun h 0) (apply_fun h 1)) (from right to left) at position 1.
rewrite the current goal using (pair_ap_1 (apply_fun h 0) (apply_fun h 1)) (from left to right).
Use reflexivity.
We prove the intermediate claim H0U: apply_fun h 0 ∈ U.
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is H0U0.
We prove the intermediate claim H1V: apply_fun h 1 ∈ V.
rewrite the current goal using H1eq (from right to left).
An exact proof term for the current goal is H1V0.
We prove the intermediate claim Hc0: h ∈ C0.
We prove the intermediate claim Hpred: 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun h 0 ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is In_0_2.
An exact proof term for the current goal is HU0.
An exact proof term for the current goal is H0U.
An exact proof term for the current goal is (SepI (product_space I Xi) (λf0 : set ⇒ 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun f0 0 ∈ U) h HhX1 Hpred).
We prove the intermediate claim Hc1: h ∈ C1.
We prove the intermediate claim Hpred: 1 ∈ I ∧ V ∈ space_family_topology Xi 1 ∧ apply_fun h 1 ∈ V.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is In_1_2.
An exact proof term for the current goal is HV1.
An exact proof term for the current goal is H1V.
An exact proof term for the current goal is (SepI (product_space I Xi) (λf0 : set ⇒ 1 ∈ I ∧ V ∈ space_family_topology Xi 1 ∧ apply_fun f0 1 ∈ V) h HhX1 Hpred).
An exact proof term for the current goal is (binintersectI C0 C1 h Hc0 Hc1).
Let h be given.
Assume Hh: h ∈ C0 ∩ C1.
We will prove h ∈ preimage_of X1 fun_pair (rectangle_set U V).
We prove the intermediate claim HhC0: h ∈ C0.
An exact proof term for the current goal is (binintersectE1 C0 C1 h Hh).
We prove the intermediate claim HhC1: h ∈ C1.
An exact proof term for the current goal is (binintersectE2 C0 C1 h Hh).
We prove the intermediate claim HhX1: h ∈ X1.
An exact proof term for the current goal is (SepE1 (product_space I Xi) (λf0 : set ⇒ 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun f0 0 ∈ U) h HhC0).
We prove the intermediate claim Hc0pred: 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun h 0 ∈ U.
An exact proof term for the current goal is (SepE2 (product_space I Xi) (λf0 : set ⇒ 0 ∈ I ∧ U ∈ space_family_topology Xi 0 ∧ apply_fun f0 0 ∈ U) h HhC0).
We prove the intermediate claim Hc1pred: 1 ∈ I ∧ V ∈ space_family_topology Xi 1 ∧ apply_fun h 1 ∈ V.
An exact proof term for the current goal is (SepE2 (product_space I Xi) (λf0 : set ⇒ 1 ∈ I ∧ V ∈ space_family_topology Xi 1 ∧ apply_fun f0 1 ∈ V) h HhC1).
We prove the intermediate claim Hh0U: apply_fun h 0 ∈ U.
An exact proof term for the current goal is (andER (0 ∈ I ∧ U ∈ space_family_topology Xi 0) (apply_fun h 0 ∈ U) Hc0pred).
We prove the intermediate claim Hh1V: apply_fun h 1 ∈ V.
An exact proof term for the current goal is (andER (1 ∈ I ∧ V ∈ space_family_topology Xi 1) (apply_fun h 1 ∈ V) Hc1pred).
We prove the intermediate claim HimgEq: apply_fun fun_pair h = (apply_fun h 0,apply_fun h 1).
rewrite the current goal using (apply_fun_graph X1 (λh0 : set ⇒ (apply_fun h0 0,apply_fun h0 1)) h HhX1) (from left to right).
Use reflexivity.
We prove the intermediate claim Hrect: (apply_fun h 0,apply_fun h 1) ∈ rectangle_set U V.
An exact proof term for the current goal is (tuple_2_rectangle_set U V (apply_fun h 0) (apply_fun h 1) Hh0U Hh1V).
We prove the intermediate claim Himg: apply_fun fun_pair h ∈ rectangle_set U V.
rewrite the current goal using HimgEq (from left to right).
An exact proof term for the current goal is Hrect.
An exact proof term for the current goal is (SepI X1 (λx0 : set ⇒ apply_fun fun_pair x0 ∈ rectangle_set U V) h HhX1 Himg).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is HinterOpen.
We prove the intermediate claim HT0eq: T0 = generated_topology X0 B0.
Use reflexivity.
rewrite the current goal using HT0eq (from left to right).
An exact proof term for the current goal is (continuous_map_to_generated_topology X1 T1 X0 B0 fun_pair (topology_from_subbasis_is_topology X1 (product_subbasis_full I Xi) HSsub) HB0 Hfun_fun_pair HpreB0).
Let x be given.
Assume Hx: x ∈ X0.
We will prove apply_fun fun_pair (apply_fun pair_fun x) = x.
We prove the intermediate claim HpxX1: apply_fun pair_fun x ∈ X1.
rewrite the current goal using (apply_fun_graph X0 (λp : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (p 0) (p 1))) x Hx) (from left to right).
Set h to be the term (λi0 : set ⇒ If_i (i0 = 0) (x 0) (x 1)).
We prove the intermediate claim Hhdef: h = (λi0 : set ⇒ If_i (i0 = 0) (x 0) (x 1)).
Use reflexivity.
rewrite the current goal using Hhdef (from right to left).
Set gp to be the term graph I h.
We prove the intermediate claim Hgpdef: gp = graph I h.
Use reflexivity.
rewrite the current goal using Hgpdef (from right to left).
We prove the intermediate claim Hx0X: x 0 ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ Y) x Hx).
We prove the intermediate claim Hx1Y: x 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ Y) x Hx).
We prove the intermediate claim Hhj_union: ∀j : set, j ∈ I → h j ∈ space_family_union I Xi.
Let j be given.
Assume HjI: j ∈ I.
We prove the intermediate claim Hhj_eq: h j = If_i (j = 0) (x 0) (x 1).
Use reflexivity.
We prove the intermediate claim Hj01: j ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 j HjI).
Apply (UPairE j 0 1 Hj01 (h j ∈ space_family_union I Xi)) to the current goal.
Assume Hj0: j = 0.
rewrite the current goal using Hhj_eq (from left to right).
rewrite the current goal using Hj0 (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (x 0) (x 1) H00) (from left to right).
We prove the intermediate claim Hx0sf: x 0 ∈ space_family_set Xi 0.
rewrite the current goal using HXset0 (from left to right).
An exact proof term for the current goal is Hx0X.
An exact proof term for the current goal is (UnionI {space_family_set Xi i0|i0 ∈ I} (x 0) (space_family_set Xi 0) Hx0sf (ReplI I (λi0 : set ⇒ space_family_set Xi i0) 0 In_0_2)).
Assume Hj1: j = 1.
rewrite the current goal using Hhj_eq (from left to right).
rewrite the current goal using Hj1 (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (x 0) (x 1) H10) (from left to right).
We prove the intermediate claim Hx1sf: x 1 ∈ space_family_set Xi 1.
rewrite the current goal using HXset1 (from left to right).
An exact proof term for the current goal is Hx1Y.
An exact proof term for the current goal is (UnionI {space_family_set Xi i0|i0 ∈ I} (x 1) (space_family_set Xi 1) Hx1sf (ReplI I (λi0 : set ⇒ space_family_set Xi i0) 1 In_1_2)).
We prove the intermediate claim Hgp_sub: gp ⊆ setprod I (space_family_union I Xi).
Let z be given.
Assume Hz: z ∈ gp.
Apply (ReplE_impred I (λj0 : set ⇒ (j0,h j0)) z Hz (z ∈ setprod I (space_family_union I Xi))) to the current goal.
Let j be given.
Assume HjI: j ∈ I.
Assume HzEq: z = (j,h j).
rewrite the current goal using HzEq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma I (space_family_union I Xi) j (h j) HjI (Hhj_union j HjI)).
We prove the intermediate claim Hgp_pow: gp ∈ 𝒫 (setprod I (space_family_union I Xi)).
An exact proof term for the current goal is (PowerI (setprod I (space_family_union I Xi)) gp Hgp_sub).
We prove the intermediate claim Hgp_tot: total_function_on gp I (space_family_union I Xi).
Apply (total_function_on_graph I (space_family_union I Xi) h) to the current goal.
An exact proof term for the current goal is Hhj_union.
We prove the intermediate claim Hgp_fun: functional_graph gp.
An exact proof term for the current goal is (functional_graph_graph I h).
We prove the intermediate claim Hcoords: ∀j : set, j ∈ I → apply_fun gp j ∈ space_family_set Xi j.
Let j be given.
Assume HjI: j ∈ I.
rewrite the current goal using (apply_fun_graph I h j HjI) (from left to right).
We prove the intermediate claim Hhj_eq: h j = If_i (j = 0) (x 0) (x 1).
Use reflexivity.
We prove the intermediate claim Hj01: j ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 j HjI).
Apply (UPairE j 0 1 Hj01 (h j ∈ space_family_set Xi j)) to the current goal.
Assume Hj0: j = 0.
rewrite the current goal using Hhj_eq (from left to right).
rewrite the current goal using Hj0 (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (x 0) (x 1) H00) (from left to right).
rewrite the current goal using HXset0 (from left to right).
An exact proof term for the current goal is Hx0X.
Assume Hj1: j = 1.
rewrite the current goal using Hhj_eq (from left to right).
rewrite the current goal using Hj1 (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (x 0) (x 1) H10) (from left to right).
rewrite the current goal using HXset1 (from left to right).
An exact proof term for the current goal is Hx1Y.
We prove the intermediate claim Hpred: total_function_on gp I (space_family_union I Xi) ∧ functional_graph gp ∧ ∀j : set, j ∈ I → apply_fun gp j ∈ space_family_set Xi j.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hgp_tot.
An exact proof term for the current goal is Hgp_fun.
An exact proof term for the current goal is Hcoords.
An exact proof term for the current goal is (SepI (𝒫 (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) gp Hgp_pow Hpred).
We prove the intermediate claim HimgEq: apply_fun fun_pair (apply_fun pair_fun x) = (apply_fun (apply_fun pair_fun x) 0,apply_fun (apply_fun pair_fun x) 1).
rewrite the current goal using (apply_fun_graph X1 (λh0 : set ⇒ (apply_fun h0 0,apply_fun h0 1)) (apply_fun pair_fun x) HpxX1) (from left to right).
Use reflexivity.
rewrite the current goal using HimgEq (from left to right).
We prove the intermediate claim Hcoord0: apply_fun (apply_fun pair_fun x) 0 = x 0.
rewrite the current goal using (apply_fun_graph X0 (λp : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (p 0) (p 1))) x Hx) (from left to right).
rewrite the current goal using (apply_fun_graph I (λi0 : set ⇒ If_i (i0 = 0) (x 0) (x 1)) 0 In_0_2) (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (x 0) (x 1) H00) (from left to right).
Use reflexivity.
We prove the intermediate claim Hcoord1: apply_fun (apply_fun pair_fun x) 1 = x 1.
rewrite the current goal using (apply_fun_graph X0 (λp : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (p 0) (p 1))) x Hx) (from left to right).
rewrite the current goal using (apply_fun_graph I (λi0 : set ⇒ If_i (i0 = 0) (x 0) (x 1)) 1 In_1_2) (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (x 0) (x 1) H10) (from left to right).
Use reflexivity.
rewrite the current goal using Hcoord0 (from left to right).
rewrite the current goal using Hcoord1 (from left to right).
We prove the intermediate claim HxEta: x = (x 0,x 1).
An exact proof term for the current goal is (setprod_eta X Y x Hx).
rewrite the current goal using HxEta (from right to left).
Use reflexivity.
Let y be given.
Assume Hy: y ∈ X1.
We will prove apply_fun pair_fun (apply_fun fun_pair y) = y.
Set p to be the term apply_fun fun_pair y.
We prove the intermediate claim HpEq: p = (apply_fun y 0,apply_fun y 1).
rewrite the current goal using (apply_fun_graph X1 (λh0 : set ⇒ (apply_fun h0 0,apply_fun h0 1)) y Hy) (from left to right).
Use reflexivity.
We prove the intermediate claim Hycoords: ∀i0 : set, i0 ∈ I → apply_fun y i0 ∈ space_family_set Xi i0.
An exact proof term for the current goal is (andER (total_function_on y I (space_family_union I Xi) ∧ functional_graph y) (∀i0 : set, i0 ∈ I → apply_fun y i0 ∈ space_family_set Xi i0) (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ I → apply_fun f0 i0 ∈ space_family_set Xi i0) y Hy)).
We prove the intermediate claim Hy0X: apply_fun y 0 ∈ X.
rewrite the current goal using HXset0 (from right to left).
An exact proof term for the current goal is (Hycoords 0 In_0_2).
We prove the intermediate claim Hy1Y: apply_fun y 1 ∈ Y.
rewrite the current goal using HXset1 (from right to left).
An exact proof term for the current goal is (Hycoords 1 In_1_2).
We prove the intermediate claim HpX0: p ∈ X0.
rewrite the current goal using HpEq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (apply_fun y 0) (apply_fun y 1) Hy0X Hy1Y).
rewrite the current goal using (apply_fun_graph X0 (λq : set ⇒ graph I (λi0 : set ⇒ If_i (i0 = 0) (q 0) (q 1))) p HpX0) (from left to right).
We prove the intermediate claim Hp0eq: p 0 = apply_fun y 0.
rewrite the current goal using HpEq (from left to right).
rewrite the current goal using (tuple_pair (apply_fun y 0) (apply_fun y 1)) (from right to left) at position 1.
rewrite the current goal using (pair_ap_0 (apply_fun y 0) (apply_fun y 1)) (from left to right).
Use reflexivity.
We prove the intermediate claim Hp1eq: p 1 = apply_fun y 1.
rewrite the current goal using HpEq (from left to right).
rewrite the current goal using (tuple_pair (apply_fun y 0) (apply_fun y 1)) (from right to left) at position 1.
rewrite the current goal using (pair_ap_1 (apply_fun y 0) (apply_fun y 1)) (from left to right).
Use reflexivity.
rewrite the current goal using Hp0eq (from left to right).
rewrite the current goal using Hp1eq (from left to right).
Set h to be the term (λi0 : set ⇒ If_i (i0 = 0) (apply_fun y 0) (apply_fun y 1)).
We prove the intermediate claim Hhdef: h = (λi0 : set ⇒ If_i (i0 = 0) (apply_fun y 0) (apply_fun y 1)).
Use reflexivity.
rewrite the current goal using Hhdef (from right to left).
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ graph I h.
We will prove z ∈ y.
Apply (ReplE_impred I (λj0 : set ⇒ (j0,h j0)) z Hz (z ∈ y)) to the current goal.
Let j be given.
Assume HjI: j ∈ I.
Assume HzEq: z = (j,h j).
rewrite the current goal using HzEq (from left to right).
We prove the intermediate claim Htoty: total_function_on y I (space_family_union I Xi).
An exact proof term for the current goal is (andEL (total_function_on y I (space_family_union I Xi)) (functional_graph y) (andEL (total_function_on y I (space_family_union I Xi) ∧ functional_graph y) (∀i0 : set, i0 ∈ I → apply_fun y i0 ∈ space_family_set Xi i0) (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ I → apply_fun f0 i0 ∈ space_family_set Xi i0) y Hy))).
We prove the intermediate claim Hyj: (j,apply_fun y j) ∈ y.
An exact proof term for the current goal is (total_function_on_apply_fun_in_graph y I (space_family_union I Xi) j Htoty HjI).
We prove the intermediate claim Heqyj: apply_fun y j = h j.
We prove the intermediate claim Hj01: j ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 j HjI).
Apply (UPairE j 0 1 Hj01 (apply_fun y j = h j)) to the current goal.
Assume Hj0: j = 0.
rewrite the current goal using Hj0 (from left to right).
We prove the intermediate claim Hh0eq: h 0 = If_i (0 = 0) (apply_fun y 0) (apply_fun y 1).
Use reflexivity.
rewrite the current goal using Hh0eq (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (apply_fun y 0) (apply_fun y 1) H00) (from left to right).
Use reflexivity.
Assume Hj1: j = 1.
rewrite the current goal using Hj1 (from left to right).
We prove the intermediate claim Hh1eq: h 1 = If_i (1 = 0) (apply_fun y 0) (apply_fun y 1).
Use reflexivity.
rewrite the current goal using Hh1eq (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (apply_fun y 0) (apply_fun y 1) H10) (from left to right).
Use reflexivity.
rewrite the current goal using Heqyj (from right to left).
An exact proof term for the current goal is Hyj.
Let z be given.
Assume Hz: z ∈ y.
We will prove z ∈ graph I h.
We prove the intermediate claim HyPow: y ∈ 𝒫 (setprod I (space_family_union I Xi)).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod I (space_family_union I Xi))) (λf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ I → apply_fun f0 i0 ∈ space_family_set Xi i0) y Hy).
We prove the intermediate claim HzUV: z ∈ setprod I (space_family_union I Xi).
An exact proof term for the current goal is (PowerE (setprod I (space_family_union I Xi)) y HyPow z Hz).
We prove the intermediate claim HjI: z 0 ∈ I.
An exact proof term for the current goal is (ap0_Sigma I (λ_ : set ⇒ space_family_union I Xi) z HzUV).
We prove the intermediate claim HzEta: z = (z 0,z 1).
An exact proof term for the current goal is (setprod_eta I (space_family_union I Xi) z HzUV).
We prove the intermediate claim Htoty: total_function_on y I (space_family_union I Xi).
An exact proof term for the current goal is (andEL (total_function_on y I (space_family_union I Xi)) (functional_graph y) (andEL (total_function_on y I (space_family_union I Xi) ∧ functional_graph y) (∀i0 : set, i0 ∈ I → apply_fun y i0 ∈ space_family_set Xi i0) (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ I → apply_fun f0 i0 ∈ space_family_set Xi i0) y Hy))).
We prove the intermediate claim Hfuny: functional_graph y.
An exact proof term for the current goal is (andER (total_function_on y I (space_family_union I Xi)) (functional_graph y) (andEL (total_function_on y I (space_family_union I Xi) ∧ functional_graph y) (∀i0 : set, i0 ∈ I → apply_fun y i0 ∈ space_family_set Xi i0) (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λf0 : set ⇒ total_function_on f0 I (space_family_union I Xi) ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ I → apply_fun f0 i0 ∈ space_family_set Xi i0) y Hy))).
We prove the intermediate claim Hyj: (z 0,apply_fun y (z 0)) ∈ y.
An exact proof term for the current goal is (total_function_on_apply_fun_in_graph y I (space_family_union I Xi) (z 0) Htoty HjI).
We prove the intermediate claim HzPair: (z 0,z 1) ∈ y.
rewrite the current goal using HzEta (from right to left).
An exact proof term for the current goal is Hz.
We prove the intermediate claim Hap: apply_fun y (z 0) = z 1.
An exact proof term for the current goal is (functional_graph_apply_fun_eq y (z 0) (z 1) Hfuny HzPair).
We prove the intermediate claim Heqyj: apply_fun y (z 0) = h (z 0).
We prove the intermediate claim Hj01: z 0 ∈ {0,1}.
An exact proof term for the current goal is (Subq_2_UPair01 (z 0) HjI).
Apply (UPairE (z 0) 0 1 Hj01 (apply_fun y (z 0) = h (z 0))) to the current goal.
Assume Hj0: z 0 = 0.
rewrite the current goal using Hj0 (from left to right).
We prove the intermediate claim Hh0eq: h 0 = If_i (0 = 0) (apply_fun y 0) (apply_fun y 1).
Use reflexivity.
rewrite the current goal using Hh0eq (from left to right).
We prove the intermediate claim H00: 0 = 0.
Use reflexivity.
rewrite the current goal using (If_i_1 (0 = 0) (apply_fun y 0) (apply_fun y 1) H00) (from left to right).
Use reflexivity.
Assume Hj1: z 0 = 1.
rewrite the current goal using Hj1 (from left to right).
We prove the intermediate claim Hh1eq: h 1 = If_i (1 = 0) (apply_fun y 0) (apply_fun y 1).
Use reflexivity.
rewrite the current goal using Hh1eq (from left to right).
We prove the intermediate claim H10: ¬ (1 = 0).
An exact proof term for the current goal is neq_1_0.
rewrite the current goal using (If_i_0 (1 = 0) (apply_fun y 0) (apply_fun y 1) H10) (from left to right).
Use reflexivity.
rewrite the current goal using HzEta (from left to right).
We prove the intermediate claim Hz1eq: z 1 = h (z 0).
We will prove z 1 = h (z 0).
rewrite the current goal using Hap (from right to left).
An exact proof term for the current goal is Heqyj.
rewrite the current goal using Hz1eq (from left to right).
An exact proof term for the current goal is (ReplI I (λj0 : set ⇒ (j0,h j0)) (z 0) HjI).
An exact proof term for the current goal is (homeomorphism_preserves_completely_regular X0 T0 X1 T1 pair_fun Hhom HcrX1).
∎