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

Theorem dfconn2 21270
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 2651 . . . . . 6 𝐽 = 𝐽
2 simpll 805 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝐽 ∈ Conn)
3 simplrl 817 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑥𝐽)
4 simpr1 1087 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑥 ≠ ∅)
5 simplrr 818 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑦𝐽)
6 simpr2 1088 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑦 ≠ ∅)
7 simpr3 1089 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) = ∅)
81, 2, 3, 4, 5, 6, 7conndisj 21267 . . . . 5 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) ≠ 𝐽)
98ex 449 . . . 4 ((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
109ralrimivva 3000 . . 3 (𝐽 ∈ Conn → ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
11 topontop 20766 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
121cldopn 20883 . . . . . . . . . . . . . 14 (𝑥 ∈ (Clsd‘𝐽) → ( 𝐽𝑥) ∈ 𝐽)
1312adantl 481 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥) ∈ 𝐽)
14 df-3an 1056 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅))
15 ineq2 3841 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∩ ( 𝐽𝑥)))
16 disjdif 4073 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∩ ( 𝐽𝑥)) = ∅
1715, 16syl6eq 2701 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = ∅)
1817biantrud 527 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅)))
19 neeq1 2885 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑦 ≠ ∅ ↔ ( 𝐽𝑥) ≠ ∅))
2019anbi2d 740 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2118, 20bitr3d 270 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2214, 21syl5bb 272 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
23 uneq2 3794 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∪ ( 𝐽𝑥)))
24 undif2 4077 . . . . . . . . . . . . . . . . 17 (𝑥 ∪ ( 𝐽𝑥)) = (𝑥 𝐽)
2523, 24syl6eq 2701 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 𝐽))
2625neeq1d 2882 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥𝑦) ≠ 𝐽 ↔ (𝑥 𝐽) ≠ 𝐽))
2722, 26imbi12d 333 . . . . . . . . . . . . . 14 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2827rspcv 3336 . . . . . . . . . . . . 13 (( 𝐽𝑥) ∈ 𝐽 → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2913, 28syl 17 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
301cldss 20881 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (Clsd‘𝐽) → 𝑥 𝐽)
3130adantl 481 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 𝐽)
32 ssequn1 3816 . . . . . . . . . . . . . . . 16 (𝑥 𝐽 ↔ (𝑥 𝐽) = 𝐽)
3331, 32sylib 208 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 𝐽) = 𝐽)
34 ssdif0 3975 . . . . . . . . . . . . . . . 16 ( 𝐽𝑥 ↔ ( 𝐽𝑥) = ∅)
35 idd 24 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 𝐽𝑥))
3635, 31jctild 565 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 → (𝑥 𝐽 𝐽𝑥)))
37 eqss 3651 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐽 ↔ (𝑥 𝐽 𝐽𝑥))
3836, 37syl6ibr 242 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥𝑥 = 𝐽))
3934, 38syl5bir 233 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (( 𝐽𝑥) = ∅ → 𝑥 = 𝐽))
4033, 39embantd 59 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → 𝑥 = 𝐽))
4140orim2d 903 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = 𝐽)))
42 impexp 461 . . . . . . . . . . . . . 14 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)))
43 df-ne 2824 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44 id 22 . . . . . . . . . . . . . . . . . 18 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4544necon4d 2847 . . . . . . . . . . . . . . . . 17 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
46 id 22 . . . . . . . . . . . . . . . . . 18 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4746necon3d 2844 . . . . . . . . . . . . . . . . 17 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4845, 47impbii 199 . . . . . . . . . . . . . . . 16 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) ↔ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4943, 48imbi12i 339 . . . . . . . . . . . . . . 15 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
50 pm4.64 386 . . . . . . . . . . . . . . 15 ((¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5149, 50bitri 264 . . . . . . . . . . . . . 14 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5242, 51bitri 264 . . . . . . . . . . . . 13 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
53 vex 3234 . . . . . . . . . . . . . 14 𝑥 ∈ V
5453elpr 4231 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝐽))
5541, 52, 543imtr4g 285 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5629, 55syld 47 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5756ex 449 . . . . . . . . . 10 (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽})))
5857com23 86 . . . . . . . . 9 (𝐽 ∈ Top → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
5958imim2d 57 . . . . . . . 8 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽}))))
60 elin 3829 . . . . . . . . . 10 (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥𝐽𝑥 ∈ (Clsd‘𝐽)))
6160imbi1i 338 . . . . . . . . 9 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ ((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
62 impexp 461 . . . . . . . . 9 (((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6361, 62bitri 264 . . . . . . . 8 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6459, 63syl6ibr 242 . . . . . . 7 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
6564alimdv 1885 . . . . . 6 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
66 df-ral 2946 . . . . . 6 (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
67 dfss2 3624 . . . . . 6 ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
6865, 66, 673imtr4g 285 . . . . 5 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
691isconn2 21265 . . . . . 6 (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7069baib 964 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7168, 70sylibrd 249 . . . 4 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7211, 71syl 17 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7310, 72impbid2 216 . 2 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
74 toponuni 20767 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7574neeq2d 2883 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → ((𝑥𝑦) ≠ 𝑋 ↔ (𝑥𝑦) ≠ 𝐽))
7675imbi2d 329 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
77762ralbidv 3018 . 2 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
7873, 77bitr4d 271 1 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054  wal 1521   = wceq 1523  wcel 2030  wne 2823  wral 2941  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  {cpr 4212   cuni 4468  cfv 5926  Topctop 20746  TopOnctopon 20763  Clsdccld 20868  Conncconn 21262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934  df-top 20747  df-topon 20764  df-cld 20871  df-conn 21263
This theorem is referenced by:  connsuba  21271  pconnconn  31339
  Copyright terms: Public domain W3C validator