Let X, Tx, Y and f be given.
Assume Hquot: quotient_map X Tx Y f.
Assume Hloc: locally_connected X Tx.
We will prove locally_connected Y (quotient_topology X Tx Y f).
Set Q to be the term quotient_topology X Tx Y f.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_connected_topology X Tx Hloc).
We prove the intermediate claim HTyQ: topology_on Y Q.
An exact proof term for the current goal is (quotient_topology_is_topology X Tx Y f HTx Hquot).
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) (function_on f X Y) (andEL (topology_on X Tx ∧ function_on f X Y) (∀y0 : set, y0 ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y0) Hquot)).
We prove the intermediate claim Hsurj: ∀y0 : set, y0 ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y0.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ function_on f X Y) (∀y0 : set, y0 ∈ Y → ∃x : set, x ∈ X ∧ apply_fun f x = y0) Hquot).
We prove the intermediate claim Hcont: continuous_map X Tx Y Q f.
We will prove topology_on X Tx ∧ topology_on Y Q ∧ function_on f X Y ∧ ∀W : set, W ∈ Q → preimage_of X f W ∈ 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 HTyQ.
An exact proof term for the current goal is Hfun.
Let W be given.
Assume HW: W ∈ Q.
We prove the intermediate claim Hraw: {x0 ∈ X|apply_fun f x0 ∈ W} ∈ Tx.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λV0 : set ⇒ {x0 ∈ X|apply_fun f x0 ∈ V0} ∈ Tx) W HW).
We prove the intermediate claim Heq: preimage_of X f W = {x0 ∈ X|apply_fun f x0 ∈ W}.
Use reflexivity.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hraw.
We will prove topology_on Y Q ∧ ∀y : set, y ∈ Y → ∀U : set, U ∈ Q → y ∈ U → ∃V : set, V ∈ Q ∧ y ∈ V ∧ V ⊆ U ∧ connected_space V (subspace_topology Y Q V).
Apply andI to the current goal.
An exact proof term for the current goal is HTyQ.
Let y be given.
Assume HyY: y ∈ Y.
Let U be given.
Assume HU: U ∈ Q.
Assume HyU: y ∈ U.
We prove the intermediate claim HUpowY: U ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λV0 : set ⇒ preimage_of X f V0 ∈ Tx) U HU).
We prove the intermediate claim HUsubY: U ⊆ Y.
An exact proof term for the current goal is (PowerE Y U HUpowY).
Set Tu to be the term subspace_topology Y Q U.
We prove the intermediate claim HTu: topology_on U Tu.
An exact proof term for the current goal is (subspace_topology_is_topology Y Q U HTyQ HUsubY).
Set V to be the term component_of U Tu y.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (point_in_component U Tu y HTu HyU).
We prove the intermediate claim HVsubU: V ⊆ U.
Let t be given.
Assume Ht: t ∈ V.
An exact proof term for the current goal is (SepE1 U (λt0 : set ⇒ ∃C : set, connected_space C (subspace_topology U Tu C) ∧ y ∈ C ∧ t0 ∈ C) t Ht).
We prove the intermediate claim HVsubY: V ⊆ Y.
An exact proof term for the current goal is (Subq_tra V U Y HVsubU HUsubY).
We prove the intermediate claim HconnVu: connected_space V (subspace_topology U Tu V).
An exact proof term for the current goal is (component_of_connected U Tu y HTu HyU).
We prove the intermediate claim HeqTopV: subspace_topology U Tu V = subspace_topology Y Q V.
An exact proof term for the current goal is (ex16_1_subspace_transitive Y Q U V HTyQ HUsubY HVsubU).
We prove the intermediate claim HconnV: connected_space V (subspace_topology Y Q V).
rewrite the current goal using HeqTopV (from right to left).
An exact proof term for the current goal is HconnVu.
Set preU to be the term preimage_of X f U.
We prove the intermediate claim HpreU: preU ∈ Tx.
We prove the intermediate claim Hraw: {x0 ∈ X|apply_fun f x0 ∈ U} ∈ Tx.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λV0 : set ⇒ {x0 ∈ X|apply_fun f x0 ∈ V0} ∈ Tx) U HU).
We prove the intermediate claim Heq: preU = {x0 ∈ X|apply_fun f x0 ∈ U}.
Use reflexivity.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hraw.
Set preV to be the term preimage_of X f V.
Set UFam to be the term {W ∈ Tx|W ⊆ preV ∧ connected_space W (subspace_topology X Tx W)}.
We prove the intermediate claim HUFsub: UFam ⊆ Tx.
Let W be given.
Assume HW: W ∈ UFam.
An exact proof term for the current goal is (SepE1 Tx (λW0 : set ⇒ W0 ⊆ preV ∧ connected_space W0 (subspace_topology X Tx W0)) W HW).
We prove the intermediate claim HUnionTx: ⋃ UFam ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx UFam HTx HUFsub).
We prove the intermediate claim HUnionEq: ⋃ UFam = preV.
Apply set_ext to the current goal.
Let x0 be given.
Assume Hx0: x0 ∈ ⋃ UFam.
Apply (UnionE UFam x0 Hx0) to the current goal.
Let W be given.
Assume Hx0W: x0 ∈ W ∧ W ∈ UFam.
We prove the intermediate claim Hx0W0: x0 ∈ W.
An exact proof term for the current goal is (andEL (x0 ∈ W) (W ∈ UFam) Hx0W).
We prove the intermediate claim HWUF: W ∈ UFam.
An exact proof term for the current goal is (andER (x0 ∈ W) (W ∈ UFam) Hx0W).
We prove the intermediate claim HWprop: W ⊆ preV ∧ connected_space W (subspace_topology X Tx W).
An exact proof term for the current goal is (SepE2 Tx (λW0 : set ⇒ W0 ⊆ preV ∧ connected_space W0 (subspace_topology X Tx W0)) W HWUF).
We prove the intermediate claim HWsub: W ⊆ preV.
An exact proof term for the current goal is (andEL (W ⊆ preV) (connected_space W (subspace_topology X Tx W)) HWprop).
An exact proof term for the current goal is (HWsub x0 Hx0W0).
Let x0 be given.
Assume Hx0: x0 ∈ preV.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λx1 : set ⇒ apply_fun f x1 ∈ V) x0 Hx0).
We prove the intermediate claim Hy0V: apply_fun f x0 ∈ V.
An exact proof term for the current goal is (SepE2 X (λx1 : set ⇒ apply_fun f x1 ∈ V) x0 Hx0).
We prove the intermediate claim Hy0U: apply_fun f x0 ∈ U.
An exact proof term for the current goal is (HVsubU (apply_fun f x0) Hy0V).
We prove the intermediate claim Hx0preU: x0 ∈ preU.
We prove the intermediate claim Heq: preU = {x1 ∈ X|apply_fun f x1 ∈ U}.
Use reflexivity.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SepI X (λx1 : set ⇒ apply_fun f x1 ∈ U) x0 Hx0X Hy0U).
Apply (locally_connected_local X Tx x0 preU Hloc Hx0X HpreU Hx0preU) to the current goal.
Let W0 be given.
Assume HW0pack: W0 ∈ Tx ∧ x0 ∈ W0 ∧ W0 ⊆ preU ∧ connected_space W0 (subspace_topology X Tx W0).
We prove the intermediate claim HW0pair: (W0 ∈ Tx ∧ x0 ∈ W0) ∧ W0 ⊆ preU.
An exact proof term for the current goal is (andEL ((W0 ∈ Tx ∧ x0 ∈ W0) ∧ W0 ⊆ preU) (connected_space W0 (subspace_topology X Tx W0)) HW0pack).
We prove the intermediate claim HW0Tx: W0 ∈ Tx.
An exact proof term for the current goal is (andEL (W0 ∈ Tx) (x0 ∈ W0) (andEL (W0 ∈ Tx ∧ x0 ∈ W0) (W0 ⊆ preU) HW0pair)).
We prove the intermediate claim Hx0W0: x0 ∈ W0.
An exact proof term for the current goal is (andER (W0 ∈ Tx) (x0 ∈ W0) (andEL (W0 ∈ Tx ∧ x0 ∈ W0) (W0 ⊆ preU) HW0pair)).
We prove the intermediate claim HW0subpreU: W0 ⊆ preU.
An exact proof term for the current goal is (andER (W0 ∈ Tx ∧ x0 ∈ W0) (W0 ⊆ preU) HW0pair).
We prove the intermediate claim HW0conn: connected_space W0 (subspace_topology X Tx W0).
An exact proof term for the current goal is (andER ((W0 ∈ Tx ∧ x0 ∈ W0) ∧ W0 ⊆ preU) (connected_space W0 (subspace_topology X Tx W0)) HW0pack).
Set ImW0 to be the term image_of f W0.
We prove the intermediate claim HImSubU: ImW0 ⊆ U.
Let y1 be given.
Assume Hy1: y1 ∈ ImW0.
Apply (ReplE_impred W0 (λz : set ⇒ apply_fun f z) y1 Hy1) to the current goal.
Let z be given.
Assume HzW0: z ∈ W0.
Assume Hy1eq: y1 = apply_fun f z.
We prove the intermediate claim HzpreU: z ∈ preU.
An exact proof term for the current goal is (HW0subpreU z HzW0).
We prove the intermediate claim HfzU: apply_fun f z ∈ U.
An exact proof term for the current goal is (SepE2 X (λu0 : set ⇒ apply_fun f u0 ∈ U) z HzpreU).
rewrite the current goal using Hy1eq (from left to right).
An exact proof term for the current goal is HfzU.
We prove the intermediate claim HcontW0: continuous_map W0 (subspace_topology X Tx W0) Y Q f.
We prove the intermediate claim HW0subX: W0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx W0 HTx HW0Tx).
An exact proof term for the current goal is (continuous_on_subspace_rule X Tx Y Q f W0 HTx HTyQ HW0subX Hcont).
We prove the intermediate claim HImConnY: connected_space ImW0 (subspace_topology Y Q ImW0).
An exact proof term for the current goal is (continuous_image_connected W0 (subspace_topology X Tx W0) Y Q f HW0conn HcontW0).
We prove the intermediate claim HeqTopIm: subspace_topology U Tu ImW0 = subspace_topology Y Q ImW0.
An exact proof term for the current goal is (ex16_1_subspace_transitive Y Q U ImW0 HTyQ HUsubY HImSubU).
We prove the intermediate claim HImConnU: connected_space ImW0 (subspace_topology U Tu ImW0).
rewrite the current goal using HeqTopIm (from left to right).
An exact proof term for the current goal is HImConnY.
We prove the intermediate claim Hy0Im: apply_fun f x0 ∈ ImW0.
An exact proof term for the current goal is (ReplI W0 (λz : set ⇒ apply_fun f z) x0 Hx0W0).
We prove the intermediate claim HImSubComp: ImW0 ⊆ component_of U Tu (apply_fun f x0).
Let y1 be given.
Assume Hy1: y1 ∈ ImW0.
We will prove y1 ∈ component_of U Tu (apply_fun f x0).
We will prove y1 ∈ {t ∈ U|∃C : set, connected_space C (subspace_topology U Tu C) ∧ apply_fun f x0 ∈ C ∧ t ∈ C}.
Apply SepI to the current goal.
An exact proof term for the current goal is (HImSubU y1 Hy1).
We will prove ∃C : set, connected_space C (subspace_topology U Tu C) ∧ apply_fun f x0 ∈ C ∧ y1 ∈ C.
We use ImW0 to witness the existential quantifier.
We will prove connected_space ImW0 (subspace_topology U Tu ImW0) ∧ apply_fun f x0 ∈ ImW0 ∧ y1 ∈ ImW0.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HImConnU.
An exact proof term for the current goal is Hy0Im.
An exact proof term for the current goal is Hy1.
We prove the intermediate claim Hy0U0: apply_fun f x0 ∈ U.
An exact proof term for the current goal is Hy0U.
We prove the intermediate claim HeqComp: component_of U Tu (apply_fun f x0) = V.
We prove the intermediate claim HVdef: V = component_of U Tu y.
Use reflexivity.
We prove the intermediate claim Hy0Comp: apply_fun f x0 ∈ component_of U Tu y.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is Hy0V.
rewrite the current goal using HVdef (from left to right).
An exact proof term for the current goal is (component_of_eq_if_in U Tu y (apply_fun f x0) HTu HyU Hy0Comp).
We prove the intermediate claim HImSubV: ImW0 ⊆ V.
rewrite the current goal using HeqComp (from right to left).
An exact proof term for the current goal is HImSubComp.
We prove the intermediate claim HW0subpreV: W0 ⊆ preV.
Let z be given.
Assume Hz: z ∈ W0.
We will prove z ∈ preV.
We prove the intermediate claim HfzV: apply_fun f z ∈ V.
We prove the intermediate claim HfzIm: apply_fun f z ∈ ImW0.
An exact proof term for the current goal is (ReplI W0 (λt : set ⇒ apply_fun f t) z Hz).
An exact proof term for the current goal is (HImSubV (apply_fun f z) HfzIm).
An exact proof term for the current goal is (SepI X (λx1 : set ⇒ apply_fun f x1 ∈ V) z (topology_elem_subset X Tx W0 HTx HW0Tx z Hz) HfzV).
We prove the intermediate claim HW0inUFam: W0 ∈ UFam.
Apply SepI to the current goal.
An exact proof term for the current goal is HW0Tx.
We will prove W0 ⊆ preV ∧ connected_space W0 (subspace_topology X Tx W0).
Apply andI to the current goal.
An exact proof term for the current goal is HW0subpreV.
An exact proof term for the current goal is HW0conn.
An exact proof term for the current goal is (UnionI UFam x0 W0 Hx0W0 HW0inUFam).
We prove the intermediate claim HpreV: preV ∈ Tx.
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HUnionTx.
We prove the intermediate claim HVpowY: V ∈ 𝒫 Y.
Apply PowerI to the current goal.
Let y0 be given.
Assume Hy0: y0 ∈ V.
An exact proof term for the current goal is (HVsubY y0 Hy0).
We prove the intermediate claim HVQ: V ∈ Q.
An exact proof term for the current goal is (SepI (𝒫 Y) (λV0 : set ⇒ preimage_of X f V0 ∈ Tx) V HVpowY HpreV).
We use V to witness the existential quantifier.
We will prove V ∈ Q ∧ y ∈ V ∧ V ⊆ U ∧ connected_space V (subspace_topology Y Q V).
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 HVQ.
An exact proof term for the current goal is HyV.
An exact proof term for the current goal is HVsubU.
An exact proof term for the current goal is HconnV.
∎