Let X, Tx, Y and Ty be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume Hcomp: compact_space Y Ty.
Let x0 be given.
Assume Hx0: x0 ∈ X.
Let N be given.
Assume HN: N ∈ product_topology X Tx Y Ty ∧ setprod {x0} Y ⊆ N.
We will prove ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ setprod U Y ⊆ N.
Set B to be the term product_subbasis X Tx Y Ty.
We prove the intermediate claim HBasis: basis_on (setprod X Y) B.
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim HNtop: N ∈ generated_topology (setprod X Y) B.
An exact proof term for the current goal is (andEL (N ∈ product_topology X Tx Y Ty) (setprod {x0} Y ⊆ N) HN).
We prove the intermediate claim HNsub: setprod {x0} Y ⊆ N.
An exact proof term for the current goal is (andER (N ∈ product_topology X Tx Y Ty) (setprod {x0} Y ⊆ N) HN).
We prove the intermediate claim HNrefine: ∀p ∈ N, ∃b ∈ B, p ∈ b ∧ b ⊆ N.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ B, x ∈ b ∧ b ⊆ U0) N HNtop).
Set VFam to be the term {V ∈ Ty|∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ setprod U V ⊆ N}.
We prove the intermediate claim HVFamSubTy: VFam ⊆ Ty.
Let V be given.
Assume HV: V ∈ VFam.
An exact proof term for the current goal is (SepE1 Ty (λV0 : set ⇒ ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ setprod U V0 ⊆ N) V HV).
We prove the intermediate claim HtopY: topology_on Y Ty.
An exact proof term for the current goal is (compact_space_topology Y Ty Hcomp).
We prove the intermediate claim HTyPow: Ty ⊆ 𝒫 Y.
An exact proof term for the current goal is (topology_subset_axiom Y Ty HtopY).
We prove the intermediate claim HVFamPowY: VFam ⊆ 𝒫 Y.
Let V be given.
Assume HV: V ∈ VFam.
We prove the intermediate claim HVTy: V ∈ Ty.
An exact proof term for the current goal is (HVFamSubTy V HV).
An exact proof term for the current goal is (HTyPow V HVTy).
We prove the intermediate claim HYcov: Y ⊆ ⋃ VFam.
Let y be given.
Assume Hy: y ∈ Y.
We will prove y ∈ ⋃ VFam.
Set p to be the term (x0,y).
We prove the intermediate claim HpXY: p ∈ setprod {x0} Y.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x0} Y x0 y (SingI x0) Hy).
We prove the intermediate claim HpN: p ∈ N.
An exact proof term for the current goal is (HNsub p HpXY).
We prove the intermediate claim Hrect: ∃b ∈ B, p ∈ b ∧ b ⊆ N.
An exact proof term for the current goal is (HNrefine p HpN).
Apply Hrect to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ B.
An exact proof term for the current goal is (andEL (b ∈ B) (p ∈ b ∧ b ⊆ N) Hbpair).
We prove the intermediate claim Hbprop: p ∈ b ∧ b ⊆ N.
An exact proof term for the current goal is (andER (b ∈ B) (p ∈ b ∧ b ⊆ N) Hbpair).
We prove the intermediate claim Hpb: p ∈ b.
An exact proof term for the current goal is (andEL (p ∈ b) (b ⊆ N) Hbprop).
We prove the intermediate claim HbsubN: b ⊆ N.
An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ N) Hbprop).
Apply (famunionE_impred Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) b HbB) to the current goal.
Let U0 be given.
Assume HU0Tx: U0 ∈ Tx.
Assume HbIn: b ∈ {rectangle_set U0 V0|V0 ∈ Ty}.
Apply (ReplE_impred Ty (λV0 : set ⇒ rectangle_set U0 V0) b HbIn) to the current goal.
Let V0 be given.
Assume HV0Ty: V0 ∈ Ty.
Assume HbEq: b = rectangle_set U0 V0.
We prove the intermediate claim HpUV: p ∈ setprod U0 V0.
We will prove p ∈ rectangle_set U0 V0.
rewrite the current goal using HbEq (from right to left) at position 1.
An exact proof term for the current goal is Hpb.
We prove the intermediate claim HpXY0: p ∈ setprod {x0} {y}.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x0} {y} x0 y (SingI x0) (SingI y)).
We prove the intermediate claim Hcoords: x0 ∈ U0 ∧ y ∈ V0.
An exact proof term for the current goal is (setprod_coords_in x0 y U0 V0 p HpXY0 HpUV).
We prove the intermediate claim Hx0U0: x0 ∈ U0.
An exact proof term for the current goal is (andEL (x0 ∈ U0) (y ∈ V0) Hcoords).
We prove the intermediate claim HyV0: y ∈ V0.
An exact proof term for the current goal is (andER (x0 ∈ U0) (y ∈ V0) Hcoords).
We prove the intermediate claim HrectSub: setprod U0 V0 ⊆ N.
rewrite the current goal using HbEq (from right to left) at position 1.
An exact proof term for the current goal is HbsubN.
We prove the intermediate claim HV0Fam: V0 ∈ VFam.
Apply (SepI Ty (λV1 : set ⇒ ∃U1 : set, U1 ∈ Tx ∧ x0 ∈ U1 ∧ setprod U1 V1 ⊆ N) V0 HV0Ty) to the current goal.
We use U0 to witness the existential quantifier.
An exact proof term for the current goal is (andI (U0 ∈ Tx ∧ x0 ∈ U0) (setprod U0 V0 ⊆ N) (andI (U0 ∈ Tx) (x0 ∈ U0) HU0Tx Hx0U0) HrectSub).
An exact proof term for the current goal is (UnionI VFam y V0 HyV0 HV0Fam).
We prove the intermediate claim HVFamCover: open_cover_of Y Ty VFam.
We will prove topology_on Y Ty ∧ VFam ⊆ 𝒫 Y ∧ Y ⊆ ⋃ VFam ∧ (∀U : set, U ∈ VFam → U ∈ Ty).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HtopY.
An exact proof term for the current goal is HVFamPowY.
An exact proof term for the current goal is HYcov.
Let V be given.
Assume HV: V ∈ VFam.
An exact proof term for the current goal is (HVFamSubTy V HV).
We prove the intermediate claim Hfin: has_finite_subcover Y Ty VFam.
An exact proof term for the current goal is (Heine_Borel_subcover Y Ty VFam Hcomp HVFamCover).
Apply Hfin to the current goal.
Let G be given.
Assume HGtriple: G ⊆ VFam ∧ finite G ∧ Y ⊆ ⋃ G.
Set pickU to be the term λV : set ⇒ Eps_i (λU0 : set ⇒ U0 ∈ Tx ∧ x0 ∈ U0 ∧ setprod U0 V ⊆ N).
We prove the intermediate claim HpickU: ∀V : set, V ∈ VFam → pickU V ∈ Tx ∧ x0 ∈ pickU V ∧ setprod (pickU V) V ⊆ N.
Let V be given.
Assume HV: V ∈ VFam.
We prove the intermediate claim Hex: ∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ setprod U0 V ⊆ N.
An exact proof term for the current goal is (SepE2 Ty (λV0 : set ⇒ ∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ setprod U0 V0 ⊆ N) V HV).
Apply Hex to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Tx ∧ x0 ∈ U0 ∧ setprod U0 V ⊆ N.
We prove the intermediate claim Hax: pickU V ∈ Tx ∧ x0 ∈ pickU V ∧ setprod (pickU V) V ⊆ N.
An exact proof term for the current goal is (Eps_i_ax (λU1 : set ⇒ U1 ∈ Tx ∧ x0 ∈ U1 ∧ setprod U1 V ⊆ N) U0 HU0).
An exact proof term for the current goal is Hax.
We prove the intermediate claim HGsub: G ⊆ VFam.
An exact proof term for the current goal is (andEL (G ⊆ VFam) (finite G) (andEL (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HGtriple)).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ VFam) (finite G) (andEL (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HGtriple)).
We prove the intermediate claim HYcovG: Y ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HGtriple).
Set UFam to be the term {pickU V|V ∈ G}.
We prove the intermediate claim HUFamFin: finite UFam.
An exact proof term for the current goal is (Repl_finite (λV : set ⇒ pickU V) G HGfin).
We prove the intermediate claim HUFamPow: UFam ∈ 𝒫 Tx.
Apply PowerI Tx UFam to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ UFam.
We will prove U0 ∈ Tx.
Apply (ReplE_impred G (λV0 : set ⇒ pickU V0) U0 HU0) to the current goal.
Let V0 be given.
Assume HV0G: V0 ∈ G.
Assume HU0Eq: U0 = pickU V0.
We prove the intermediate claim HV0Fam: V0 ∈ VFam.
An exact proof term for the current goal is (HGsub V0 HV0G).
We prove the intermediate claim HU0Prop: pickU V0 ∈ Tx ∧ x0 ∈ pickU V0 ∧ setprod (pickU V0) V0 ⊆ N.
An exact proof term for the current goal is (HpickU V0 HV0Fam).
We prove the intermediate claim HU0AB: pickU V0 ∈ Tx ∧ x0 ∈ pickU V0.
An exact proof term for the current goal is (andEL (pickU V0 ∈ Tx ∧ x0 ∈ pickU V0) (setprod (pickU V0) V0 ⊆ N) HU0Prop).
We prove the intermediate claim HU0Tx: pickU V0 ∈ Tx.
An exact proof term for the current goal is (andEL (pickU V0 ∈ Tx) (x0 ∈ pickU V0) HU0AB).
rewrite the current goal using HU0Eq (from left to right).
An exact proof term for the current goal is HU0Tx.
Set U to be the term intersection_of_family X UFam.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx UFam HTx HUFamPow HUFamFin).
We prove the intermediate claim Hx0U: x0 ∈ U.
We will prove x0 ∈ intersection_of_family X UFam.
We prove the intermediate claim Hall: ∀W : set, W ∈ UFam → x0 ∈ W.
Let W be given.
Assume HW: W ∈ UFam.
We will prove x0 ∈ W.
Apply (ReplE_impred G (λV0 : set ⇒ pickU V0) W HW) to the current goal.
Let V0 be given.
Assume HV0G: V0 ∈ G.
Assume HWEq: W = pickU V0.
We prove the intermediate claim HV0Fam: V0 ∈ VFam.
An exact proof term for the current goal is (HGsub V0 HV0G).
We prove the intermediate claim HWProp: pickU V0 ∈ Tx ∧ x0 ∈ pickU V0 ∧ setprod (pickU V0) V0 ⊆ N.
An exact proof term for the current goal is (HpickU V0 HV0Fam).
We prove the intermediate claim HWPropAB: pickU V0 ∈ Tx ∧ x0 ∈ pickU V0.
An exact proof term for the current goal is (andEL (pickU V0 ∈ Tx ∧ x0 ∈ pickU V0) (setprod (pickU V0) V0 ⊆ N) HWProp).
We prove the intermediate claim Hx0Pick: x0 ∈ pickU V0.
An exact proof term for the current goal is (andER (pickU V0 ∈ Tx) (x0 ∈ pickU V0) HWPropAB).
rewrite the current goal using HWEq (from left to right).
An exact proof term for the current goal is Hx0Pick.
An exact proof term for the current goal is (SepI X (λx : set ⇒ ∀W : set, W ∈ UFam → x ∈ W) x0 Hx0 Hall).
We prove the intermediate claim HUsubN: setprod U Y ⊆ N.
Let p be given.
Assume Hp: p ∈ setprod U Y.
We will prove p ∈ N.
We prove the intermediate claim Hp0: p 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λu : set ⇒ Y) p Hp).
We prove the intermediate claim Hp1: p 1 ∈ Y.
An exact proof term for the current goal is (ap1_Sigma U (λu : set ⇒ Y) p Hp).
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta U Y p Hp).
We prove the intermediate claim Hp1InUnion: p 1 ∈ ⋃ G.
An exact proof term for the current goal is (HYcovG (p 1) Hp1).
Apply (UnionE_impred G (p 1) Hp1InUnion) to the current goal.
Let V0 be given.
Assume Hp1V0: p 1 ∈ V0.
Assume HV0G: V0 ∈ G.
We prove the intermediate claim HV0Fam: V0 ∈ VFam.
An exact proof term for the current goal is (HGsub V0 HV0G).
We prove the intermediate claim HV0Ty: V0 ∈ Ty.
An exact proof term for the current goal is (HVFamSubTy V0 HV0Fam).
We prove the intermediate claim Hpick: pickU V0 ∈ Tx ∧ x0 ∈ pickU V0 ∧ setprod (pickU V0) V0 ⊆ N.
An exact proof term for the current goal is (HpickU V0 HV0Fam).
We prove the intermediate claim HrectSubN: setprod (pickU V0) V0 ⊆ N.
An exact proof term for the current goal is (andER (pickU V0 ∈ Tx ∧ x0 ∈ pickU V0) (setprod (pickU V0) V0 ⊆ N) Hpick).
We prove the intermediate claim Hp0Pick: p 0 ∈ pickU V0.
We prove the intermediate claim Hp0All: ∀W : set, W ∈ UFam → p 0 ∈ W.
An exact proof term for the current goal is (SepE2 X (λx : set ⇒ ∀W : set, W ∈ UFam → x ∈ W) (p 0) Hp0).
We prove the intermediate claim Hmem: pickU V0 ∈ UFam.
An exact proof term for the current goal is (ReplI G (λV1 : set ⇒ pickU V1) V0 HV0G).
An exact proof term for the current goal is (Hp0All (pickU V0) Hmem).
We prove the intermediate claim HpairIn: (p 0,p 1) ∈ setprod (pickU V0) V0.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (pickU V0) V0 (p 0) (p 1) Hp0Pick Hp1V0).
We prove the intermediate claim HpN: (p 0,p 1) ∈ N.
An exact proof term for the current goal is (HrectSubN (p 0,p 1) HpairIn).
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is HpN.
We use U to witness the existential quantifier.
An exact proof term for the current goal is (andI (U ∈ Tx ∧ x0 ∈ U) (setprod U Y ⊆ N) (andI (U ∈ Tx) (x0 ∈ U) HUinTx Hx0U) HUsubN).
∎