Let X, Tx, x and y be given.
Assume HTx: topology_on X Tx.
Assume HxX: x ∈ X.
Assume HyComp: y ∈ component_of X Tx x.
We will prove component_of X Tx y = component_of X Tx x.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y0 ∈ C) y HyComp).
We prove the intermediate claim HexC: ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y0 ∈ C) y HyComp).
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ component_of X Tx y.
We will prove z ∈ component_of X Tx x.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∃D : set, connected_space D (subspace_topology X Tx D) ∧ y ∈ D ∧ z0 ∈ D) z Hz).
We prove the intermediate claim HexD: ∃D : set, connected_space D (subspace_topology X Tx D) ∧ y ∈ D ∧ z ∈ D.
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ ∃D : set, connected_space D (subspace_topology X Tx D) ∧ y ∈ D ∧ z0 ∈ D) z Hz).
We will prove z ∈ {y0 ∈ X|∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y0 ∈ C}.
Apply SepI to the current goal.
An exact proof term for the current goal is HzX.
Set C to be the term Eps_i (λC0 : set ⇒ connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0 ∧ y ∈ C0).
We prove the intermediate claim HC: connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C.
An exact proof term for the current goal is (Eps_i_ex (λC0 : set ⇒ connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0 ∧ y ∈ C0) HexC).
Set D to be the term Eps_i (λD0 : set ⇒ connected_space D0 (subspace_topology X Tx D0) ∧ y ∈ D0 ∧ z ∈ D0).
We prove the intermediate claim HD: connected_space D (subspace_topology X Tx D) ∧ y ∈ D ∧ z ∈ D.
An exact proof term for the current goal is (Eps_i_ex (λD0 : set ⇒ connected_space D0 (subspace_topology X Tx D0) ∧ y ∈ D0 ∧ z ∈ D0) HexD).
We prove the intermediate claim HCconn: connected_space C (subspace_topology X Tx C).
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology X Tx C)) (x ∈ C) (andEL (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC)).
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C)) (x ∈ C) (andEL (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC)).
We prove the intermediate claim HyC: y ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC).
We prove the intermediate claim HDconn: connected_space D (subspace_topology X Tx D).
An exact proof term for the current goal is (andEL (connected_space D (subspace_topology X Tx D)) (y ∈ D) (andEL (connected_space D (subspace_topology X Tx D) ∧ y ∈ D) (z ∈ D) HD)).
We prove the intermediate claim HyD: y ∈ D.
An exact proof term for the current goal is (andER (connected_space D (subspace_topology X Tx D)) (y ∈ D) (andEL (connected_space D (subspace_topology X Tx D) ∧ y ∈ D) (z ∈ D) HD)).
We prove the intermediate claim HzD: z ∈ D.
An exact proof term for the current goal is (andER (connected_space D (subspace_topology X Tx D) ∧ y ∈ D) (z ∈ D) HD).
We prove the intermediate claim HCsubX: C ⊆ X.
An exact proof term for the current goal is (connected_subspace_subset X Tx C HTx HCconn).
We prove the intermediate claim HDsubX: D ⊆ X.
An exact proof term for the current goal is (connected_subspace_subset X Tx D HTx HDconn).
Set F to be the term UPair C D.
We prove the intermediate claim HFsub: ∀E : set, E ∈ F → E ⊆ X.
Let E be given.
Assume HE: E ∈ F.
Apply (UPairE E C D HE (E ⊆ X)) to the current goal.
Assume HEq: E = C.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HCsubX.
Assume HEq: E = D.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HDsubX.
We prove the intermediate claim HFconn: ∀E : set, E ∈ F → connected_space E (subspace_topology X Tx E).
Let E be given.
Assume HE: E ∈ F.
Apply (UPairE E C D HE (connected_space E (subspace_topology X Tx E))) to the current goal.
Assume HEq: E = C.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HCconn.
Assume HEq: E = D.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HDconn.
We prove the intermediate claim Hcommon: ∃w : set, ∀E : set, E ∈ F → w ∈ E.
We use y to witness the existential quantifier.
Let E be given.
Assume HE: E ∈ F.
Apply (UPairE E C D HE (y ∈ E)) to the current goal.
Assume HEq: E = C.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HyC.
Assume HEq: E = D.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HyD.
We prove the intermediate claim HUnionConn: connected_space (⋃ F) (subspace_topology X Tx (⋃ F)).
An exact proof term for the current goal is (union_connected_common_point X Tx F HTx HFsub HFconn Hcommon).
We prove the intermediate claim HCinF: C ∈ F.
An exact proof term for the current goal is (UPairI1 C D).
We prove the intermediate claim HDinF: D ∈ F.
An exact proof term for the current goal is (UPairI2 C D).
We prove the intermediate claim HxUF: x ∈ ⋃ F.
An exact proof term for the current goal is (UnionI F x C HxC HCinF).
We prove the intermediate claim HzUF: z ∈ ⋃ F.
An exact proof term for the current goal is (UnionI F z D HzD HDinF).
We will prove ∃C0 : set, connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0 ∧ z ∈ C0.
We use (⋃ F) to witness the existential quantifier.
We will prove connected_space (⋃ F) (subspace_topology X Tx (⋃ F)) ∧ x ∈ ⋃ F ∧ z ∈ ⋃ F.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUnionConn.
An exact proof term for the current goal is HxUF.
An exact proof term for the current goal is HzUF.
Let z be given.
Assume Hz: z ∈ component_of X Tx x.
We will prove z ∈ component_of X Tx y.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ z0 ∈ C) z Hz).
We prove the intermediate claim HexCz: ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ z ∈ C.
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ z0 ∈ C) z Hz).
We will prove z ∈ {y0 ∈ X|∃C : set, connected_space C (subspace_topology X Tx C) ∧ y ∈ C ∧ y0 ∈ C}.
Apply SepI to the current goal.
An exact proof term for the current goal is HzX.
Set C to be the term Eps_i (λC0 : set ⇒ connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0 ∧ y ∈ C0).
We prove the intermediate claim HC: connected_space C (subspace_topology X Tx C) ∧ x ∈ C ∧ y ∈ C.
An exact proof term for the current goal is (Eps_i_ex (λC0 : set ⇒ connected_space C0 (subspace_topology X Tx C0) ∧ x ∈ C0 ∧ y ∈ C0) HexC).
Set D to be the term Eps_i (λD0 : set ⇒ connected_space D0 (subspace_topology X Tx D0) ∧ x ∈ D0 ∧ z ∈ D0).
We prove the intermediate claim HD: connected_space D (subspace_topology X Tx D) ∧ x ∈ D ∧ z ∈ D.
An exact proof term for the current goal is (Eps_i_ex (λD0 : set ⇒ connected_space D0 (subspace_topology X Tx D0) ∧ x ∈ D0 ∧ z ∈ D0) HexCz).
We prove the intermediate claim HCconn: connected_space C (subspace_topology X Tx C).
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology X Tx C)) (x ∈ C) (andEL (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC)).
We prove the intermediate claim HxC: x ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C)) (x ∈ C) (andEL (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC)).
We prove the intermediate claim HyC: y ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C) ∧ x ∈ C) (y ∈ C) HC).
We prove the intermediate claim HDconn: connected_space D (subspace_topology X Tx D).
An exact proof term for the current goal is (andEL (connected_space D (subspace_topology X Tx D)) (x ∈ D) (andEL (connected_space D (subspace_topology X Tx D) ∧ x ∈ D) (z ∈ D) HD)).
We prove the intermediate claim HxD: x ∈ D.
An exact proof term for the current goal is (andER (connected_space D (subspace_topology X Tx D)) (x ∈ D) (andEL (connected_space D (subspace_topology X Tx D) ∧ x ∈ D) (z ∈ D) HD)).
We prove the intermediate claim HzD: z ∈ D.
An exact proof term for the current goal is (andER (connected_space D (subspace_topology X Tx D) ∧ x ∈ D) (z ∈ D) HD).
We prove the intermediate claim HCsubX: C ⊆ X.
An exact proof term for the current goal is (connected_subspace_subset X Tx C HTx HCconn).
We prove the intermediate claim HDsubX: D ⊆ X.
An exact proof term for the current goal is (connected_subspace_subset X Tx D HTx HDconn).
Set F to be the term UPair C D.
We prove the intermediate claim HFsub: ∀E : set, E ∈ F → E ⊆ X.
Let E be given.
Assume HE: E ∈ F.
Apply (UPairE E C D HE (E ⊆ X)) to the current goal.
Assume HEq: E = C.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HCsubX.
Assume HEq: E = D.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HDsubX.
We prove the intermediate claim HFconn: ∀E : set, E ∈ F → connected_space E (subspace_topology X Tx E).
Let E be given.
Assume HE: E ∈ F.
Apply (UPairE E C D HE (connected_space E (subspace_topology X Tx E))) to the current goal.
Assume HEq: E = C.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HCconn.
Assume HEq: E = D.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HDconn.
We prove the intermediate claim Hcommon: ∃w : set, ∀E : set, E ∈ F → w ∈ E.
We use x to witness the existential quantifier.
Let E be given.
Assume HE: E ∈ F.
Apply (UPairE E C D HE (x ∈ E)) to the current goal.
Assume HEq: E = C.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HxC.
Assume HEq: E = D.
rewrite the current goal using HEq (from left to right).
An exact proof term for the current goal is HxD.
We prove the intermediate claim HUnionConn: connected_space (⋃ F) (subspace_topology X Tx (⋃ F)).
An exact proof term for the current goal is (union_connected_common_point X Tx F HTx HFsub HFconn Hcommon).
We prove the intermediate claim HCinF: C ∈ F.
An exact proof term for the current goal is (UPairI1 C D).
We prove the intermediate claim HDinF: D ∈ F.
An exact proof term for the current goal is (UPairI2 C D).
We prove the intermediate claim HyUF: y ∈ ⋃ F.
An exact proof term for the current goal is (UnionI F y C HyC HCinF).
We prove the intermediate claim HzUF: z ∈ ⋃ F.
An exact proof term for the current goal is (UnionI F z D HzD HDinF).
We will prove ∃C0 : set, connected_space C0 (subspace_topology X Tx C0) ∧ y ∈ C0 ∧ z ∈ C0.
We use (⋃ F) to witness the existential quantifier.
We will prove connected_space (⋃ F) (subspace_topology X Tx (⋃ F)) ∧ y ∈ ⋃ F ∧ z ∈ ⋃ F.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUnionConn.
An exact proof term for the current goal is HyUF.
An exact proof term for the current goal is HzUF.
∎