Theorem dfconn2 22029

Description: An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)

Assertion

Ref	Expression
dfconn2	⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))

Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝑋,𝑦

Proof of Theorem dfconn2

Step	Hyp	Ref	Expression
1		eqid 2823	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
2		simpll 765	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝐽 ∈ Conn)
3		simplrl 775	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ∈ 𝐽)
4		simpr1 1190	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ≠ ∅)
5		simplrr 776	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ∈ 𝐽)
6		simpr2 1191	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ≠ ∅)
7		simpr3 1192	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∩ 𝑦) = ∅)
8	1, 2, 3, 4, 5, 6, 7	conndisj 22026	. . . . 5 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)
9	8	ex 415	. . . 4 ⊢ ((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
10	9	ralrimivva 3193	. . 3 ⊢ (𝐽 ∈ Conn → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
11		topontop 21523	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
12	1	cldopn 21641	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (Clsd‘𝐽) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
13	12	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
14		df-3an 1085	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅))
15		ineq2 4185	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)))
16		disjdif 4423	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)) = ∅
17	15, 16	syl6eq 2874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = ∅)
18	17	biantrud 534	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅)))
19		neeq1 3080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑦 ≠ ∅ ↔ (∪ 𝐽 ∖ 𝑥) ≠ ∅))
20	19	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
21	18, 20	bitr3d 283	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
22	14, 21	syl5bb 285	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
23		uneq2 4135	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)))
24		undif2 4427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)) = (𝑥 ∪ ∪ 𝐽)
25	23, 24	syl6eq 2874	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ ∪ 𝐽))
26	25	neeq1d 3077	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ∪ 𝑦) ≠ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
27	22, 26	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
28	27	rspcv 3620	. . . . . . . . . . . . 13 ⊢ ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
29	13, 28	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
30	1	cldss 21639	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽)
31	30	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ ∪ 𝐽)
32		ssequn1 4158	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
33	31, 32	sylib 220	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
34		ssdif0 4325	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝐽 ⊆ 𝑥 ↔ (∪ 𝐽 ∖ 𝑥) = ∅)
35		idd 24	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → ∪ 𝐽 ⊆ 𝑥))
36	35, 31	jctild 528	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥)))
37		eqss 3984	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∪ 𝐽 ↔ (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥))
38	36, 37	syl6ibr 254	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → 𝑥 = ∪ 𝐽))
39	34, 38	syl5bir 245	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((∪ 𝐽 ∖ 𝑥) = ∅ → 𝑥 = ∪ 𝐽))
40	33, 39	embantd 59	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → 𝑥 = ∪ 𝐽))
41	40	orim2d 963	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽)))
42		impexp 453	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
43		df-ne 3019	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
45	44	necon4d 3042	. . . . . . . . . . . . . . . . 17 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
46		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
47	46	necon3d 3039	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
48	45, 47	impbii 211	. . . . . . . . . . . . . . . 16 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
49	43, 48	imbi12i 353	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
50		pm4.64 845	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
51	49, 50	bitri 277	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
52	42, 51	bitri 277	. . . . . . . . . . . . 13 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
53		vex 3499	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
54	53	elpr 4592	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∅, ∪ 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽))
55	41, 52, 54	3imtr4g 298	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))
56	29, 55	syld 47	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))
57	56	ex 415	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
58	57	com23 86	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
59	58	imim2d 57	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))))
60		elin 4171	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)))
61	60	imbi1i 352	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
62		impexp 453	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
63	61, 62	bitri 277	. . . . . . . 8 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
64	59, 63	syl6ibr 254	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
65	64	alimdv 1917	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
66		df-ral 3145	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
67		dfss2 3957	. . . . . 6 ⊢ ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
68	65, 66, 67	3imtr4g 298	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
69	1	isconn2 22024	. . . . . 6 ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
70	69	baib 538	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
71	68, 70	sylibrd 261	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
72	11, 71	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
73	10, 72	impbid2 228	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
74		toponuni 21524	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
75	74	neeq2d 3078	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∪ 𝑦) ≠ 𝑋 ↔ (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
76	75	imbi2d 343	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
77	76	2ralbidv 3201	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
78	73, 77	bitr4d 284	1 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083  ∀wal 1535   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ∀wral 3140   ∖ cdif 3935   ∪ cun 3936   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293  {cpr 4571  ∪ cuni 4840  ‘cfv 6357  Topctop 21503  TopOnctopon 21520  Clsdccld 21626  Conncconn 22021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-iota 6316  df-fun 6359  df-fn 6360  df-fv 6365  df-top 21504  df-topon 21521  df-cld 21629  df-conn 22022

This theorem is referenced by:  connsuba  22030  pconnconn  32480