Assume Hcomp: compact_space Y Ty.

We will prove ∀Fam : set, (Fam ⊆ Tx ∧ Y ⊆ ⋃ Fam) → has_finite_subcover Y Tx Fam.

Let Fam be given.

Assume Hcov: Fam ⊆ Tx ∧ Y ⊆ ⋃ Fam.

We prove the intermediate claim HFamSub: Fam ⊆ Tx.

An exact proof term for the current goal is (andEL (Fam ⊆ Tx) (Y ⊆ ⋃ Fam) Hcov).

We prove the intermediate claim HYcov: Y ⊆ ⋃ Fam.

An exact proof term for the current goal is (andER (Fam ⊆ Tx) (Y ⊆ ⋃ Fam) Hcov).

Set FamY to be the term {U ∩ Y|U ∈ Fam}.

We prove the intermediate claim HtopY: topology_on Y Ty.

An exact proof term for the current goal is (andEL (topology_on Y Ty) (∀Fam : set, open_cover_of Y Ty Fam → has_finite_subcover Y Ty Fam) Hcomp).

We prove the intermediate claim HcoverFamY: open_cover_of Y Ty FamY.

We will prove topology_on Y Ty ∧ FamY ⊆ 𝒫 Y ∧ Y ⊆ ⋃ FamY ∧ (∀U : set, U ∈ FamY → U ∈ Ty).

Apply andI to the current goal.

An exact proof term for the current goal is HtopY.

Let W be given.

Assume HW: W ∈ FamY.

We will prove W ∈ 𝒫 Y.

Apply (ReplE_impred Fam (λU : set ⇒ U ∩ Y) W HW) to the current goal.

Let U be given.

Assume HUfam: U ∈ Fam.

Assume HWeq: W = U ∩ Y.

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

Apply PowerI to the current goal.

An exact proof term for the current goal is (binintersect_Subq_2 U Y).

Let y be given.

Assume HyY: y ∈ Y.

We will prove y ∈ ⋃ FamY.

We prove the intermediate claim HyUnionFam: y ∈ ⋃ Fam.

An exact proof term for the current goal is (HYcov y HyY).

Apply (UnionE_impred Fam y HyUnionFam) to the current goal.

Let U be given.

Assume HyU: y ∈ U.

Assume HUfam: U ∈ Fam.

We will prove y ∈ ⋃ FamY.

Apply (UnionI FamY y (U ∩ Y)) to the current goal.

We will prove y ∈ U ∩ Y.

An exact proof term for the current goal is (binintersectI U Y y HyU HyY).

We will prove (U ∩ Y) ∈ FamY.

An exact proof term for the current goal is (ReplI Fam (λV : set ⇒ V ∩ Y) U HUfam).

Let W be given.

Assume HW: W ∈ FamY.

We will prove W ∈ Ty.

Apply (ReplE_impred Fam (λU : set ⇒ U ∩ Y) W HW) to the current goal.

Let U be given.

Assume HUfam: U ∈ Fam.

Assume HWeq: W = U ∩ Y.

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

An exact proof term for the current goal is (subspace_topologyI X Tx Y U (HFamSub U HUfam)).

We prove the intermediate claim Hsubcover: ∀Fam0 : set, open_cover_of Y Ty Fam0 → has_finite_subcover Y Ty Fam0.

An exact proof term for the current goal is (andER (topology_on Y Ty) (∀Fam0 : set, open_cover_of Y Ty Fam0 → has_finite_subcover Y Ty Fam0) Hcomp).

We prove the intermediate claim HfinY: has_finite_subcover Y Ty FamY.

An exact proof term for the current goal is (Hsubcover FamY HcoverFamY).

Apply HfinY to the current goal.

Let GY be given.

Assume HGY: GY ⊆ FamY ∧ finite GY ∧ Y ⊆ ⋃ GY.

We prove the intermediate claim HGYleft: GY ⊆ FamY ∧ finite GY.

An exact proof term for the current goal is (andEL (GY ⊆ FamY ∧ finite GY) (Y ⊆ ⋃ GY) HGY).

We prove the intermediate claim HGYsub: GY ⊆ FamY.

An exact proof term for the current goal is (andEL (GY ⊆ FamY) (finite GY) HGYleft).

We prove the intermediate claim HGYfin: finite GY.

An exact proof term for the current goal is (andER (GY ⊆ FamY) (finite GY) HGYleft).

We prove the intermediate claim HGYcov: Y ⊆ ⋃ GY.

An exact proof term for the current goal is (andER (GY ⊆ FamY ∧ finite GY) (Y ⊆ ⋃ GY) HGY).

Set pickU to be the term λW : set ⇒ Eps_i (λU : set ⇒ U ∈ Fam ∧ W = U ∩ Y).

Set G to be the term {pickU W|W ∈ GY}.

We will prove ∃G1 : set, G1 ⊆ Fam ∧ finite G1 ∧ Y ⊆ ⋃ G1.

We use G to witness the existential quantifier.

We will prove G ⊆ Fam ∧ finite G ∧ Y ⊆ ⋃ G.

Apply andI to the current goal.

Let U be given.

Assume HU: U ∈ G.

We will prove U ∈ Fam.

Apply (ReplE_impred GY (λW : set ⇒ pickU W) U HU) to the current goal.

Let W be given.

Assume HWGY: W ∈ GY.

Assume HeqU: U = pickU W.

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

We prove the intermediate claim HWFamY: W ∈ FamY.

An exact proof term for the current goal is (HGYsub W HWGY).

We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ Fam ∧ W = U0 ∩ Y.

Apply (ReplE_impred Fam (λU1 : set ⇒ U1 ∩ Y) W HWFamY) to the current goal.

Let U0 be given.

Assume HU0fam: U0 ∈ Fam.

Assume HW0: W = U0 ∩ Y.

We use U0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HU0fam.

An exact proof term for the current goal is HW0.

Apply HexU to the current goal.

Let U0 be given.

Assume HU0pair: U0 ∈ Fam ∧ W = U0 ∩ Y.

We prove the intermediate claim HU0: U0 ∈ Fam.

An exact proof term for the current goal is (andEL (U0 ∈ Fam) (W = U0 ∩ Y) HU0pair).

An exact proof term for the current goal is (andEL (pickU W ∈ Fam) (W = pickU W ∩ Y) (Eps_i_ax (λU1 : set ⇒ U1 ∈ Fam ∧ W = U1 ∩ Y) U0 HU0pair)).

An exact proof term for the current goal is (Repl_finite (λW : set ⇒ pickU W) GY HGYfin).

Let y be given.

Assume HyY: y ∈ Y.

We will prove y ∈ ⋃ G.

We prove the intermediate claim HyUGY: y ∈ ⋃ GY.

An exact proof term for the current goal is (HGYcov y HyY).

Apply (UnionE_impred GY y HyUGY) to the current goal.

Let W be given.

Assume HyW: y ∈ W.

Assume HWGY: W ∈ GY.

We will prove y ∈ ⋃ G.

We prove the intermediate claim HWFamY: W ∈ FamY.

An exact proof term for the current goal is (HGYsub W HWGY).

We prove the intermediate claim HexU: ∃U0 : set, U0 ∈ Fam ∧ W = U0 ∩ Y.

Apply (ReplE_impred Fam (λU1 : set ⇒ U1 ∩ Y) W HWFamY) to the current goal.

Let U0 be given.

Assume HU0fam: U0 ∈ Fam.

Assume HW0: W = U0 ∩ Y.

We use U0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HU0fam.

An exact proof term for the current goal is HW0.

We prove the intermediate claim Hpick: W = pickU W ∩ Y.

Apply HexU to the current goal.

Let U0 be given.

Assume HU0pair: U0 ∈ Fam ∧ W = U0 ∩ Y.

An exact proof term for the current goal is (andER (pickU W ∈ Fam) (W = pickU W ∩ Y) (Eps_i_ax (λU1 : set ⇒ U1 ∈ Fam ∧ W = U1 ∩ Y) U0 HU0pair)).

We prove the intermediate claim HyInPick: y ∈ pickU W.

We prove the intermediate claim HyWY: y ∈ pickU W ∩ Y.

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

An exact proof term for the current goal is HyW.

An exact proof term for the current goal is (binintersectE1 (pickU W) Y y HyWY).

An exact proof term for the current goal is (UnionI G y (pickU W) HyInPick (ReplI GY (λW0 : set ⇒ pickU W0) W HWGY)).

Assume Hprop: ∀Fam : set, (Fam ⊆ Tx ∧ Y ⊆ ⋃ Fam) → has_finite_subcover Y Tx Fam.

We will prove compact_space Y Ty.

We will prove topology_on Y Ty ∧ ∀Fam : set, open_cover_of Y Ty Fam → has_finite_subcover Y Ty Fam.

Apply andI to the current goal.

An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HY).

Let Fam0 be given.

Assume Hcov0: open_cover_of Y Ty Fam0.

We will prove has_finite_subcover Y Ty Fam0.

We prove the intermediate claim Hcov0_ABC: (topology_on Y Ty ∧ Fam0 ⊆ 𝒫 Y) ∧ Y ⊆ ⋃ Fam0.

An exact proof term for the current goal is (andEL ((topology_on Y Ty ∧ Fam0 ⊆ 𝒫 Y) ∧ Y ⊆ ⋃ Fam0) (∀U : set, U ∈ Fam0 → U ∈ Ty) Hcov0).

We prove the intermediate claim Hcov0_AB: topology_on Y Ty ∧ Fam0 ⊆ 𝒫 Y.

An exact proof term for the current goal is (andEL (topology_on Y Ty ∧ Fam0 ⊆ 𝒫 Y) (Y ⊆ ⋃ Fam0) Hcov0_ABC).

We prove the intermediate claim HF0subPow: Fam0 ⊆ 𝒫 Y.

An exact proof term for the current goal is (andER (topology_on Y Ty) (Fam0 ⊆ 𝒫 Y) Hcov0_AB).

We prove the intermediate claim HYcov0: Y ⊆ ⋃ Fam0.

An exact proof term for the current goal is (andER (topology_on Y Ty ∧ Fam0 ⊆ 𝒫 Y) (Y ⊆ ⋃ Fam0) Hcov0_ABC).

We prove the intermediate claim HF0open: ∀U : set, U ∈ Fam0 → U ∈ Ty.

An exact proof term for the current goal is (andER ((topology_on Y Ty ∧ Fam0 ⊆ 𝒫 Y) ∧ Y ⊆ ⋃ Fam0) (∀U : set, U ∈ Fam0 → U ∈ Ty) Hcov0).

Set Vof to be the term λW : set ⇒ Eps_i (λV : set ⇒ V ∈ Tx ∧ W = V ∩ Y).

Set Fam to be the term {Vof W|W ∈ Fam0}.

We prove the intermediate claim HFamSub: Fam ⊆ Tx.

Let V be given.

Assume HV: V ∈ Fam.

We will prove V ∈ Tx.

Apply (ReplE_impred Fam0 (λW : set ⇒ Vof W) V HV) to the current goal.

Let W be given.

Assume HW: W ∈ Fam0.

Assume HVeq: V = Vof W.

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

We prove the intermediate claim HexV: ∃V0 : set, V0 ∈ Tx ∧ W = V0 ∩ Y.

We prove the intermediate claim HWty: W ∈ Ty.

An exact proof term for the current goal is (HF0open W HW).

We prove the intermediate claim HWsub: W ∈ subspace_topology X Tx Y.

We prove the intermediate claim HdefTy: Ty = subspace_topology X Tx Y.

Use reflexivity.

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

An exact proof term for the current goal is HWty.

An exact proof term for the current goal is (subspace_topologyE X Tx Y W HWsub).

Apply HexV to the current goal.

Let V0 be given.

Assume HV0pair: V0 ∈ Tx ∧ W = V0 ∩ Y.

An exact proof term for the current goal is (andEL (Vof W ∈ Tx) (W = Vof W ∩ Y) (Eps_i_ax (λV1 : set ⇒ V1 ∈ Tx ∧ W = V1 ∩ Y) V0 HV0pair)).

We prove the intermediate claim HYcovFam: Y ⊆ ⋃ Fam.

Let y be given.

Assume HyY: y ∈ Y.

We will prove y ∈ ⋃ Fam.

We prove the intermediate claim HyUF0: y ∈ ⋃ Fam0.

An exact proof term for the current goal is (HYcov0 y HyY).

Apply (UnionE_impred Fam0 y HyUF0) to the current goal.

Let W be given.

Assume HyW: y ∈ W.

Assume HW: W ∈ Fam0.

We will prove y ∈ ⋃ Fam.

We prove the intermediate claim HyV: y ∈ Vof W.

We prove the intermediate claim HexV: ∃V0 : set, V0 ∈ Tx ∧ W = V0 ∩ Y.

We prove the intermediate claim HWty: W ∈ Ty.

An exact proof term for the current goal is (HF0open W HW).

We prove the intermediate claim HWsub: W ∈ subspace_topology X Tx Y.

We prove the intermediate claim HdefTy: Ty = subspace_topology X Tx Y.

Use reflexivity.

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

An exact proof term for the current goal is HWty.

An exact proof term for the current goal is (subspace_topologyE X Tx Y W HWsub).

We prove the intermediate claim Hpick: W = Vof W ∩ Y.

Apply HexV to the current goal.

Let V0 be given.

Assume HV0pair: V0 ∈ Tx ∧ W = V0 ∩ Y.

An exact proof term for the current goal is (andER (Vof W ∈ Tx) (W = Vof W ∩ Y) (Eps_i_ax (λV1 : set ⇒ V1 ∈ Tx ∧ W = V1 ∩ Y) V0 HV0pair)).

We prove the intermediate claim HyWY: y ∈ Vof W ∩ Y.

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

An exact proof term for the current goal is HyW.

An exact proof term for the current goal is (binintersectE1 (Vof W) Y y HyWY).

We prove the intermediate claim HVFam: (Vof W) ∈ Fam.

An exact proof term for the current goal is (ReplI Fam0 (λW0 : set ⇒ Vof W0) W HW).

An exact proof term for the current goal is (UnionI Fam y (Vof W) HyV HVFam).

We prove the intermediate claim Hfin: has_finite_subcover Y Tx Fam.

An exact proof term for the current goal is (Hprop Fam (andI (Fam ⊆ Tx) (Y ⊆ ⋃ Fam) HFamSub HYcovFam)).

Apply Hfin to the current goal.

Let G be given.

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

We prove the intermediate claim HGleft: G ⊆ Fam ∧ finite G.

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

We prove the intermediate claim HGsub: G ⊆ Fam.

An exact proof term for the current goal is (andEL (G ⊆ Fam) (finite G) HGleft).

We prove the intermediate claim HGfin: finite G.

An exact proof term for the current goal is (andER (G ⊆ Fam) (finite G) HGleft).

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

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

Set Wof to be the term λV : set ⇒ Eps_i (λW : set ⇒ W ∈ Fam0 ∧ V = Vof W).

Set G0 to be the term {Wof V|V ∈ G}.

We will prove ∃G1 : set, G1 ⊆ Fam0 ∧ finite G1 ∧ Y ⊆ ⋃ G1.

We use G0 to witness the existential quantifier.

We will prove G0 ⊆ Fam0 ∧ finite G0 ∧ Y ⊆ ⋃ G0.

Apply andI to the current goal.

Let W be given.

Assume HW: W ∈ G0.

We will prove W ∈ Fam0.

Apply (ReplE_impred G (λV : set ⇒ Wof V) W HW) to the current goal.

Let V be given.

Assume HVG: V ∈ G.

Assume HWof: W = Wof V.

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

We prove the intermediate claim HVFam: V ∈ Fam.

An exact proof term for the current goal is (HGsub V HVG).

We prove the intermediate claim HexW: ∃W0 : set, W0 ∈ Fam0 ∧ V = Vof W0.

Apply (ReplE_impred Fam0 (λW0 : set ⇒ Vof W0) V HVFam) to the current goal.

Let W0 be given.

Assume HW0: W0 ∈ Fam0.

Assume HVeq: V = Vof W0.

We use W0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HW0.

An exact proof term for the current goal is HVeq.

Apply HexW to the current goal.

Let W0 be given.

Assume HW0pair: W0 ∈ Fam0 ∧ V = Vof W0.

An exact proof term for the current goal is (andEL (Wof V ∈ Fam0) (V = Vof (Wof V)) (Eps_i_ax (λW1 : set ⇒ W1 ∈ Fam0 ∧ V = Vof W1) W0 HW0pair)).

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

Let y be given.

Assume HyY: y ∈ Y.

We will prove y ∈ ⋃ G0.

We prove the intermediate claim HyUG: y ∈ ⋃ G.

An exact proof term for the current goal is (HGcov y HyY).

Apply (UnionE_impred G y HyUG) to the current goal.

Let V be given.

Assume HyV: y ∈ V.

Assume HVG: V ∈ G.

We will prove y ∈ ⋃ G0.

We prove the intermediate claim HVFam: V ∈ Fam.

An exact proof term for the current goal is (HGsub V HVG).

We prove the intermediate claim HexW: ∃W0 : set, W0 ∈ Fam0 ∧ V = Vof W0.

Apply (ReplE_impred Fam0 (λW0 : set ⇒ Vof W0) V HVFam) to the current goal.

Let W0 be given.

Assume HW0: W0 ∈ Fam0.

Assume HVeq: V = Vof W0.

We use W0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HW0.

An exact proof term for the current goal is HVeq.

We prove the intermediate claim HVeq: V = Vof (Wof V).

Apply HexW to the current goal.

Let W0 be given.

Assume HW0pair: W0 ∈ Fam0 ∧ V = Vof W0.

An exact proof term for the current goal is (andER (Wof V ∈ Fam0) (V = Vof (Wof V)) (Eps_i_ax (λW1 : set ⇒ W1 ∈ Fam0 ∧ V = Vof W1) W0 HW0pair)).

We prove the intermediate claim HWty: (Wof V) ∈ Ty.

We prove the intermediate claim HWinFam0: (Wof V) ∈ Fam0.

Apply HexW to the current goal.

Let W0 be given.

Assume HW0pair: W0 ∈ Fam0 ∧ V = Vof W0.

An exact proof term for the current goal is (andEL (Wof V ∈ Fam0) (V = Vof (Wof V)) (Eps_i_ax (λW1 : set ⇒ W1 ∈ Fam0 ∧ V = Vof W1) W0 HW0pair)).

An exact proof term for the current goal is (HF0open (Wof V) HWinFam0).

We prove the intermediate claim HexV: ∃V0 : set, V0 ∈ Tx ∧ (Wof V) = V0 ∩ Y.

We prove the intermediate claim HWsub: (Wof V) ∈ subspace_topology X Tx Y.

We prove the intermediate claim HdefTy: Ty = subspace_topology X Tx Y.

Use reflexivity.

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

An exact proof term for the current goal is HWty.

An exact proof term for the current goal is (subspace_topologyE X Tx Y (Wof V) HWsub).

We prove the intermediate claim HWrepr: (Wof V) = (Vof (Wof V)) ∩ Y.

Apply HexV to the current goal.

Let V0 be given.

Assume HV0pair: V0 ∈ Tx ∧ (Wof V) = V0 ∩ Y.

An exact proof term for the current goal is (andER (Vof (Wof V) ∈ Tx) ((Wof V) = (Vof (Wof V)) ∩ Y) (Eps_i_ax (λV1 : set ⇒ V1 ∈ Tx ∧ (Wof V) = V1 ∩ Y) V0 HV0pair)).

We prove the intermediate claim HyInWof: y ∈ (Wof V).

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

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

An exact proof term for the current goal is (binintersectI V Y y HyV HyY).

An exact proof term for the current goal is (UnionI G0 y (Wof V) HyInWof (ReplI G (λV0 : set ⇒ Wof V0) V HVG)).