MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfconn2 Structured version   Visualization version   GIF version

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
StepHypRef 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 ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) = ∅)
81, 2, 3, 4, 5, 6, 7conndisj 22767 . . . . 5 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) ≠ 𝐽)
98ex 413 . . . 4 ((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
109ralrimivva 3197 . . 3 (𝐽 ∈ Conn → ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
11 topontop 22262 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
121cldopn 22382 . . . . . . . . . . . . . 14 (𝑥 ∈ (Clsd‘𝐽) → ( 𝐽𝑥) ∈ 𝐽)
1312adantl 482 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥) ∈ 𝐽)
14 df-3an 1089 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅))
15 ineq2 4166 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∩ ( 𝐽𝑥)))
16 disjdif 4431 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∩ ( 𝐽𝑥)) = ∅
1715, 16eqtrdi 2792 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = ∅)
1817biantrud 532 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅)))
19 neeq1 3006 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑦 ≠ ∅ ↔ ( 𝐽𝑥) ≠ ∅))
2019anbi2d 629 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2118, 20bitr3d 280 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2214, 21bitrid 282 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
23 uneq2 4117 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∪ ( 𝐽𝑥)))
24 undif2 4436 . . . . . . . . . . . . . . . . 17 (𝑥 ∪ ( 𝐽𝑥)) = (𝑥 𝐽)
2523, 24eqtrdi 2792 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 𝐽))
2625neeq1d 3003 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥𝑦) ≠ 𝐽 ↔ (𝑥 𝐽) ≠ 𝐽))
2722, 26imbi12d 344 . . . . . . . . . . . . . 14 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2827rspcv 3577 . . . . . . . . . . . . 13 (( 𝐽𝑥) ∈ 𝐽 → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2913, 28syl 17 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
301cldss 22380 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (Clsd‘𝐽) → 𝑥 𝐽)
3130adantl 482 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 𝐽)
32 ssequn1 4140 . . . . . . . . . . . . . . . 16 (𝑥 𝐽 ↔ (𝑥 𝐽) = 𝐽)
3331, 32sylib 217 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 𝐽) = 𝐽)
34 ssdif0 4323 . . . . . . . . . . . . . . . 16 ( 𝐽𝑥 ↔ ( 𝐽𝑥) = ∅)
35 idd 24 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 𝐽𝑥))
3635, 31jctild 526 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 → (𝑥 𝐽 𝐽𝑥)))
37 eqss 3959 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐽 ↔ (𝑥 𝐽 𝐽𝑥))
3836, 37syl6ibr 251 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥𝑥 = 𝐽))
3934, 38biimtrrid 242 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (( 𝐽𝑥) = ∅ → 𝑥 = 𝐽))
4033, 39embantd 59 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → 𝑥 = 𝐽))
4140orim2d 965 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = 𝐽)))
42 impexp 451 . . . . . . . . . . . . . 14 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)))
43 df-ne 2944 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44 id 22 . . . . . . . . . . . . . . . . . 18 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4544necon4d 2967 . . . . . . . . . . . . . . . . 17 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
46 id 22 . . . . . . . . . . . . . . . . . 18 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4746necon3d 2964 . . . . . . . . . . . . . . . . 17 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4845, 47impbii 208 . . . . . . . . . . . . . . . 16 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) ↔ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4943, 48imbi12i 350 . . . . . . . . . . . . . . 15 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
50 pm4.64 847 . . . . . . . . . . . . . . 15 ((¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5149, 50bitri 274 . . . . . . . . . . . . . 14 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5242, 51bitri 274 . . . . . . . . . . . . 13 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
53 vex 3449 . . . . . . . . . . . . . 14 𝑥 ∈ V
5453elpr 4609 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝐽))
5541, 52, 543imtr4g 295 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5629, 55syld 47 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5756ex 413 . . . . . . . . . 10 (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽})))
5857com23 86 . . . . . . . . 9 (𝐽 ∈ Top → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
5958imim2d 57 . . . . . . . 8 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽}))))
60 elin 3926 . . . . . . . . . 10 (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥𝐽𝑥 ∈ (Clsd‘𝐽)))
6160imbi1i 349 . . . . . . . . 9 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ ((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
62 impexp 451 . . . . . . . . 9 (((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6361, 62bitri 274 . . . . . . . 8 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6459, 63syl6ibr 251 . . . . . . 7 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
6564alimdv 1919 . . . . . 6 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
66 df-ral 3065 . . . . . 6 (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
67 dfss2 3930 . . . . . 6 ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
6865, 66, 673imtr4g 295 . . . . 5 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
691isconn2 22765 . . . . . 6 (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7069baib 536 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7168, 70sylibrd 258 . . . 4 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7211, 71syl 17 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7310, 72impbid2 225 . 2 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
74 toponuni 22263 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7574neeq2d 3004 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → ((𝑥𝑦) ≠ 𝑋 ↔ (𝑥𝑦) ≠ 𝐽))
7675imbi2d 340 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
77762ralbidv 3212 . 2 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
7873, 77bitr4d 281 1 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋)))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator