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

Theorem dfconn2 21436
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 2806 . . . . . 6 𝐽 = 𝐽
2 simpll 774 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝐽 ∈ Conn)
3 simplrl 786 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑥𝐽)
4 simpr1 1241 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑥 ≠ ∅)
5 simplrr 787 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑦𝐽)
6 simpr2 1243 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑦 ≠ ∅)
7 simpr3 1245 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) = ∅)
81, 2, 3, 4, 5, 6, 7conndisj 21433 . . . . 5 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) ≠ 𝐽)
98ex 399 . . . 4 ((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
109ralrimivva 3159 . . 3 (𝐽 ∈ Conn → ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
11 topontop 20931 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
121cldopn 21049 . . . . . . . . . . . . . 14 (𝑥 ∈ (Clsd‘𝐽) → ( 𝐽𝑥) ∈ 𝐽)
1312adantl 469 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥) ∈ 𝐽)
14 df-3an 1102 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅))
15 ineq2 4007 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∩ ( 𝐽𝑥)))
16 disjdif 4236 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∩ ( 𝐽𝑥)) = ∅
1715, 16syl6eq 2856 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = ∅)
1817biantrud 523 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅)))
19 neeq1 3040 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑦 ≠ ∅ ↔ ( 𝐽𝑥) ≠ ∅))
2019anbi2d 616 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2118, 20bitr3d 272 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2214, 21syl5bb 274 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
23 uneq2 3960 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∪ ( 𝐽𝑥)))
24 undif2 4240 . . . . . . . . . . . . . . . . 17 (𝑥 ∪ ( 𝐽𝑥)) = (𝑥 𝐽)
2523, 24syl6eq 2856 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 𝐽))
2625neeq1d 3037 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥𝑦) ≠ 𝐽 ↔ (𝑥 𝐽) ≠ 𝐽))
2722, 26imbi12d 335 . . . . . . . . . . . . . 14 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2827rspcv 3498 . . . . . . . . . . . . 13 (( 𝐽𝑥) ∈ 𝐽 → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2913, 28syl 17 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
301cldss 21047 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (Clsd‘𝐽) → 𝑥 𝐽)
3130adantl 469 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 𝐽)
32 ssequn1 3982 . . . . . . . . . . . . . . . 16 (𝑥 𝐽 ↔ (𝑥 𝐽) = 𝐽)
3331, 32sylib 209 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 𝐽) = 𝐽)
34 ssdif0 4143 . . . . . . . . . . . . . . . 16 ( 𝐽𝑥 ↔ ( 𝐽𝑥) = ∅)
35 idd 24 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 𝐽𝑥))
3635, 31jctild 517 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 → (𝑥 𝐽 𝐽𝑥)))
37 eqss 3813 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐽 ↔ (𝑥 𝐽 𝐽𝑥))
3836, 37syl6ibr 243 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥𝑥 = 𝐽))
3934, 38syl5bir 234 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (( 𝐽𝑥) = ∅ → 𝑥 = 𝐽))
4033, 39embantd 59 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → 𝑥 = 𝐽))
4140orim2d 980 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = 𝐽)))
42 impexp 439 . . . . . . . . . . . . . 14 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)))
43 df-ne 2979 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44 id 22 . . . . . . . . . . . . . . . . . 18 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4544necon4d 3002 . . . . . . . . . . . . . . . . 17 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
46 id 22 . . . . . . . . . . . . . . . . . 18 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4746necon3d 2999 . . . . . . . . . . . . . . . . 17 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4845, 47impbii 200 . . . . . . . . . . . . . . . 16 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) ↔ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4943, 48imbi12i 341 . . . . . . . . . . . . . . 15 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
50 pm4.64 867 . . . . . . . . . . . . . . 15 ((¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5149, 50bitri 266 . . . . . . . . . . . . . 14 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5242, 51bitri 266 . . . . . . . . . . . . 13 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
53 vex 3394 . . . . . . . . . . . . . 14 𝑥 ∈ V
5453elpr 4393 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝐽))
5541, 52, 543imtr4g 287 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5629, 55syld 47 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5756ex 399 . . . . . . . . . 10 (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽})))
5857com23 86 . . . . . . . . 9 (𝐽 ∈ Top → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
5958imim2d 57 . . . . . . . 8 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽}))))
60 elin 3995 . . . . . . . . . 10 (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥𝐽𝑥 ∈ (Clsd‘𝐽)))
6160imbi1i 340 . . . . . . . . 9 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ ((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
62 impexp 439 . . . . . . . . 9 (((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6361, 62bitri 266 . . . . . . . 8 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6459, 63syl6ibr 243 . . . . . . 7 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
6564alimdv 2007 . . . . . 6 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
66 df-ral 3101 . . . . . 6 (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
67 dfss2 3786 . . . . . 6 ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
6865, 66, 673imtr4g 287 . . . . 5 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
691isconn2 21431 . . . . . 6 (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7069baib 527 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7168, 70sylibrd 250 . . . 4 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7211, 71syl 17 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7310, 72impbid2 217 . 2 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
74 toponuni 20932 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7574neeq2d 3038 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → ((𝑥𝑦) ≠ 𝑋 ↔ (𝑥𝑦) ≠ 𝐽))
7675imbi2d 331 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
77762ralbidv 3177 . 2 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
7873, 77bitr4d 273 1 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100  wal 1635   = wceq 1637  wcel 2156  wne 2978  wral 3096  cdif 3766  cun 3767  cin 3768  wss 3769  c0 4116  {cpr 4372   cuni 4630  cfv 6101  Topctop 20911  TopOnctopon 20928  Clsdccld 21034  Conncconn 21428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-iota 6064  df-fun 6103  df-fn 6104  df-fv 6109  df-top 20912  df-topon 20929  df-cld 21037  df-conn 21429
This theorem is referenced by:  connsuba  21437  pconnconn  31536
  Copyright terms: Public domain W3C validator