Theorem dfconn2 23402

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 2739	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
2		simpll 772	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝐽 ∈ Conn)
3		simplrl 782	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ∈ 𝐽)
4		simpr1 1201	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ≠ ∅)
5		simplrr 783	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ∈ 𝐽)
6		simpr2 1202	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ≠ ∅)
7		simpr3 1203	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∩ 𝑦) = ∅)
8	1, 2, 3, 4, 5, 6, 7	conndisj 23399	. . . . 5 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)
9	8	ex 413	. . . 4 ⊢ ((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
10	9	ralrimivva 3182	. . 3 ⊢ (𝐽 ∈ Conn → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
11		topontop 22896	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
12	1	cldopn 23014	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (Clsd‘𝐽) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
13	12	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
14		df-3an 1094	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅))
15		ineq2 4143	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)))
16		disjdif 4400	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)) = ∅
17	15, 16	eqtrdi 2790	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = ∅)
18	17	biantrud 536	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅)))
19		neeq1 2996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑦 ≠ ∅ ↔ (∪ 𝐽 ∖ 𝑥) ≠ ∅))
20	19	anbi2d 636	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
21	18, 20	bitr3d 282	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
22	14, 21	bitrid 284	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
23		uneq2 4092	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)))
24		undif2 4405	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)) = (𝑥 ∪ ∪ 𝐽)
25	23, 24	eqtrdi 2790	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ ∪ 𝐽))
26	25	neeq1d 2993	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ∪ 𝑦) ≠ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
27	22, 26	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
28	27	rspcv 3556	. . . . . . . . . . . . 13 ⊢ ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
29	13, 28	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
30	1	cldss 23012	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽)
31	30	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ ∪ 𝐽)
32		ssequn1 4115	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
33	31, 32	sylib 219	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
34		ssdif0 4294	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝐽 ⊆ 𝑥 ↔ (∪ 𝐽 ∖ 𝑥) = ∅)
35		idd 24	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → ∪ 𝐽 ⊆ 𝑥))
36	35, 31	jctild 530	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥)))
37		eqss 3930	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∪ 𝐽 ↔ (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥))
38	36, 37	imbitrrdi 253	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → 𝑥 = ∪ 𝐽))
39	34, 38	biimtrrid 244	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((∪ 𝐽 ∖ 𝑥) = ∅ → 𝑥 = ∪ 𝐽))
40	33, 39	embantd 59	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → 𝑥 = ∪ 𝐽))
41	40	orim2d 974	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽)))
42		impexp 451	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
43		df-ne 2935	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
45	44	necon4d 2958	. . . . . . . . . . . . . . . . 17 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
46		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
47	46	necon3d 2955	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
48	45, 47	impbii 210	. . . . . . . . . . . . . . . 16 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
49	43, 48	imbi12i 351	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
50		pm4.64 855	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
51	49, 50	bitri 276	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
52	42, 51	bitri 276	. . . . . . . . . . . . 13 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
53		vex 3435	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
54	53	elpr 4580	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∅, ∪ 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽))
55	41, 52, 54	3imtr4g 297	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))
56	29, 55	syld 47	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))
57	56	ex 413	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
58	57	com23 86	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
59	58	imim2d 57	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))))
60		elin 3899	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)))
61	60	imbi1i 350	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
62		impexp 451	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
63	61, 62	bitri 276	. . . . . . . 8 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
64	59, 63	imbitrrdi 253	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
65	64	alimdv 1923	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
66		df-ral 3054	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
67		df-ss 3900	. . . . . 6 ⊢ ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
68	65, 66, 67	3imtr4g 297	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
69	1	isconn2 23397	. . . . . 6 ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
70	69	baib 540	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
71	68, 70	sylibrd 260	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
72	11, 71	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
73	10, 72	impbid2 227	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
74		toponuni 22897	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
75	74	neeq2d 2994	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∪ 𝑦) ≠ 𝑋 ↔ (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
76	75	imbi2d 341	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
77	76	2ralbidv 3203	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
78	73, 77	bitr4d 283	1 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092  ∀wal 1545   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4261  {cpr 4557  ∪ cuni 4838  ‘cfv 6485  Topctop 22876  TopOnctopon 22893  Clsdccld 22999  Conncconn 23394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fn 6488  df-fv 6493  df-top 22877  df-topon 22894  df-cld 23002  df-conn 23395

This theorem is referenced by:  connsuba  23403  pconnconn  35459