Theorem dfconn2 23427

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 2737	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
2		simpll 767	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝐽 ∈ Conn)
3		simplrl 777	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ∈ 𝐽)
4		simpr1 1195	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ≠ ∅)
5		simplrr 778	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ∈ 𝐽)
6		simpr2 1196	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ≠ ∅)
7		simpr3 1197	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∩ 𝑦) = ∅)
8	1, 2, 3, 4, 5, 6, 7	conndisj 23424	. . . . 5 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)
9	8	ex 412	. . . 4 ⊢ ((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
10	9	ralrimivva 3202	. . 3 ⊢ (𝐽 ∈ Conn → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
11		topontop 22919	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
12	1	cldopn 23039	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (Clsd‘𝐽) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
13	12	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
14		df-3an 1089	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅))
15		ineq2 4214	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)))
16		disjdif 4472	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)) = ∅
17	15, 16	eqtrdi 2793	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = ∅)
18	17	biantrud 531	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅)))
19		neeq1 3003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑦 ≠ ∅ ↔ (∪ 𝐽 ∖ 𝑥) ≠ ∅))
20	19	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
21	18, 20	bitr3d 281	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
22	14, 21	bitrid 283	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
23		uneq2 4162	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)))
24		undif2 4477	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)) = (𝑥 ∪ ∪ 𝐽)
25	23, 24	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ ∪ 𝐽))
26	25	neeq1d 3000	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ∪ 𝑦) ≠ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
27	22, 26	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
28	27	rspcv 3618	. . . . . . . . . . . . 13 ⊢ ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
29	13, 28	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
30	1	cldss 23037	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽)
31	30	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ ∪ 𝐽)
32		ssequn1 4186	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
33	31, 32	sylib 218	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
34		ssdif0 4366	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝐽 ⊆ 𝑥 ↔ (∪ 𝐽 ∖ 𝑥) = ∅)
35		idd 24	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → ∪ 𝐽 ⊆ 𝑥))
36	35, 31	jctild 525	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥)))
37		eqss 3999	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∪ 𝐽 ↔ (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥))
38	36, 37	imbitrrdi 252	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → 𝑥 = ∪ 𝐽))
39	34, 38	biimtrrid 243	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((∪ 𝐽 ∖ 𝑥) = ∅ → 𝑥 = ∪ 𝐽))
40	33, 39	embantd 59	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → 𝑥 = ∪ 𝐽))
41	40	orim2d 969	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽)))
42		impexp 450	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
43		df-ne 2941	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
45	44	necon4d 2964	. . . . . . . . . . . . . . . . 17 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
46		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
47	46	necon3d 2961	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
48	45, 47	impbii 209	. . . . . . . . . . . . . . . 16 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
49	43, 48	imbi12i 350	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
50		pm4.64 850	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
51	49, 50	bitri 275	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
52	42, 51	bitri 275	. . . . . . . . . . . . 13 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
53		vex 3484	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
54	53	elpr 4650	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∅, ∪ 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽))
55	41, 52, 54	3imtr4g 296	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))
56	29, 55	syld 47	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))
57	56	ex 412	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
58	57	com23 86	. . . . . . . . 9 ⊢ (𝐽 ∈ Top → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
59	58	imim2d 57	. . . . . . . 8 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽}))))
60		elin 3967	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)))
61	60	imbi1i 349	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
62		impexp 450	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
63	61, 62	bitri 275	. . . . . . . 8 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
64	59, 63	imbitrrdi 252	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
65	64	alimdv 1916	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
66		df-ral 3062	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
67		df-ss 3968	. . . . . 6 ⊢ ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
68	65, 66, 67	3imtr4g 296	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
69	1	isconn2 23422	. . . . . 6 ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
70	69	baib 535	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
71	68, 70	sylibrd 259	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
72	11, 71	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
73	10, 72	impbid2 226	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
74		toponuni 22920	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
75	74	neeq2d 3001	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∪ 𝑦) ≠ 𝑋 ↔ (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
76	75	imbi2d 340	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
77	76	2ralbidv 3221	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
78	73, 77	bitr4d 282	1 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  {cpr 4628  ∪ cuni 4907  ‘cfv 6561  Topctop 22899  TopOnctopon 22916  Clsdccld 23024  Conncconn 23419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569  df-top 22900  df-topon 22917  df-cld 23027  df-conn 23420

This theorem is referenced by:  connsuba  23428  pconnconn  35236