Theorem dfconn2 22770

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 2736	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
2		simpll 765	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝐽 ∈ Conn)
3		simplrl 775	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ∈ 𝐽)
4		simpr1 1194	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑥 ≠ ∅)
5		simplrr 776	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ∈ 𝐽)
6		simpr2 1195	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → 𝑦 ≠ ∅)
7		simpr3 1196	. . . . . 6 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∩ 𝑦) = ∅)
8	1, 2, 3, 4, 5, 6, 7	conndisj 22767	. . . . 5 ⊢ (((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅)) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)
9	8	ex 413	. . . 4 ⊢ ((𝐽 ∈ Conn ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
10	9	ralrimivva 3197	. . 3 ⊢ (𝐽 ∈ Conn → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
11		topontop 22262	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
12	1	cldopn 22382	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (Clsd‘𝐽) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
13	12	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)
14		df-3an 1089	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅))
15		ineq2 4166	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)))
16		disjdif 4431	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∩ (∪ 𝐽 ∖ 𝑥)) = ∅
17	15, 16	eqtrdi 2792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∩ 𝑦) = ∅)
18	17	biantrud 532	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅)))
19		neeq1 3006	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑦 ≠ ∅ ↔ (∪ 𝐽 ∖ 𝑥) ≠ ∅))
20	19	anbi2d 629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
21	18, 20	bitr3d 280	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
22	14, 21	bitrid 282	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅)))
23		uneq2 4117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)))
24		undif2 4436	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∪ (∪ 𝐽 ∖ 𝑥)) = (𝑥 ∪ ∪ 𝐽)
25	23, 24	eqtrdi 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (𝑥 ∪ 𝑦) = (𝑥 ∪ ∪ 𝐽))
26	25	neeq1d 3003	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → ((𝑥 ∪ 𝑦) ≠ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
27	22, 26	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (∪ 𝐽 ∖ 𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
28	27	rspcv 3577	. . . . . . . . . . . . 13 ⊢ ((∪ 𝐽 ∖ 𝑥) ∈ 𝐽 → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
29	13, 28	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → ((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
30	1	cldss 22380	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽)
31	30	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ ∪ 𝐽)
32		ssequn1 4140	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ ∪ 𝐽 ↔ (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
33	31, 32	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 ∪ ∪ 𝐽) = ∪ 𝐽)
34		ssdif0 4323	. . . . . . . . . . . . . . . 16 ⊢ (∪ 𝐽 ⊆ 𝑥 ↔ (∪ 𝐽 ∖ 𝑥) = ∅)
35		idd 24	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → ∪ 𝐽 ⊆ 𝑥))
36	35, 31	jctild 526	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥)))
37		eqss 3959	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∪ 𝐽 ↔ (𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥))
38	36, 37	syl6ibr 251	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∪ 𝐽 ⊆ 𝑥 → 𝑥 = ∪ 𝐽))
39	34, 38	biimtrrid 242	. . . . . . . . . . . . . . 15 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((∪ 𝐽 ∖ 𝑥) = ∅ → 𝑥 = ∪ 𝐽))
40	33, 39	embantd 59	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → 𝑥 = ∪ 𝐽))
41	40	orim2d 965	. . . . . . . . . . . . 13 ⊢ ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽)))
42		impexp 451	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)))
43		df-ne 2944	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
45	44	necon4d 2967	. . . . . . . . . . . . . . . . 17 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
46		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
47	46	necon3d 2964	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅) → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽))
48	45, 47	impbii 208	. . . . . . . . . . . . . . . 16 ⊢ (((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅))
49	43, 48	imbi12i 350	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
50		pm4.64 847	. . . . . . . . . . . . . . 15 ⊢ ((¬ 𝑥 = ∅ → ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
51	49, 50	bitri 274	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ≠ ∅ → ((∪ 𝐽 ∖ 𝑥) ≠ ∅ → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
52	42, 51	bitri 274	. . . . . . . . . . . . 13 ⊢ (((𝑥 ≠ ∅ ∧ (∪ 𝐽 ∖ 𝑥) ≠ ∅) → (𝑥 ∪ ∪ 𝐽) ≠ ∪ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 ∪ ∪ 𝐽) = ∪ 𝐽 → (∪ 𝐽 ∖ 𝑥) = ∅)))
53		vex 3449	. . . . . . . . . . . . . 14 ⊢ 𝑥 ∈ V
54	53	elpr 4609	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {∅, ∪ 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽))
55	41, 52, 54	3imtr4g 295	. . . . . . . . . . . 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 3926	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)))
61	60	imbi1i 349	. . . . . . . . 9 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
62		impexp 451	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐽 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
63	61, 62	bitri 274	. . . . . . . 8 ⊢ ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}) ↔ (𝑥 ∈ 𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, ∪ 𝐽})))
64	59, 63	syl6ibr 251	. . . . . . 7 ⊢ (𝐽 ∈ Top → ((𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
65	64	alimdv 1919	. . . . . 6 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽})))
66		df-ral 3065	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) ↔ ∀𝑥(𝑥 ∈ 𝐽 → ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
67		dfss2 3930	. . . . . 6 ⊢ ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, ∪ 𝐽}))
68	65, 66, 67	3imtr4g 295	. . . . 5 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
69	1	isconn2 22765	. . . . . 6 ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
70	69	baib 536	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, ∪ 𝐽}))
71	68, 70	sylibrd 258	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
72	11, 71	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽) → 𝐽 ∈ Conn))
73	10, 72	impbid2 225	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
74		toponuni 22263	. . . . 5 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
75	74	neeq2d 3004	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((𝑥 ∪ 𝑦) ≠ 𝑋 ↔ (𝑥 ∪ 𝑦) ≠ ∪ 𝐽))
76	75	imbi2d 340	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
77	76	2ralbidv 3212	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋) ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ ∪ 𝐽)))
78	73, 77	bitr4d 281	1 ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087  ∀wal 1539   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064   ∖ cdif 3907   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  {cpr 4588  ∪ cuni 4865  ‘cfv 6496  Topctop 22242  TopOnctopon 22259  Clsdccld 22367  Conncconn 22762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-iota 6448  df-fun 6498  df-fn 6499  df-fv 6504  df-top 22243  df-topon 22260  df-cld 22370  df-conn 22763

This theorem is referenced by:  connsuba  22771  pconnconn  33825