Let Cover be given.

Assume HCover: open_cover (setprod X Y) (product_topology X Tx Y Ty) Cover.

We will prove ∃V : set, countable_subcollection V Cover ∧ covers (setprod X Y) V.

We prove the intermediate claim HCoverOpen: ∀N0 : set, N0 ∈ Cover → N0 ∈ product_topology X Tx Y Ty.

An exact proof term for the current goal is (andEL (∀u : set, u ∈ Cover → u ∈ product_topology X Tx Y Ty) (covers (setprod X Y) Cover) HCover).

We prove the intermediate claim HCoverCovers: covers (setprod X Y) Cover.

An exact proof term for the current goal is (andER (∀u : set, u ∈ Cover → u ∈ product_topology X Tx Y Ty) (covers (setprod X Y) Cover) HCover).

Set UFam to be the term {U ∈ Tx|∃H : set, H ⊆ Cover ∧ finite H ∧ setprod U Y ⊆ ⋃ H}.

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 ⇒ ∃H : set, H ⊆ Cover ∧ finite H ∧ setprod U0 Y ⊆ ⋃ H) U HU).

We prove the intermediate claim HUFamCover: open_cover X Tx UFam.

We will prove (∀U : set, U ∈ UFam → U ∈ Tx) ∧ covers X UFam.

Apply andI to the current goal.

Let U be given.

Assume HU: U ∈ UFam.

An exact proof term for the current goal is (HUFamSubTx U HU).

We will prove covers X UFam.

Let x be given.

Assume Hx: x ∈ X.

We will prove ∃U : set, U ∈ UFam ∧ x ∈ U.

We prove the intermediate claim HexSlice: ∃H : set, H ⊆ Cover ∧ finite H ∧ setprod {x} Y ⊆ ⋃ H.

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).

Set VFam to be the term {V ∈ Ty|∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod U0 V ⊆ N0}.

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 ⇒ ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod U0 V0 ⊆ N0) V HV).

We prove the intermediate claim HTyPow: Ty ⊆ 𝒫 Y.

An exact proof term for the current goal is (topology_subset_axiom Y Ty HTy).

We prove the intermediate claim HVFamPow: 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 HYcovV: Y ⊆ ⋃ VFam.

Let y be given.

Assume Hy: y ∈ Y.

We will prove y ∈ ⋃ VFam.

Set p to be the term (x,y).

We prove the intermediate claim HpXY: p ∈ setprod X Y.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y x y Hx Hy).

Apply (HCoverCovers p HpXY) to the current goal.

Let N0 be given.

Assume HN0pair: N0 ∈ Cover ∧ p ∈ N0.

We prove the intermediate claim HN0Cover: N0 ∈ Cover.

An exact proof term for the current goal is (andEL (N0 ∈ Cover) (p ∈ N0) HN0pair).

We prove the intermediate claim HpN0: p ∈ N0.

An exact proof term for the current goal is (andER (N0 ∈ Cover) (p ∈ N0) HN0pair).

We prove the intermediate claim HN0Top: N0 ∈ generated_topology (setprod X Y) B.

An exact proof term for the current goal is (HCoverOpen N0 HN0Cover).

We prove the intermediate claim HN0refine: ∀q ∈ N0, ∃b ∈ B, q ∈ b ∧ b ⊆ N0.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λU0 : set ⇒ ∀q ∈ U0, ∃b ∈ B, q ∈ b ∧ b ⊆ U0) N0 HN0Top).

We prove the intermediate claim Hexb: ∃b ∈ B, p ∈ b ∧ b ⊆ N0.

An exact proof term for the current goal is (HN0refine p HpN0).

Apply Hexb 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 ⊆ N0) Hbpair).

We prove the intermediate claim Hbprop: p ∈ b ∧ b ⊆ N0.

An exact proof term for the current goal is (andER (b ∈ B) (p ∈ b ∧ b ⊆ N0) Hbpair).

We prove the intermediate claim Hpb: p ∈ b.

An exact proof term for the current goal is (andEL (p ∈ b) (b ⊆ N0) Hbprop).

We prove the intermediate claim HbsubN0: b ⊆ N0.

An exact proof term for the current goal is (andER (p ∈ b) (b ⊆ N0) 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} {y}.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x} {y} x y (SingI x) (SingI y)).

We prove the intermediate claim Hcoords: x ∈ U0 ∧ y ∈ V0.

An exact proof term for the current goal is (setprod_coords_in x y 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) (y ∈ V0) Hcoords).

We prove the intermediate claim HyV0: y ∈ V0.

An exact proof term for the current goal is (andER (x ∈ U0) (y ∈ V0) Hcoords).

We prove the intermediate claim HrectSub: setprod U0 V0 ⊆ N0.

rewrite the current goal using HbEq (from right to left) at position 1.

An exact proof term for the current goal is HbsubN0.

We prove the intermediate claim HV0Fam: V0 ∈ VFam.

Apply (SepI Ty (λV1 : set ⇒ ∃U1 : set, U1 ∈ Tx ∧ x ∈ U1 ∧ ∃N1 : set, N1 ∈ Cover ∧ setprod U1 V1 ⊆ N1) V0 HV0Ty) to the current goal.

We use U0 to witness the existential quantifier.

We will prove U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N1 : set, N1 ∈ Cover ∧ setprod U0 V0 ⊆ N1.

Apply andI to the current goal.

An exact proof term for the current goal is (andI (U0 ∈ Tx) (x ∈ U0) HU0Tx HxU0).

We use N0 to witness the existential quantifier.

An exact proof term for the current goal is (andI (N0 ∈ Cover) (setprod U0 V0 ⊆ N0) HN0Cover 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 ∧ (∀U0 : set, U0 ∈ VFam → U0 ∈ Ty).

Apply andI to the current goal.

An exact proof term for the current goal is HTy.

An exact proof term for the current goal is HVFamPow.

An exact proof term for the current goal is HYcovV.

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 HfinV: has_finite_subcover Y Ty VFam.

An exact proof term for the current goal is (Heine_Borel_subcover Y Ty VFam HY HVFamCover).

Apply HfinV to the current goal.

Let G be given.

Assume HG: G ⊆ VFam ∧ finite G ∧ Y ⊆ ⋃ G.

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) HG)).

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) HG)).

We prove the intermediate claim HYcovG: Y ⊆ ⋃ G.

An exact proof term for the current goal is (andER (G ⊆ VFam ∧ finite G) (Y ⊆ ⋃ G) HG).

Set pickU to be the term λV : set ⇒ Eps_i (λU0 : set ⇒ U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod U0 V ⊆ N0).

We prove the intermediate claim HpickU: ∀V : set, V ∈ VFam → pickU V ∈ Tx ∧ x ∈ pickU V ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod (pickU V) V ⊆ N0.

Let V be given.

Assume HV: V ∈ VFam.

We prove the intermediate claim Hex: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod U0 V ⊆ N0.

An exact proof term for the current goal is (SepE2 Ty (λV0 : set ⇒ ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod U0 V0 ⊆ N0) V HV).

Apply Hex to the current goal.

Let U0 be given.

Assume HU0: U0 ∈ Tx ∧ x ∈ U0 ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod U0 V ⊆ N0.

An exact proof term for the current goal is (Eps_i_ax (λU1 : set ⇒ U1 ∈ Tx ∧ x ∈ U1 ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod U1 V ⊆ N0) U0 HU0).

Set pickN to be the term λV : set ⇒ Eps_i (λN0 : set ⇒ N0 ∈ Cover ∧ setprod (pickU V) V ⊆ N0).

We prove the intermediate claim HpickN: ∀V : set, V ∈ VFam → pickN V ∈ Cover ∧ setprod (pickU V) V ⊆ pickN V.

Let V be given.

Assume HV: V ∈ VFam.

We prove the intermediate claim Hprop: pickU V ∈ Tx ∧ x ∈ pickU V ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod (pickU V) V ⊆ N0.

An exact proof term for the current goal is (HpickU V HV).

We prove the intermediate claim HexN: ∃N0 : set, N0 ∈ Cover ∧ setprod (pickU V) V ⊆ N0.

An exact proof term for the current goal is (andER (pickU V ∈ Tx ∧ x ∈ pickU V) (∃N0 : set, N0 ∈ Cover ∧ setprod (pickU V) V ⊆ N0) Hprop).

Apply HexN to the current goal.

Let N0 be given.

Assume HN0: N0 ∈ Cover ∧ setprod (pickU V) V ⊆ N0.

An exact proof term for the current goal is (Eps_i_ax (λN1 : set ⇒ N1 ∈ Cover ∧ setprod (pickU V) V ⊆ N1) N0 HN0).

Set H to be the term {pickN V|V ∈ G}.

We use H to witness the existential quantifier.

Apply andI to the current goal.

We will prove H ⊆ Cover.

Let N0 be given.

Assume HN0: N0 ∈ H.

Apply (ReplE_impred G (λV0 : set ⇒ pickN V0) N0 HN0) to the current goal.

Let V0 be given.

Assume HV0G: V0 ∈ G.

Assume HN0Eq: N0 = pickN 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 HNprop: pickN V0 ∈ Cover ∧ setprod (pickU V0) V0 ⊆ pickN V0.

An exact proof term for the current goal is (HpickN V0 HV0Fam).

We prove the intermediate claim HN0Cover: pickN V0 ∈ Cover.

An exact proof term for the current goal is (andEL (pickN V0 ∈ Cover) (setprod (pickU V0) V0 ⊆ pickN V0) HNprop).

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

An exact proof term for the current goal is HN0Cover.

An exact proof term for the current goal is (Repl_finite (λV0 : set ⇒ pickN V0) G HGfin).

We will prove setprod {x} Y ⊆ ⋃ H.

Let p be given.

Assume Hp: p ∈ setprod {x} Y.

We will prove p ∈ ⋃ H.

We prove the intermediate claim Hp0: p 0 ∈ {x}.

An exact proof term for the current goal is (ap0_Sigma {x} (λ_ : set ⇒ Y) p Hp).

We prove the intermediate claim Hp1: p 1 ∈ Y.

An exact proof term for the current goal is (ap1_Sigma {x} (λ_ : set ⇒ Y) p Hp).

We prove the intermediate claim Hp0eq: p 0 = x.

An exact proof term for the current goal is (SingE x (p 0) Hp0).

We prove the intermediate claim HpEta: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta {x} 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 HUN: pickU V0 ∈ Tx ∧ x ∈ pickU V0 ∧ ∃N0 : set, N0 ∈ Cover ∧ setprod (pickU V0) V0 ⊆ N0.

An exact proof term for the current goal is (HpickU V0 HV0Fam).

We prove the intermediate claim HUNAB: pickU V0 ∈ Tx ∧ x ∈ pickU V0.

An exact proof term for the current goal is (andEL (pickU V0 ∈ Tx ∧ x ∈ pickU V0) (∃N0 : set, N0 ∈ Cover ∧ setprod (pickU V0) V0 ⊆ N0) HUN).

We prove the intermediate claim HxU: x ∈ pickU V0.

An exact proof term for the current goal is (andER (pickU V0 ∈ Tx) (x ∈ pickU V0) HUNAB).

We prove the intermediate claim HpInRect: (x,p 1) ∈ setprod (pickU V0) V0.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (pickU V0) V0 x (p 1) HxU Hp1V0).

We prove the intermediate claim HrectSub: setprod (pickU V0) V0 ⊆ pickN V0.

An exact proof term for the current goal is (andER (pickN V0 ∈ Cover) (setprod (pickU V0) V0 ⊆ pickN V0) (HpickN V0 HV0Fam)).

We prove the intermediate claim HpInN: (x,p 1) ∈ pickN V0.

An exact proof term for the current goal is (HrectSub (x,p 1) HpInRect).

We prove the intermediate claim HNinH: pickN V0 ∈ H.

An exact proof term for the current goal is (ReplI G (λV1 : set ⇒ pickN V1) V0 HV0G).

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

rewrite the current goal using Hp0eq (from left to right) at position 1.

An exact proof term for the current goal is (UnionI H (x,p 1) (pickN V0) HpInN HNinH).

Apply HexSlice to the current goal.

Let H be given.

Assume HH: H ⊆ Cover ∧ finite H ∧ setprod {x} Y ⊆ ⋃ H.

We prove the intermediate claim HHsub: H ⊆ Cover.

An exact proof term for the current goal is (andEL (H ⊆ Cover) (finite H) (andEL (H ⊆ Cover ∧ finite H) (setprod {x} Y ⊆ ⋃ H) HH)).

We prove the intermediate claim HHfin: finite H.

An exact proof term for the current goal is (andER (H ⊆ Cover) (finite H) (andEL (H ⊆ Cover ∧ finite H) (setprod {x} Y ⊆ ⋃ H) HH)).

We prove the intermediate claim HHcov: setprod {x} Y ⊆ ⋃ H.

An exact proof term for the current goal is (andER (H ⊆ Cover ∧ finite H) (setprod {x} Y ⊆ ⋃ H) HH).

We prove the intermediate claim HHsubTop: H ⊆ product_topology X Tx Y Ty.

Let N0 be given.

Assume HN0: N0 ∈ H.

We prove the intermediate claim HN0Cover: N0 ∈ Cover.

An exact proof term for the current goal is (HHsub N0 HN0).

An exact proof term for the current goal is (HCoverOpen N0 HN0Cover).

We prove the intermediate claim HtopProd: topology_on (setprod X Y) (product_topology X Tx Y Ty).

An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).

We prove the intermediate claim HNtop: ⋃ H ∈ product_topology X Tx Y Ty.

An exact proof term for the current goal is (topology_union_closed (setprod X Y) (product_topology X Tx Y Ty) H HtopProd HHsubTop).

We prove the intermediate claim Htube: ∃U : set, U ∈ Tx ∧ x ∈ U ∧ setprod U Y ⊆ ⋃ H.

An exact proof term for the current goal is (tube_lemma X Tx Y Ty HTx HTy HY x Hx (⋃ H) (andI ((⋃ H) ∈ product_topology X Tx Y Ty) (setprod {x} Y ⊆ ⋃ H) HNtop HHcov)).

Apply Htube to the current goal.

Let U be given.

Assume HU: U ∈ Tx ∧ x ∈ U ∧ setprod U Y ⊆ ⋃ H.

We prove the intermediate claim HUAB: U ∈ Tx ∧ x ∈ U.

An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x ∈ U) (setprod U Y ⊆ ⋃ H) HU).

We prove the intermediate claim HUtx: U ∈ Tx.

An exact proof term for the current goal is (andEL (U ∈ Tx) (x ∈ U) HUAB).

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (andER (U ∈ Tx) (x ∈ U) HUAB).

We prove the intermediate claim HUcov: setprod U Y ⊆ ⋃ H.

An exact proof term for the current goal is (andER (U ∈ Tx ∧ x ∈ U) (setprod U Y ⊆ ⋃ H) HU).

We use U to witness the existential quantifier.

Apply andI to the current goal.

Apply (SepI Tx (λU0 : set ⇒ ∃H0 : set, H0 ⊆ Cover ∧ finite H0 ∧ setprod U0 Y ⊆ ⋃ H0) U HUtx) to the current goal.

We use H to witness the existential quantifier.

An exact proof term for the current goal is (andI (H ⊆ Cover ∧ finite H) (setprod U Y ⊆ ⋃ H) (andI (H ⊆ Cover) (finite H) HHsub HHfin) HUcov).

An exact proof term for the current goal is HxU.

We prove the intermediate claim HW: ∃W : set, countable_subcollection W UFam ∧ covers X W.

An exact proof term for the current goal is (HXprop UFam HUFamCover).

Apply HW to the current goal.

Let W be given.

Assume HWpair: countable_subcollection W UFam ∧ covers X W.

We prove the intermediate claim HWsub: W ⊆ UFam.

An exact proof term for the current goal is (andEL (W ⊆ UFam) (countable_set W) (andEL (W ⊆ UFam ∧ countable_set W) (covers X W) HWpair)).

We prove the intermediate claim HWcount: countable_set W.

An exact proof term for the current goal is (andER (W ⊆ UFam) (countable_set W) (andEL (W ⊆ UFam ∧ countable_set W) (covers X W) HWpair)).

We prove the intermediate claim HWcov: covers X W.

An exact proof term for the current goal is (andER (W ⊆ UFam ∧ countable_set W) (covers X W) HWpair).

Set pickH to be the term λU : set ⇒ Eps_i (λH : set ⇒ H ⊆ Cover ∧ finite H ∧ setprod U Y ⊆ ⋃ H).

We prove the intermediate claim HpickH: ∀U : set, U ∈ W → pickH U ⊆ Cover ∧ finite (pickH U) ∧ setprod U Y ⊆ ⋃ (pickH U).

Let U be given.

Assume HU: U ∈ W.

We prove the intermediate claim HUFam: U ∈ UFam.

An exact proof term for the current goal is (HWsub U HU).

We prove the intermediate claim Hex: ∃H : set, H ⊆ Cover ∧ finite H ∧ setprod U Y ⊆ ⋃ H.

An exact proof term for the current goal is (SepE2 Tx (λU0 : set ⇒ ∃H : set, H ⊆ Cover ∧ finite H ∧ setprod U0 Y ⊆ ⋃ H) U HUFam).

Apply Hex to the current goal.

Let H0 be given.

Assume HH0: H0 ⊆ Cover ∧ finite H0 ∧ setprod U Y ⊆ ⋃ H0.

An exact proof term for the current goal is (Eps_i_ax (λH : set ⇒ H ⊆ Cover ∧ finite H ∧ setprod U Y ⊆ ⋃ H) H0 HH0).

Set P to be the term ∑U ∈ W, pickH U.

Set V to be the term {z 1|z ∈ P}.

We use V to witness the existential quantifier.

Apply andI to the current goal.

We will prove countable_subcollection V Cover.

We will prove V ⊆ Cover ∧ countable_set V.

Apply andI to the current goal.

Let N be given.

Assume HN: N ∈ V.

We will prove N ∈ Cover.

Apply (ReplE_impred P (λz : set ⇒ z 1) N HN) to the current goal.

Let z be given.

Assume HzP: z ∈ P.

Assume HNeq: N = z 1.

We prove the intermediate claim Hz0W: z 0 ∈ W.

An exact proof term for the current goal is (ap0_Sigma W (λU0 : set ⇒ pickH U0) z HzP).

We prove the intermediate claim Hz1In: z 1 ∈ pickH (z 0).

An exact proof term for the current goal is (ap1_Sigma W (λU0 : set ⇒ pickH U0) z HzP).

We prove the intermediate claim Hpick: pickH (z 0) ⊆ Cover.

An exact proof term for the current goal is (andEL (pickH (z 0) ⊆ Cover) (finite (pickH (z 0))) (andEL (pickH (z 0) ⊆ Cover ∧ finite (pickH (z 0))) (setprod (z 0) Y ⊆ ⋃ (pickH (z 0))) (HpickH (z 0) Hz0W))).

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

An exact proof term for the current goal is (Hpick (z 1) Hz1In).

We prove the intermediate claim HcountPick: ∀U : set, U ∈ W → countable (pickH U).

Let U be given.

Assume HU: U ∈ W.

We prove the intermediate claim Hfin: finite (pickH U).

An exact proof term for the current goal is (andER (pickH U ⊆ Cover) (finite (pickH U)) (andEL (pickH U ⊆ Cover ∧ finite (pickH U)) (setprod U Y ⊆ ⋃ (pickH U)) (HpickH U HU))).

An exact proof term for the current goal is (finite_countable (pickH U) Hfin).

We prove the intermediate claim HPcount: countable_set P.

An exact proof term for the current goal is (Sigma_countable W HWcount (λU0 : set ⇒ pickH U0) HcountPick).

An exact proof term for the current goal is (countable_image P HPcount (λz : set ⇒ z 1)).

We will prove covers (setprod X Y) V.

Let p be given.

Assume Hp: p ∈ setprod X Y.

We will prove ∃N : set, N ∈ V ∧ p ∈ N.

We prove the intermediate claim Hp0: p 0 ∈ X.

An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ Y) p Hp).

We prove the intermediate claim Hp1: p 1 ∈ Y.

An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ Y) p Hp).

Apply (HWcov (p 0) Hp0) to the current goal.

Let U be given.

Assume HUWpair: U ∈ W ∧ p 0 ∈ U.

We prove the intermediate claim HUW: U ∈ W.

An exact proof term for the current goal is (andEL (U ∈ W) (p 0 ∈ U) HUWpair).

We prove the intermediate claim Hp0U: p 0 ∈ U.

An exact proof term for the current goal is (andER (U ∈ W) (p 0 ∈ U) HUWpair).

We prove the intermediate claim HUpow: U ∈ 𝒫 X.

An exact proof term for the current goal is (topology_subset_axiom X Tx HTx U (HUFamSubTx U (HWsub U HUW))).

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (PowerE X U HUpow).

We prove the intermediate claim HpUY: p ∈ setprod U Y.

We prove the intermediate claim HpEta: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta X Y p Hp).

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 (p 0) (p 1) Hp0U Hp1).

We prove the intermediate claim HcovUY: setprod U Y ⊆ ⋃ (pickH U).

An exact proof term for the current goal is (andER (pickH U ⊆ Cover ∧ finite (pickH U)) (setprod U Y ⊆ ⋃ (pickH U)) (HpickH U HUW)).

We prove the intermediate claim HpInUnion: p ∈ ⋃ (pickH U).

An exact proof term for the current goal is (HcovUY p HpUY).

Apply (UnionE_impred (pickH U) p HpInUnion) to the current goal.

Let N be given.

Assume HpN: p ∈ N.

Assume HNin: N ∈ pickH U.

We use N to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HzP: (U,N) ∈ P.

An exact proof term for the current goal is (tuple_2_Sigma W (λU0 : set ⇒ pickH U0) U HUW N HNin).

We prove the intermediate claim Htup1: (U,N) 1 = N.

An exact proof term for the current goal is (tuple_2_1_eq U N).

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

An exact proof term for the current goal is (ReplI P (λz : set ⇒ z 1) (U,N) HzP).

An exact proof term for the current goal is HpN.