Let X, Tx and Y be given.
Assume Hloc: locally_connected X Tx.
Assume HYopen: Y ∈ Tx.
Set Ty to be the term subspace_topology X Tx Y.
We will prove locally_connected Y Ty.
We prove the intermediate claim Hdef: locally_connected Y Ty = (topology_on Y Ty ∧ ∀y : set, y ∈ Y → ∀U : set, U ∈ Ty → y ∈ U → ∃V : set, V ∈ Ty ∧ y ∈ V ∧ V ⊆ U ∧ connected_space V (subspace_topology Y Ty V)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply andI to the current goal.
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 HYpow: Y ∈ 𝒫 X.
An exact proof term for the current goal is ((topology_sub_Power X Tx HTx) Y HYopen).
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (PowerE X Y HYpow).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Y HTx HYsub).
Let y be given.
Assume HyY: y ∈ Y.
Let U be given.
Assume HU: U ∈ Ty.
Assume HyU: y ∈ U.
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, U = U0 ∩ Y.
An exact proof term for the current goal is (subspace_topologyE X Tx Y U HU).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0pair.
We prove the intermediate claim HU0open: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (U = U0 ∩ Y) HU0pair).
We prove the intermediate claim HUeq: U = U0 ∩ Y.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (U = U0 ∩ Y) HU0pair).
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 HYpow: Y ∈ 𝒫 X.
An exact proof term for the current goal is ((topology_sub_Power X Tx HTx) Y HYopen).
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (PowerE X Y HYpow).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HYsub y HyY).
We prove the intermediate claim HyU0Y: y ∈ U0 ∩ Y.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HyU.
We prove the intermediate claim HU0Yopen: (U0 ∩ Y) ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U0 Y HTx HU0open HYopen).
We prove the intermediate claim Hloc0: ∃V0 : set, V0 ∈ Tx ∧ y ∈ V0 ∧ V0 ⊆ (U0 ∩ Y) ∧ connected_space V0 (subspace_topology X Tx V0).
An exact proof term for the current goal is (locally_connected_local X Tx y (U0 ∩ Y) Hloc HyX HU0Yopen HyU0Y).
Apply Hloc0 to the current goal.
Let V0 be given.
Assume HV0data.
We prove the intermediate claim HABC: (V0 ∈ Tx ∧ y ∈ V0) ∧ V0 ⊆ (U0 ∩ Y).
An exact proof term for the current goal is (andEL ((V0 ∈ Tx ∧ y ∈ V0) ∧ V0 ⊆ (U0 ∩ Y)) (connected_space V0 (subspace_topology X Tx V0)) HV0data).
We prove the intermediate claim HV0connX: connected_space V0 (subspace_topology X Tx V0).
An exact proof term for the current goal is (andER ((V0 ∈ Tx ∧ y ∈ V0) ∧ V0 ⊆ (U0 ∩ Y)) (connected_space V0 (subspace_topology X Tx V0)) HV0data).
We prove the intermediate claim HAB: V0 ∈ Tx ∧ y ∈ V0.
An exact proof term for the current goal is (andEL (V0 ∈ Tx ∧ y ∈ V0) (V0 ⊆ (U0 ∩ Y)) HABC).
We prove the intermediate claim HV0subU0Y: V0 ⊆ (U0 ∩ Y).
An exact proof term for the current goal is (andER (V0 ∈ Tx ∧ y ∈ V0) (V0 ⊆ (U0 ∩ Y)) HABC).
We prove the intermediate claim HV0open: V0 ∈ Tx.
An exact proof term for the current goal is (andEL (V0 ∈ Tx) (y ∈ V0) HAB).
We prove the intermediate claim HyV0: y ∈ V0.
An exact proof term for the current goal is (andER (V0 ∈ Tx) (y ∈ V0) HAB).
We prove the intermediate claim HV0subY: V0 ⊆ Y.
Let z be given.
Assume HzV0: z ∈ V0.
We prove the intermediate claim HzU0Y: z ∈ U0 ∩ Y.
An exact proof term for the current goal is (HV0subU0Y z HzV0).
An exact proof term for the current goal is (binintersectE2 U0 Y z HzU0Y).
We prove the intermediate claim HV0subU: V0 ⊆ U.
Let z be given.
Assume HzV0: z ∈ V0.
We prove the intermediate claim HzU0Y: z ∈ U0 ∩ Y.
An exact proof term for the current goal is (HV0subU0Y z HzV0).
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 Y z HzU0Y).
We prove the intermediate claim HzY: z ∈ Y.
An exact proof term for the current goal is (binintersectE2 U0 Y z HzU0Y).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binintersectI U0 Y z HzU0 HzY).
We prove the intermediate claim HV0inTy: V0 ∈ Ty.
We prove the intermediate claim HV0eq: V0 = V0 ∩ Y.
Use symmetry.
An exact proof term for the current goal is (binintersect_Subq_eq_1 V0 Y HV0subY).
rewrite the current goal using HV0eq (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx Y V0 HV0open).
We prove the intermediate claim HV0connY: connected_space V0 (subspace_topology Y Ty V0).
rewrite the current goal using (ex16_1_subspace_transitive X Tx Y V0 HTx HYsub HV0subY) (from left to right).
An exact proof term for the current goal is HV0connX.
We use V0 to witness the existential quantifier.
We will prove V0 ∈ Ty ∧ y ∈ V0 ∧ V0 ⊆ U ∧ connected_space V0 (subspace_topology Y Ty V0).
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 HV0inTy.
An exact proof term for the current goal is HyV0.
An exact proof term for the current goal is HV0subU.
An exact proof term for the current goal is HV0connY.
∎