Let X, Tx, Y, Ty and f be given.
Assume Hcomp: compact_space X Tx.
Assume Hf: continuous_map X Tx Y Ty f.
We will prove compact_space (image_of_fun f X) (subspace_topology Y Ty (image_of_fun f X)).
Set Img to be the term image_of_fun f X.
Set Timg to be the term subspace_topology Y Ty Img.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
We prove the intermediate claim HsubcoverX: ∀Fam : set, open_cover_of X Tx Fam → has_finite_subcover X Tx Fam.
An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp).
We prove the intermediate claim Hf_left: ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) ∧ (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx).
An exact proof term for the current goal is Hf.
We prove the intermediate claim Hf_mid: (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y.
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf_left).
We prove the intermediate claim Hf_pre: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (andER ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf_left).
We prove the intermediate claim HtopXY: topology_on X Tx ∧ topology_on Y Ty.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Hf_mid).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andER (topology_on X Tx) (topology_on Y Ty) HtopXY).
We prove the intermediate claim Hfun: function_on f X Y.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Hf_mid).
We prove the intermediate claim HImgSubY: Img ⊆ Y.
Let y be given.
Assume Hy: y ∈ Img.
Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) y Hy) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume Heq: y = apply_fun f x0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Hfun x0 Hx0X).
We prove the intermediate claim Hprop: ∀Fam : set, (Fam ⊆ Ty ∧ Img ⊆ ⋃ Fam) → has_finite_subcover Img Ty Fam.
Let Fam be given.
Assume Hcov: Fam ⊆ Ty ∧ Img ⊆ ⋃ Fam.
We prove the intermediate claim HFamSub: Fam ⊆ Ty.
An exact proof term for the current goal is (andEL (Fam ⊆ Ty) (Img ⊆ ⋃ Fam) Hcov).
We prove the intermediate claim HImgCov: Img ⊆ ⋃ Fam.
An exact proof term for the current goal is (andER (Fam ⊆ Ty) (Img ⊆ ⋃ Fam) Hcov).
Set PreFam to be the term {preimage_of X f V|V ∈ Fam}.
We prove the intermediate claim HPrePow: PreFam ⊆ 𝒫 X.
Let W be given.
Assume HW: W ∈ PreFam.
Apply (ReplE_impred Fam (λV0 : set ⇒ preimage_of X f V0) W HW) to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ Fam.
Assume HWeq: W = preimage_of X f V0.
rewrite the current goal using HWeq (from left to right).
We will prove preimage_of X f V0 ∈ 𝒫 X.
Apply PowerI to the current goal.
Let x0 be given.
Assume Hx0: x0 ∈ preimage_of X f V0.
Apply (SepE X (λu : set ⇒ apply_fun f u ∈ V0) x0 Hx0) to the current goal.
Assume Hx0X.
Assume _.
An exact proof term for the current goal is Hx0X.
We prove the intermediate claim HPreOpen: ∀W : set, W ∈ PreFam → W ∈ Tx.
Let W be given.
Assume HW: W ∈ PreFam.
Apply (ReplE_impred Fam (λV0 : set ⇒ preimage_of X f V0) W HW) to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ Fam.
Assume HWeq: W = preimage_of X f V0.
We prove the intermediate claim HV0Ty: V0 ∈ Ty.
An exact proof term for the current goal is (HFamSub V0 HV0).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is (Hf_pre V0 HV0Ty).
We prove the intermediate claim HXcov: X ⊆ ⋃ PreFam.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
We will prove x0 ∈ ⋃ PreFam.
We prove the intermediate claim HyImg: apply_fun f x0 ∈ Img.
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ apply_fun f x1) x0 Hx0X).
We prove the intermediate claim HyUnion: apply_fun f x0 ∈ ⋃ Fam.
An exact proof term for the current goal is (HImgCov (apply_fun f x0) HyImg).
Apply (UnionE_impred Fam (apply_fun f x0) HyUnion) to the current goal.
Let V0 be given.
Assume HyV0: apply_fun f x0 ∈ V0.
Assume HV0: V0 ∈ Fam.
We prove the intermediate claim Hx0Pre: x0 ∈ preimage_of X f V0.
We will prove x0 ∈ {u ∈ X|apply_fun f u ∈ V0}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hx0X.
An exact proof term for the current goal is HyV0.
An exact proof term for the current goal is (UnionI PreFam x0 (preimage_of X f V0) Hx0Pre (ReplI Fam (λV1 : set ⇒ preimage_of X f V1) V0 HV0)).
We prove the intermediate claim HopenCov: open_cover_of X Tx PreFam.
We will prove topology_on X Tx ∧ PreFam ⊆ 𝒫 X ∧ X ⊆ ⋃ PreFam ∧ (∀U : set, U ∈ PreFam → U ∈ Tx).
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 HTx.
An exact proof term for the current goal is HPrePow.
An exact proof term for the current goal is HXcov.
An exact proof term for the current goal is HPreOpen.
We prove the intermediate claim HfinPre: has_finite_subcover X Tx PreFam.
An exact proof term for the current goal is (HsubcoverX PreFam HopenCov).
Apply HfinPre to the current goal.
Let Gpre be given.
Assume HGpre: Gpre ⊆ PreFam ∧ finite Gpre ∧ X ⊆ ⋃ Gpre.
We prove the intermediate claim HGpreLeft: Gpre ⊆ PreFam ∧ finite Gpre.
An exact proof term for the current goal is (andEL (Gpre ⊆ PreFam ∧ finite Gpre) (X ⊆ ⋃ Gpre) HGpre).
We prove the intermediate claim HGpreSub: Gpre ⊆ PreFam.
An exact proof term for the current goal is (andEL (Gpre ⊆ PreFam) (finite Gpre) HGpreLeft).
We prove the intermediate claim HGpreFin: finite Gpre.
An exact proof term for the current goal is (andER (Gpre ⊆ PreFam) (finite Gpre) HGpreLeft).
We prove the intermediate claim HXcovGpre: X ⊆ ⋃ Gpre.
An exact proof term for the current goal is (andER (Gpre ⊆ PreFam ∧ finite Gpre) (X ⊆ ⋃ Gpre) HGpre).
Set pickV to be the term λW : set ⇒ Eps_i (λV0 : set ⇒ V0 ∈ Fam ∧ W = preimage_of X f V0).
Set G to be the term {pickV W|W ∈ Gpre}.
We prove the intermediate claim HGsubFam: G ⊆ Fam.
Let V0 be given.
Assume HV0: V0 ∈ G.
Apply (ReplE_impred Gpre (λW0 : set ⇒ pickV W0) V0 HV0) to the current goal.
Let W0 be given.
Assume HW0G: W0 ∈ Gpre.
Assume HV0eq: V0 = pickV W0.
We prove the intermediate claim HW0Pre: W0 ∈ PreFam.
An exact proof term for the current goal is (HGpreSub W0 HW0G).
We prove the intermediate claim Hex: ∃V1 : set, V1 ∈ Fam ∧ W0 = preimage_of X f V1.
Apply (ReplE_impred Fam (λV2 : set ⇒ preimage_of X f V2) W0 HW0Pre) to the current goal.
Let V2 be given.
Assume HV2: V2 ∈ Fam.
Assume HW0eq2: W0 = preimage_of X f V2.
We use V2 to witness the existential quantifier.
An exact proof term for the current goal is (andI (V2 ∈ Fam) (W0 = preimage_of X f V2) HV2 HW0eq2).
Apply Hex to the current goal.
Let V1 be given.
Assume HV1: V1 ∈ Fam ∧ W0 = preimage_of X f V1.
We prove the intermediate claim Hpick: pickV W0 ∈ Fam ∧ W0 = preimage_of X f (pickV W0).
An exact proof term for the current goal is (Eps_i_ax (λV : set ⇒ V ∈ Fam ∧ W0 = preimage_of X f V) V1 HV1).
rewrite the current goal using HV0eq (from left to right).
An exact proof term for the current goal is (andEL (pickV W0 ∈ Fam) (W0 = preimage_of X f (pickV W0)) Hpick).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (Repl_finite (λW0 : set ⇒ pickV W0) Gpre HGpreFin).
We prove the intermediate claim HImgCovG: Img ⊆ ⋃ G.
Let y be given.
Assume Hy: y ∈ Img.
We will prove y ∈ ⋃ G.
Apply (ReplE_impred X (λx0 : set ⇒ apply_fun f x0) y Hy) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume Heq: y = apply_fun f x0.
We prove the intermediate claim Hx0UG: x0 ∈ ⋃ Gpre.
An exact proof term for the current goal is (HXcovGpre x0 Hx0X).
Apply (UnionE_impred Gpre x0 Hx0UG) to the current goal.
Let W0 be given.
Assume Hx0W0: x0 ∈ W0.
Assume HW0G: W0 ∈ Gpre.
We prove the intermediate claim HW0Pre: W0 ∈ PreFam.
An exact proof term for the current goal is (HGpreSub W0 HW0G).
We prove the intermediate claim Hex: ∃V1 : set, V1 ∈ Fam ∧ W0 = preimage_of X f V1.
Apply (ReplE_impred Fam (λV2 : set ⇒ preimage_of X f V2) W0 HW0Pre) to the current goal.
Let V2 be given.
Assume HV2: V2 ∈ Fam.
Assume HW0eq2: W0 = preimage_of X f V2.
We use V2 to witness the existential quantifier.
An exact proof term for the current goal is (andI (V2 ∈ Fam) (W0 = preimage_of X f V2) HV2 HW0eq2).
Apply Hex to the current goal.
Let V1 be given.
Assume HV1: V1 ∈ Fam ∧ W0 = preimage_of X f V1.
We prove the intermediate claim Hpick: pickV W0 ∈ Fam ∧ W0 = preimage_of X f (pickV W0).
An exact proof term for the current goal is (Eps_i_ax (λV : set ⇒ V ∈ Fam ∧ W0 = preimage_of X f V) V1 HV1).
We prove the intermediate claim HW0eq: W0 = preimage_of X f (pickV W0).
An exact proof term for the current goal is (andER (pickV W0 ∈ Fam) (W0 = preimage_of X f (pickV W0)) Hpick).
We prove the intermediate claim Hx0Pre: x0 ∈ preimage_of X f (pickV W0).
rewrite the current goal using HW0eq (from right to left) at position 1.
An exact proof term for the current goal is Hx0W0.
We prove the intermediate claim HyV: apply_fun f x0 ∈ pickV W0.
Apply (SepE X (λu : set ⇒ apply_fun f u ∈ pickV W0) x0 Hx0Pre) to the current goal.
Assume _.
Assume Hy0.
An exact proof term for the current goal is Hy0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (UnionI G (apply_fun f x0) (pickV W0) HyV (ReplI Gpre (λW1 : set ⇒ pickV W1) W0 HW0G)).
An exact proof term for the current goal is (has_finite_subcoverI Img Ty Fam G (andI (G ⊆ Fam ∧ finite G) (Img ⊆ ⋃ G) (andI (G ⊆ Fam) (finite G) HGsubFam HGfin) HImgCovG)).
An exact proof term for the current goal is (iffER (compact_space Img Timg) (∀Fam : set, (Fam ⊆ Ty ∧ Img ⊆ ⋃ Fam) → has_finite_subcover Img Ty Fam) (compact_subspace_via_ambient_covers Y Ty Img HTy HImgSubY) Hprop).
∎