Let X, Tx, Y and f be given.
Assume HTx: topology_on X Tx.
Assume Hf: quotient_map X Tx Y f.
We will prove topology_on Y (quotient_topology X Tx Y f).
Set Q to be the term quotient_topology X Tx Y f.
Set pre to be the term λV : set ⇒ preimage_of X f V.
We will prove Q ⊆ 𝒫 Y ∧ Empty ∈ Q ∧ Y ∈ Q ∧ (∀UFam ∈ 𝒫 Q, ⋃ UFam ∈ Q) ∧ (∀U ∈ Q, ∀V ∈ Q, U ∩ V ∈ Q).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let V be given.
Assume HV: V ∈ Q.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) V HV).
We will prove Empty ∈ Q.
We prove the intermediate claim HpreE: pre Empty ∈ Tx.
Set Epre to be the term pre Empty.
We prove the intermediate claim HEsub: Epre ⊆ Empty.
Let x be given.
Assume Hx: x ∈ Epre.
We will prove x ∈ Empty.
We prove the intermediate claim Hxprop: apply_fun f x ∈ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ apply_fun f x0 ∈ Empty) x Hx).
An exact proof term for the current goal is (EmptyE (apply_fun f x) Hxprop (x ∈ Empty)).
We prove the intermediate claim HEeq: Epre = Empty.
An exact proof term for the current goal is (Empty_Subq_eq Epre HEsub).
rewrite the current goal using HEeq (from left to right).
An exact proof term for the current goal is (topology_has_empty X Tx HTx).
We prove the intermediate claim Hpow: Empty ∈ 𝒫 Y.
An exact proof term for the current goal is (Empty_In_Power Y).
An exact proof term for the current goal is (SepI (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) Empty Hpow HpreE).
We will prove Y ∈ Q.
We prove the intermediate claim Hf_on: function_on f X Y.
An exact proof term for the current goal is (andER (topology_on X Tx) (function_on f X Y) (andEL (topology_on X Tx ∧ function_on f X Y) (∀y : set, y ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y) Hf)).
We prove the intermediate claim HpreY: pre Y ∈ Tx.
Set Ypre to be the term pre Y.
We prove the intermediate claim HYsub: Ypre ⊆ X.
Let x be given.
Assume Hx: x ∈ Ypre.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ apply_fun f x0 ∈ Y) x Hx).
We prove the intermediate claim HXsub: X ⊆ Ypre.
Let x be given.
Assume Hx: x ∈ X.
We will prove x ∈ Ypre.
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hf_on x Hx).
An exact proof term for the current goal is (SepI X (λx0 ⇒ apply_fun f x0 ∈ Y) x Hx HfxY).
We prove the intermediate claim HYeq: Ypre = X.
Apply set_ext to the current goal.
An exact proof term for the current goal is HYsub.
An exact proof term for the current goal is HXsub.
rewrite the current goal using HYeq (from left to right).
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim Hpow: Y ∈ 𝒫 Y.
Apply PowerI to the current goal.
An exact proof term for the current goal is (λx Hx ⇒ Hx).
An exact proof term for the current goal is (SepI (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) Y Hpow HpreY).
Let UFam be given.
Assume HUFam: UFam ∈ 𝒫 Q.
We will prove ⋃ UFam ∈ Q.
We prove the intermediate claim HUFamSub: UFam ⊆ Q.
An exact proof term for the current goal is (PowerE Q UFam HUFam).
We prove the intermediate claim HUnionPow: ⋃ UFam ∈ 𝒫 Y.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ ⋃ UFam.
We will prove y ∈ Y.
Apply (UnionE_impred UFam y Hy) to the current goal.
Let V be given.
Assume HyV.
Assume HVUF.
We prove the intermediate claim HVQ: V ∈ Q.
An exact proof term for the current goal is (HUFamSub V HVUF).
We prove the intermediate claim HVPow: V ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) V HVQ).
An exact proof term for the current goal is (PowerE Y V HVPow y HyV).
We prove the intermediate claim HpreU: pre (⋃ UFam) ∈ Tx.
Set PUFam to be the term {pre V|V ∈ UFam}.
We prove the intermediate claim HPUFamPow: PUFam ∈ 𝒫 Tx.
Apply PowerI to the current goal.
Let W be given.
Assume HW: W ∈ PUFam.
We will prove W ∈ Tx.
Apply (ReplE UFam (λV : set ⇒ pre V) W HW) to the current goal.
Let V be given.
Assume HVconj.
We prove the intermediate claim HVUF: V ∈ UFam.
An exact proof term for the current goal is (andEL (V ∈ UFam) (W = pre V) HVconj).
We prove the intermediate claim HWeq: W = pre V.
An exact proof term for the current goal is (andER (V ∈ UFam) (W = pre V) HVconj).
We prove the intermediate claim HVQ: V ∈ Q.
An exact proof term for the current goal is (HUFamSub V HVUF).
We prove the intermediate claim HpreV: pre V ∈ Tx.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) V HVQ).
rewrite the current goal using HWeq (from left to right).
An exact proof term for the current goal is HpreV.
We prove the intermediate claim Heq: pre (⋃ UFam) = ⋃ PUFam.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ pre (⋃ UFam).
We will prove x ∈ ⋃ PUFam.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ apply_fun f x0 ∈ ⋃ UFam) x Hx).
We prove the intermediate claim HxU: apply_fun f x ∈ ⋃ UFam.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ apply_fun f x0 ∈ ⋃ UFam) x Hx).
Apply (UnionE_impred UFam (apply_fun f x) HxU) to the current goal.
Let V be given.
Assume HfxV.
Assume HVUF.
We prove the intermediate claim HxpreV: x ∈ pre V.
An exact proof term for the current goal is (SepI X (λx0 ⇒ apply_fun f x0 ∈ V) x HxX HfxV).
We prove the intermediate claim HpreVin: pre V ∈ PUFam.
An exact proof term for the current goal is (ReplI UFam (λV0 : set ⇒ pre V0) V HVUF).
An exact proof term for the current goal is (UnionI PUFam x (pre V) HxpreV HpreVin).
Let x be given.
Assume Hx: x ∈ ⋃ PUFam.
We will prove x ∈ pre (⋃ UFam).
Apply (UnionE_impred PUFam x Hx) to the current goal.
Let W be given.
Assume HxW.
Assume HWPU.
Apply (ReplE UFam (λV : set ⇒ pre V) W HWPU) to the current goal.
Let V be given.
Assume HVconj.
We prove the intermediate claim HVUF: V ∈ UFam.
An exact proof term for the current goal is (andEL (V ∈ UFam) (W = pre V) HVconj).
We prove the intermediate claim HWeq: W = pre V.
An exact proof term for the current goal is (andER (V ∈ UFam) (W = pre V) HVconj).
We prove the intermediate claim HxpreV: x ∈ pre V.
rewrite the current goal using HWeq (from right to left).
An exact proof term for the current goal is HxW.
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ apply_fun f x0 ∈ V) x HxpreV).
We prove the intermediate claim HfxU: apply_fun f x ∈ ⋃ UFam.
An exact proof term for the current goal is (UnionI UFam (apply_fun f x) V HfxV HVUF).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ apply_fun f x0 ∈ V) x HxpreV).
An exact proof term for the current goal is (SepI X (λx0 ⇒ apply_fun f x0 ∈ ⋃ UFam) x HxX HfxU).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_union_axiom X Tx HTx PUFam HPUFamPow).
An exact proof term for the current goal is (SepI (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) (⋃ UFam) HUnionPow HpreU).
Let U be given.
Assume HU: U ∈ Q.
Let V be given.
Assume HV: V ∈ Q.
We will prove U ∩ V ∈ Q.
We prove the intermediate claim HUPow: U ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) U HU).
We prove the intermediate claim HVPow: V ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) V HV).
We prove the intermediate claim HpreU: pre U ∈ Tx.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) U HU).
We prove the intermediate claim HpreV: pre V ∈ Tx.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) V HV).
We prove the intermediate claim HUVPow: U ∩ V ∈ 𝒫 Y.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ V.
We will prove y ∈ Y.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U V y Hy).
An exact proof term for the current goal is (PowerE Y U HUPow y HyU).
We prove the intermediate claim Heq: pre (U ∩ V) = pre U ∩ pre V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ pre (U ∩ V).
We will prove x ∈ pre U ∩ pre V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ apply_fun f x0 ∈ U ∩ V) x Hx).
We prove the intermediate claim Hfx: apply_fun f x ∈ U ∩ V.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ apply_fun f x0 ∈ U ∩ V) x Hx).
We prove the intermediate claim HfxU: apply_fun f x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V (apply_fun f x) Hfx).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V (apply_fun f x) Hfx).
An exact proof term for the current goal is (binintersectI (pre U) (pre V) x (SepI X (λx0 ⇒ apply_fun f x0 ∈ U) x HxX HfxU) (SepI X (λx0 ⇒ apply_fun f x0 ∈ V) x HxX HfxV)).
Let x be given.
Assume Hx: x ∈ pre U ∩ pre V.
We will prove x ∈ pre (U ∩ V).
We prove the intermediate claim HxpreU: x ∈ pre U.
An exact proof term for the current goal is (binintersectE1 (pre U) (pre V) x Hx).
We prove the intermediate claim HxpreV: x ∈ pre V.
An exact proof term for the current goal is (binintersectE2 (pre U) (pre V) x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 ⇒ apply_fun f x0 ∈ U) x HxpreU).
We prove the intermediate claim HfxU: apply_fun f x ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ apply_fun f x0 ∈ U) x HxpreU).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 ⇒ apply_fun f x0 ∈ V) x HxpreV).
We prove the intermediate claim HfxUV: apply_fun f x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V (apply_fun f x) HfxU HfxV).
An exact proof term for the current goal is (SepI X (λx0 ⇒ apply_fun f x0 ∈ U ∩ V) x HxX HfxUV).
We prove the intermediate claim HpreUV: pre (U ∩ V) ∈ Tx.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X Tx (pre U) (pre V) HTx HpreU HpreV).
An exact proof term for the current goal is (SepI (𝒫 Y) (λV0 : set ⇒ pre V0 ∈ Tx) (U ∩ V) HUVPow HpreUV).
∎