clsconn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > clsconn		Structured version Visualization version GIF version

Theorem clsconn 23278

Description: The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)

**Assertion**
Ref	Expression
clsconn	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) → (𝐽 ↾_t ((cls‘𝐽)‘𝐴)) ∈ Conn)

Proof of Theorem clsconn Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll3 1211	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ ((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴)))) → (𝐽 ↾_t 𝐴) ∈ Conn)
2		simpll1 1209	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐽 ∈ (TopOn‘𝑋))
3		simpll2 1210	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐴 ⊆ 𝑋)
4		simplrl 774	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝑥 ∈ 𝐽)
5		simplrr 775	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝑦 ∈ 𝐽)
6		simprl1 1215	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅)
7		n0 4339	. . . . . . . . 9 ⊢ ((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴)))
8	6, 7	sylib 217	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ∃𝑧 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴)))
9	2	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝐽 ∈ (TopOn‘𝑋))
10		topontop 22759	. . . . . . . . . 10 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
11	9, 10	syl 17	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝐽 ∈ Top)
12	3	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝐴 ⊆ 𝑋)
13		toponuni 22760	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
14	9, 13	syl 17	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑋 = ∪ 𝐽)
15	12, 14	sseqtrd 4015	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝐴 ⊆ ∪ 𝐽)
16		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴)))
17	16	elin2d 4192	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
18	4	adantr 480	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑥 ∈ 𝐽)
19	16	elin1d 4191	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ 𝑥)
20		eqid 2724	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
21	20	clsndisj 22923	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑧 ∈ ((cls‘𝐽)‘𝐴)) ∧ (𝑥 ∈ 𝐽 ∧ 𝑧 ∈ 𝑥)) → (𝑥 ∩ 𝐴) ≠ ∅)
22	11, 15, 17, 18, 19, 21	syl32anc 1375	. . . . . . . 8 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑥 ∩ ((cls‘𝐽)‘𝐴))) → (𝑥 ∩ 𝐴) ≠ ∅)
23	8, 22	exlimddv 1930	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ 𝐴) ≠ ∅)
24		simprl2 1216	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅)
25		n0 4339	. . . . . . . . 9 ⊢ ((𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴)))
26	24, 25	sylib 217	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ∃𝑧 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴)))
27	2	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝐽 ∈ (TopOn‘𝑋))
28	27, 10	syl 17	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝐽 ∈ Top)
29	3	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝐴 ⊆ 𝑋)
30	27, 13	syl 17	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑋 = ∪ 𝐽)
31	29, 30	sseqtrd 4015	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝐴 ⊆ ∪ 𝐽)
32		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴)))
33	32	elin2d 4192	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ ((cls‘𝐽)‘𝐴))
34	5	adantr 480	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑦 ∈ 𝐽)
35	32	elin1d 4191	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → 𝑧 ∈ 𝑦)
36	20	clsndisj 22923	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑧 ∈ ((cls‘𝐽)‘𝐴)) ∧ (𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝑦)) → (𝑦 ∩ 𝐴) ≠ ∅)
37	28, 31, 33, 34, 35, 36	syl32anc 1375	. . . . . . . 8 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) ∧ 𝑧 ∈ (𝑦 ∩ ((cls‘𝐽)‘𝐴))) → (𝑦 ∩ 𝐴) ≠ ∅)
38	26, 37	exlimddv 1930	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑦 ∩ 𝐴) ≠ ∅)
39		simprl3 1217	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴)))
40	2, 10	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐽 ∈ Top)
41	2, 13	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝑋 = ∪ 𝐽)
42	3, 41	sseqtrd 4015	. . . . . . . . . . . 12 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐴 ⊆ ∪ 𝐽)
43	20	sscls 22904	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽) → 𝐴 ⊆ ((cls‘𝐽)‘𝐴))
44	40, 42, 43	syl2anc 583	. . . . . . . . . . 11 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐴 ⊆ ((cls‘𝐽)‘𝐴))
45	44	sscond 4134	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑋 ∖ ((cls‘𝐽)‘𝐴)) ⊆ (𝑋 ∖ 𝐴))
46	39, 45	sstrd 3985	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ 𝐴))
47		ssv 3999	. . . . . . . . . 10 ⊢ 𝑋 ⊆ V
48		ssdif 4132	. . . . . . . . . 10 ⊢ (𝑋 ⊆ V → (𝑋 ∖ 𝐴) ⊆ (V ∖ 𝐴))
49	47, 48	ax-mp 5	. . . . . . . . 9 ⊢ (𝑋 ∖ 𝐴) ⊆ (V ∖ 𝐴)
50	46, 49	sstrdi 3987	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → (𝑥 ∩ 𝑦) ⊆ (V ∖ 𝐴))
51		disj2 4450	. . . . . . . 8 ⊢ (((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅ ↔ (𝑥 ∩ 𝑦) ⊆ (V ∖ 𝐴))
52	50, 51	sylibr 233	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅)
53		simprr 770	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))
54	44, 53	sstrd 3985	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → 𝐴 ⊆ (𝑥 ∪ 𝑦))
55	2, 3, 4, 5, 23, 38, 52, 54	nconnsubb 23271	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) ∧ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))) → ¬ (𝐽 ↾_t 𝐴) ∈ Conn)
56	55	expr 456	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ ((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴)))) → (((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦) → ¬ (𝐽 ↾_t 𝐴) ∈ Conn))
57	1, 56	mt2d 136	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ ((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴)))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))
58	57	ex 412	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦)))
59	58	ralrimivva 3192	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦)))
60		simp1 1133	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) → 𝐽 ∈ (TopOn‘𝑋))
61	13	sseq2d 4007	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ∪ 𝐽))
62	61	biimpa 476	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ 𝐽)
63	20	clsss3 22907	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽) → ((cls‘𝐽)‘𝐴) ⊆ ∪ 𝐽)
64	10, 62, 63	syl2an2r 682	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ⊆ ∪ 𝐽)
65	13	adantr 480	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 = ∪ 𝐽)
66	64, 65	sseqtrrd 4016	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ⊆ 𝑋)
67	66	3adant3 1129	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) → ((cls‘𝐽)‘𝐴) ⊆ 𝑋)
68		connsub 23269	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((cls‘𝐽)‘𝐴) ⊆ 𝑋) → ((𝐽 ↾_t ((cls‘𝐽)‘𝐴)) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))))
69	60, 67, 68	syl2anc 583	. 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) → ((𝐽 ↾_t ((cls‘𝐽)‘𝐴)) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑦 ∩ ((cls‘𝐽)‘𝐴)) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ ((cls‘𝐽)‘𝐴))) → ¬ ((cls‘𝐽)‘𝐴) ⊆ (𝑥 ∪ 𝑦))))
70	59, 69	mpbird 257	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾_t 𝐴) ∈ Conn) → (𝐽 ↾_t ((cls‘𝐽)‘𝐴)) ∈ Conn)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ≠ wne 2932 ∀wral 3053 Vcvv 3466 ∖ cdif 3938 ∪ cun 3939 ∩ cin 3940 ⊆ wss 3941 ∅c0 4315 ∪ cuni 4900 ‘cfv 6534 (class class class)co 7402 ↾_t crest 17371 Topctop 22739 TopOnctopon 22756 clsccl 22866 Conncconn 23259

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5276 ax-sep 5290 ax-nul 5297 ax-pow 5354 ax-pr 5418 ax-un 7719

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3960 df-nul 4316 df-if 4522 df-pw 4597 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-int 4942 df-iun 4990 df-iin 4991 df-br 5140 df-opab 5202 df-mpt 5223 df-tr 5257 df-id 5565 df-eprel 5571 df-po 5579 df-so 5580 df-fr 5622 df-we 5624 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6486 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-ov 7405 df-oprab 7406 df-mpo 7407 df-om 7850 df-1st 7969 df-2nd 7970 df-en 8937 df-fin 8940 df-fi 9403 df-rest 17373 df-topgen 17394 df-top 22740 df-topon 22757 df-bases 22793 df-cld 22867 df-ntr 22868 df-cls 22869 df-conn 23260

This theorem is referenced by: conncompcld 23282

W3C validator