Theorem dfconn2 21222

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 2622	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
2		simpll 790	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝐽 ∈ Conn)
3		simplrl 800	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ∈ 𝐽)
4		simpr1 1067	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ≠ ∅)
5		simplrr 801	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ∈ 𝐽)
6		simpr2 1068	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ≠ ∅)
7		simpr3 1069	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∩ 𝑦) = ∅)
8	1, 2, 3, 4, 5, 6, 7	conndisj 21219	. . . . 5 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)
9	8	ex 450	. . . 4 ⊢ ((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
10	9	ralrimivva 2971	. . 3 ⊢ (𝐽 ∈ Conn → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
11		topontop 20718	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
12	1	cldopn 20835	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (Clsd‘𝐽) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
13	12	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
14		df-3an 1039	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅))
15		ineq2 3808	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)))
16		disjdif 4040	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)) = ∅
17	15, 16	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = ∅)
18	17	biantrud 528	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅)))
19		neeq1 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑦 ≠ ∅ ↔ (∪ 𝐽 ∖ 𝑥) ≠ ∅))
20	19	anbi2d 740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
21	18, 20	bitr3d 270	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
22	14, 21	syl5bb 272	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
23		uneq2 3761	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)))
24		undif2 4044	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)) = (𝑥 ∪ ∪ 𝐽)
25	23, 24	syl6eq 2672	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ ∪ 𝐽))
26	25	neeq1d 2853	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ∪ 𝑦) ≠ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
27	22, 26	imbi12d 334	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
28	27	rspcv 3305	. . . . . . . . . . . . 13 ⊢ ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
29	13, 28	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
30	1	cldss 20833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽)
31	30	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ ∪ 𝐽)
32		ssequn1 3783	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
33	31, 32	sylib 208	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
34		ssdif0 3942	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝐽 ⊆ 𝑥 ↔ (∪ 𝐽 ∖ 𝑥) = ∅)
35		idd 24	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → ∪ 𝐽 ⊆ 𝑥))
36	35, 31	jctild 566	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥)))
37		eqss 3618	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∪ 𝐽 ↔ (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥))
38	36, 37	syl6ibr 242	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → 𝑥 = ∪ 𝐽))
39	34, 38	syl5bir 233	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((∪ 𝐽 ∖ 𝑥) = ∅ → 𝑥 = ∪ 𝐽))
40	33, 39	embantd 59	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → 𝑥 = ∪ 𝐽))
41	40	orim2d 885	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽)))
42		impexp 462	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
43		df-ne 2795	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
45	44	necon4d 2818	. . . . . . . . . . . . . . . . 17 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
46		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
47	46	necon3d 2815	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
48	45, 47	impbii 199	. . . . . . . . . . . . . . . 16 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
49	43, 48	imbi12i 340	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
50		pm4.64 387	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
51	49, 50	bitri 264	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
52	42, 51	bitri 264	. . . . . . . . . . . . 13 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
53		vex 3203	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
54	53	elpr 4198	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∅, ∪ 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽))
55	41, 52, 54	3imtr4g 285	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))
56	29, 55	syld 47	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))
57	56	ex 450	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
58	57	com23 86	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
59	58	imim2d 57	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))))
60		elin 3796	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)))
61	60	imbi1i 339	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
62		impexp 462	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
63	61, 62	bitri 264	. . . . . . . 8 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
64	59, 63	syl6ibr 242	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
65	64	alimdv 1845	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
66		df-ral 2917	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
67		dfss2 3591	. . . . . 6 ⊢ ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
68	65, 66, 67	3imtr4g 285	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
69	1	isconn2 21217	. . . . . 6 ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
70	69	baib 944	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
71	68, 70	sylibrd 249	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
72	11, 71	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
73	10, 72	impbid2 216	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
74		toponuni 20719	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
75	74	neeq2d 2854	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∪ 𝑦) ≠ 𝑋 ↔ (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
76	75	imbi2d 330	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
77	76	2ralbidv 2989	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
78	73, 77	bitr4d 271	1 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1037  ∀wal 1481   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912   ∖ cdif 3571   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  {cpr 4179  ∪ cuni 4436  ‘cfv 5888  Topctop 20698  TopOnctopon 20715  Clsdccld 20820  Conncconn 21214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896  df-top 20699  df-topon 20716  df-cld 20823  df-conn 21215

This theorem is referenced by:  connsuba  21223  pconnconn  31213