Let X, Tx, Y, Ty and K be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume HKcomp: compact_space K (subspace_topology X Tx K).
Assume HKsubX: K ⊆ X.
Let y0 be given.
Assume Hy0Y: y0 ∈ Y.
Let N be given.
Assume HN: N ∈ product_topology X Tx Y Ty ∧ setprod K {y0} ⊆ 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 K {y0} ⊆ N) HN).
We prove the intermediate claim HNsub: setprod K {y0} ⊆ N.
An exact proof term for the current goal is (andER (N ∈ product_topology X Tx Y Ty) (setprod K {y0} ⊆ 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 ⇒ ∀q ∈ U0, ∃b ∈ B, q ∈ b ∧ b ⊆ U0) N HNtop).
Set UFam to be the term {U ∈ Tx|∃V : set, V ∈ Ty ∧ y0 ∈ V ∧ setprod U V ⊆ N}.
We prove the intermediate claim HUFamSubTx: UFam ⊆ Tx.
Let U be given.
Assume HU: U ∈ UFam.
An exact proof term for the current goal is (SepE1 Tx (λU0 : set ⇒ ∃V : set, V ∈ Ty ∧ y0 ∈ V ∧ setprod U0 V ⊆ N) U HU).
We prove the intermediate claim HKcov: K ⊆ ⋃ UFam.
Let x be given.
Assume HxK: x ∈ K.
We will prove x ∈ ⋃ UFam.
Set p to be the term (x,y0).
We prove the intermediate claim HpK: p ∈ setprod K {y0}.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K {y0} x y0 HxK (SingI y0)).
We prove the intermediate claim HpN: p ∈ N.
An exact proof term for the current goal is (HNsub p HpK).
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 {x} {y0}.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x} {y0} x y0 (SingI x) (SingI y0)).
We prove the intermediate claim Hcoords: x ∈ U0 ∧ y0 ∈ V0.
An exact proof term for the current goal is (setprod_coords_in x y0 U0 V0 p HpXY0 HpUV).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (andEL (x ∈ U0) (y0 ∈ V0) Hcoords).
We prove the intermediate claim HyV0: y0 ∈ V0.
An exact proof term for the current goal is (andER (x ∈ U0) (y0 ∈ 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 HU0Fam: U0 ∈ UFam.
Apply (SepI Tx (λU1 : set ⇒ ∃V1 : set, V1 ∈ Ty ∧ y0 ∈ V1 ∧ setprod U1 V1 ⊆ N) U0 HU0Tx) to the current goal.
We use V0 to witness the existential quantifier.
An exact proof term for the current goal is (andI (V0 ∈ Ty ∧ y0 ∈ V0) (setprod U0 V0 ⊆ N) (andI (V0 ∈ Ty) (y0 ∈ V0) HV0Ty HyV0) HrectSub).
An exact proof term for the current goal is (UnionI UFam x U0 HxU0 HU0Fam).
We prove the intermediate claim HKsubX': K ⊆ X.
An exact proof term for the current goal is HKsubX.
We prove the intermediate claim HKcover_prop: ∀Fam : set, (Fam ⊆ Tx ∧ K ⊆ ⋃ Fam) → has_finite_subcover K Tx Fam.
An exact proof term for the current goal is (iffEL (compact_space K (subspace_topology X Tx K)) (∀Fam : set, (Fam ⊆ Tx ∧ K ⊆ ⋃ Fam) → has_finite_subcover K Tx Fam) (compact_subspace_via_ambient_covers X Tx K HTx HKsubX') HKcomp).
We prove the intermediate claim Hfin: has_finite_subcover K Tx UFam.
An exact proof term for the current goal is (HKcover_prop UFam (andI (UFam ⊆ Tx) (K ⊆ ⋃ UFam) HUFamSubTx HKcov)).
Apply Hfin to the current goal.
Let G be given.
Assume HGtriple: G ⊆ UFam ∧ finite G ∧ K ⊆ ⋃ G.
We prove the intermediate claim HGsub: G ⊆ UFam.
An exact proof term for the current goal is (andEL (G ⊆ UFam) (finite G) (andEL (G ⊆ UFam ∧ finite G) (K ⊆ ⋃ G) HGtriple)).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ UFam) (finite G) (andEL (G ⊆ UFam ∧ finite G) (K ⊆ ⋃ G) HGtriple)).
We prove the intermediate claim HKcovG: K ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ UFam ∧ finite G) (K ⊆ ⋃ G) HGtriple).
Set pickV to be the term λU : set ⇒ Eps_i (λV : set ⇒ V ∈ Ty ∧ y0 ∈ V ∧ setprod U V ⊆ N).
We prove the intermediate claim HpickV: ∀U : set, U ∈ UFam → pickV U ∈ Ty ∧ y0 ∈ pickV U ∧ setprod U (pickV U) ⊆ N.
Let U be given.
Assume HU: U ∈ UFam.
We prove the intermediate claim Hex: ∃V : set, V ∈ Ty ∧ y0 ∈ V ∧ setprod U V ⊆ N.
An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ ∃V : set, V ∈ Ty ∧ y0 ∈ V ∧ setprod U0 V ⊆ N) U HU).
Apply Hex to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ Ty ∧ y0 ∈ V0 ∧ setprod U V0 ⊆ N.
An exact proof term for the current goal is (Eps_i_ax (λV : set ⇒ V ∈ Ty ∧ y0 ∈ V ∧ setprod U V ⊆ N) V0 HV0).
Set VFam to be the term {pickV U|U ∈ G}.
We prove the intermediate claim HVFamFin: finite VFam.
An exact proof term for the current goal is (Repl_finite (λU : set ⇒ pickV U) G HGfin).
We prove the intermediate claim HVFamPow: VFam ∈ 𝒫 Ty.
Apply PowerI Ty VFam to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ VFam.
We will prove V0 ∈ Ty.
Apply (ReplE_impred G (λU0 : set ⇒ pickV U0) V0 HV0) to the current goal.
Let U0 be given.
Assume HU0G: U0 ∈ G.
Assume HV0eq: V0 = pickV U0.
We prove the intermediate claim HU0Fam: U0 ∈ UFam.
An exact proof term for the current goal is (HGsub U0 HU0G).
We prove the intermediate claim Hprop: pickV U0 ∈ Ty ∧ y0 ∈ pickV U0 ∧ setprod U0 (pickV U0) ⊆ N.
An exact proof term for the current goal is (HpickV U0 HU0Fam).
We prove the intermediate claim Hab: pickV U0 ∈ Ty.
An exact proof term for the current goal is (andEL (pickV U0 ∈ Ty) (y0 ∈ pickV U0) (andEL (pickV U0 ∈ Ty ∧ y0 ∈ pickV U0) (setprod U0 (pickV U0) ⊆ N) Hprop)).
rewrite the current goal using HV0eq (from left to right).
An exact proof term for the current goal is Hab.
Set V to be the term intersection_of_family Y VFam.
We prove the intermediate claim HVinTy: V ∈ Ty.
An exact proof term for the current goal is (finite_intersection_in_topology Y Ty VFam HTy HVFamPow HVFamFin).
We prove the intermediate claim Hy0V: y0 ∈ V.
We will prove y0 ∈ intersection_of_family Y VFam.
We prove the intermediate claim Hall: ∀W : set, W ∈ VFam → y0 ∈ W.
Let W be given.
Assume HW: W ∈ VFam.
Apply (ReplE_impred G (λU0 : set ⇒ pickV U0) W HW) to the current goal.
Let U0 be given.
Assume HU0G: U0 ∈ G.
Assume HWeq: W = pickV U0.
We prove the intermediate claim HU0Fam: U0 ∈ UFam.
An exact proof term for the current goal is (HGsub U0 HU0G).
We prove the intermediate claim Hprop: pickV U0 ∈ Ty ∧ y0 ∈ pickV U0 ∧ setprod U0 (pickV U0) ⊆ N.
An exact proof term for the current goal is (HpickV U0 HU0Fam).
We prove the intermediate claim Hab: y0 ∈ pickV U0.
An exact proof term for the current goal is (andER (pickV U0 ∈ Ty) (y0 ∈ pickV U0) (andEL (pickV U0 ∈ Ty ∧ y0 ∈ pickV U0) (setprod U0 (pickV U0) ⊆ N) Hprop)).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is Hab.
An exact proof term for the current goal is (SepI Y (λy : set ⇒ ∀W : set, W ∈ VFam → y ∈ W) y0 Hy0Y Hall).
We prove the intermediate claim HVsubN: setprod K V ⊆ N.
Let p be given.
Assume Hp: p ∈ setprod K V.
We will prove p ∈ N.
We prove the intermediate claim Hp0: p 0 ∈ K.
An exact proof term for the current goal is (ap0_Sigma K (λ_ : set ⇒ V) p Hp).
We prove the intermediate claim Hp1: p 1 ∈ V.
An exact proof term for the current goal is (ap1_Sigma K (λ_ : set ⇒ V) p Hp).
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta K V p Hp).
We prove the intermediate claim Hp0InUnion: p 0 ∈ ⋃ G.
An exact proof term for the current goal is (HKcovG (p 0) Hp0).
Apply (UnionE_impred G (p 0) Hp0InUnion) to the current goal.
Let U0 be given.
Assume Hp0U0: p 0 ∈ U0.
Assume HU0G: U0 ∈ G.
We prove the intermediate claim HU0Fam: U0 ∈ UFam.
An exact proof term for the current goal is (HGsub U0 HU0G).
We prove the intermediate claim Hprop: pickV U0 ∈ Ty ∧ y0 ∈ pickV U0 ∧ setprod U0 (pickV U0) ⊆ N.
An exact proof term for the current goal is (HpickV U0 HU0Fam).
We prove the intermediate claim HrectSubN: setprod U0 (pickV U0) ⊆ N.
An exact proof term for the current goal is (andER (pickV U0 ∈ Ty ∧ y0 ∈ pickV U0) (setprod U0 (pickV U0) ⊆ N) Hprop).
We prove the intermediate claim Hp1Pick: p 1 ∈ pickV U0.
We prove the intermediate claim Hp1All: ∀W : set, W ∈ VFam → p 1 ∈ W.
An exact proof term for the current goal is (SepE2 Y (λy : set ⇒ ∀W : set, W ∈ VFam → y ∈ W) (p 1) Hp1).
We prove the intermediate claim Hmem: pickV U0 ∈ VFam.
An exact proof term for the current goal is (ReplI G (λU1 : set ⇒ pickV U1) U0 HU0G).
An exact proof term for the current goal is (Hp1All (pickV U0) Hmem).
We prove the intermediate claim HpairIn: (p 0,p 1) ∈ setprod U0 (pickV U0).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U0 (pickV U0) (p 0) (p 1) Hp0U0 Hp1Pick).
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 V to witness the existential quantifier.
An exact proof term for the current goal is (andI (V ∈ Ty ∧ y0 ∈ V) (setprod K V ⊆ N) (andI (V ∈ Ty) (y0 ∈ V) HVinTy Hy0V) HVsubN).
∎