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

Theorem dfconn2 23443
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 2735 . . . . . 6 𝐽 = 𝐽
2 simpll 767 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝐽 ∈ Conn)
3 simplrl 777 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑥𝐽)
4 simpr1 1193 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑥 ≠ ∅)
5 simplrr 778 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑦𝐽)
6 simpr2 1194 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑦 ≠ ∅)
7 simpr3 1195 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) = ∅)
81, 2, 3, 4, 5, 6, 7conndisj 23440 . . . . 5 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) ≠ 𝐽)
98ex 412 . . . 4 ((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
109ralrimivva 3200 . . 3 (𝐽 ∈ Conn → ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
11 topontop 22935 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
121cldopn 23055 . . . . . . . . . . . . . 14 (𝑥 ∈ (Clsd‘𝐽) → ( 𝐽𝑥) ∈ 𝐽)
1312adantl 481 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥) ∈ 𝐽)
14 df-3an 1088 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅))
15 ineq2 4222 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∩ ( 𝐽𝑥)))
16 disjdif 4478 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∩ ( 𝐽𝑥)) = ∅
1715, 16eqtrdi 2791 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = ∅)
1817biantrud 531 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅)))
19 neeq1 3001 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑦 ≠ ∅ ↔ ( 𝐽𝑥) ≠ ∅))
2019anbi2d 630 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2118, 20bitr3d 281 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2214, 21bitrid 283 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
23 uneq2 4172 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∪ ( 𝐽𝑥)))
24 undif2 4483 . . . . . . . . . . . . . . . . 17 (𝑥 ∪ ( 𝐽𝑥)) = (𝑥 𝐽)
2523, 24eqtrdi 2791 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 𝐽))
2625neeq1d 2998 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥𝑦) ≠ 𝐽 ↔ (𝑥 𝐽) ≠ 𝐽))
2722, 26imbi12d 344 . . . . . . . . . . . . . 14 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2827rspcv 3618 . . . . . . . . . . . . 13 (( 𝐽𝑥) ∈ 𝐽 → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2913, 28syl 17 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
301cldss 23053 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (Clsd‘𝐽) → 𝑥 𝐽)
3130adantl 481 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 𝐽)
32 ssequn1 4196 . . . . . . . . . . . . . . . 16 (𝑥 𝐽 ↔ (𝑥 𝐽) = 𝐽)
3331, 32sylib 218 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 𝐽) = 𝐽)
34 ssdif0 4372 . . . . . . . . . . . . . . . 16 ( 𝐽𝑥 ↔ ( 𝐽𝑥) = ∅)
35 idd 24 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 𝐽𝑥))
3635, 31jctild 525 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 → (𝑥 𝐽 𝐽𝑥)))
37 eqss 4011 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐽 ↔ (𝑥 𝐽 𝐽𝑥))
3836, 37imbitrrdi 252 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥𝑥 = 𝐽))
3934, 38biimtrrid 243 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (( 𝐽𝑥) = ∅ → 𝑥 = 𝐽))
4033, 39embantd 59 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → 𝑥 = 𝐽))
4140orim2d 968 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = 𝐽)))
42 impexp 450 . . . . . . . . . . . . . 14 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)))
43 df-ne 2939 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44 id 22 . . . . . . . . . . . . . . . . . 18 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4544necon4d 2962 . . . . . . . . . . . . . . . . 17 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
46 id 22 . . . . . . . . . . . . . . . . . 18 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4746necon3d 2959 . . . . . . . . . . . . . . . . 17 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4845, 47impbii 209 . . . . . . . . . . . . . . . 16 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) ↔ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4943, 48imbi12i 350 . . . . . . . . . . . . . . 15 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
50 pm4.64 849 . . . . . . . . . . . . . . 15 ((¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5149, 50bitri 275 . . . . . . . . . . . . . 14 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5242, 51bitri 275 . . . . . . . . . . . . 13 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
53 vex 3482 . . . . . . . . . . . . . 14 𝑥 ∈ V
5453elpr 4655 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝐽))
5541, 52, 543imtr4g 296 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5629, 55syld 47 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5756ex 412 . . . . . . . . . 10 (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽})))
5857com23 86 . . . . . . . . 9 (𝐽 ∈ Top → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
5958imim2d 57 . . . . . . . 8 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽}))))
60 elin 3979 . . . . . . . . . 10 (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥𝐽𝑥 ∈ (Clsd‘𝐽)))
6160imbi1i 349 . . . . . . . . 9 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ ((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
62 impexp 450 . . . . . . . . 9 (((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6361, 62bitri 275 . . . . . . . 8 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6459, 63imbitrrdi 252 . . . . . . 7 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
6564alimdv 1914 . . . . . 6 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
66 df-ral 3060 . . . . . 6 (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
67 df-ss 3980 . . . . . 6 ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
6865, 66, 673imtr4g 296 . . . . 5 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
691isconn2 23438 . . . . . 6 (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7069baib 535 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7168, 70sylibrd 259 . . . 4 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7211, 71syl 17 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7310, 72impbid2 226 . 2 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
74 toponuni 22936 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7574neeq2d 2999 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → ((𝑥𝑦) ≠ 𝑋 ↔ (𝑥𝑦) ≠ 𝐽))
7675imbi2d 340 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
77762ralbidv 3219 . 2 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
7873, 77bitr4d 282 1 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086  wal 1535   = wceq 1537  wcel 2106  wne 2938  wral 3059  cdif 3960  cun 3961  cin 3962  wss 3963  c0 4339  {cpr 4633   cuni 4912  cfv 6563  Topctop 22915  TopOnctopon 22932  Clsdccld 23040  Conncconn 23435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-iota 6516  df-fun 6565  df-fn 6566  df-fv 6571  df-top 22916  df-topon 22933  df-cld 23043  df-conn 23436
This theorem is referenced by:  connsuba  23444  pconnconn  35216
  Copyright terms: Public domain W3C validator