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

Theorem dfconn2 21203
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 2620 . . . . . 6 𝐽 = 𝐽
2 simpll 789 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝐽 ∈ Conn)
3 simplrl 799 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑥𝐽)
4 simpr1 1065 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑥 ≠ ∅)
5 simplrr 800 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑦𝐽)
6 simpr2 1066 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → 𝑦 ≠ ∅)
7 simpr3 1067 . . . . . 6 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) = ∅)
81, 2, 3, 4, 5, 6, 7conndisj 21200 . . . . 5 (((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) ∧ (𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) ≠ 𝐽)
98ex 450 . . . 4 ((𝐽 ∈ Conn ∧ (𝑥𝐽𝑦𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
109ralrimivva 2968 . . 3 (𝐽 ∈ Conn → ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
11 topontop 20699 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
121cldopn 20816 . . . . . . . . . . . . . 14 (𝑥 ∈ (Clsd‘𝐽) → ( 𝐽𝑥) ∈ 𝐽)
1312adantl 482 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥) ∈ 𝐽)
14 df-3an 1038 . . . . . . . . . . . . . . . 16 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅))
15 ineq2 3800 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∩ ( 𝐽𝑥)))
16 disjdif 4031 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∩ ( 𝐽𝑥)) = ∅
1715, 16syl6eq 2670 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = ∅)
1817biantrud 528 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅)))
19 neeq1 2853 . . . . . . . . . . . . . . . . . 18 (𝑦 = ( 𝐽𝑥) → (𝑦 ≠ ∅ ↔ ( 𝐽𝑥) ≠ ∅))
2019anbi2d 739 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2118, 20bitr3d 270 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
2214, 21syl5bb 272 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ (𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅)))
23 uneq2 3753 . . . . . . . . . . . . . . . . 17 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 ∪ ( 𝐽𝑥)))
24 undif2 4035 . . . . . . . . . . . . . . . . 17 (𝑥 ∪ ( 𝐽𝑥)) = (𝑥 𝐽)
2523, 24syl6eq 2670 . . . . . . . . . . . . . . . 16 (𝑦 = ( 𝐽𝑥) → (𝑥𝑦) = (𝑥 𝐽))
2625neeq1d 2850 . . . . . . . . . . . . . . 15 (𝑦 = ( 𝐽𝑥) → ((𝑥𝑦) ≠ 𝐽 ↔ (𝑥 𝐽) ≠ 𝐽))
2722, 26imbi12d 334 . . . . . . . . . . . . . 14 (𝑦 = ( 𝐽𝑥) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2827rspcv 3300 . . . . . . . . . . . . 13 (( 𝐽𝑥) ∈ 𝐽 → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
2913, 28syl 17 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → ((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽)))
301cldss 20814 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (Clsd‘𝐽) → 𝑥 𝐽)
3130adantl 482 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 𝐽)
32 ssequn1 3775 . . . . . . . . . . . . . . . 16 (𝑥 𝐽 ↔ (𝑥 𝐽) = 𝐽)
3331, 32sylib 208 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑥 𝐽) = 𝐽)
34 ssdif0 3933 . . . . . . . . . . . . . . . 16 ( 𝐽𝑥 ↔ ( 𝐽𝑥) = ∅)
35 idd 24 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 𝐽𝑥))
3635, 31jctild 565 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥 → (𝑥 𝐽 𝐽𝑥)))
37 eqss 3610 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐽 ↔ (𝑥 𝐽 𝐽𝑥))
3836, 37syl6ibr 242 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ( 𝐽𝑥𝑥 = 𝐽))
3934, 38syl5bir 233 . . . . . . . . . . . . . . 15 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (( 𝐽𝑥) = ∅ → 𝑥 = 𝐽))
4033, 39embantd 59 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → 𝑥 = 𝐽))
4140orim2d 884 . . . . . . . . . . . . 13 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → ((𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) → (𝑥 = ∅ ∨ 𝑥 = 𝐽)))
42 impexp 462 . . . . . . . . . . . . . 14 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)))
43 df-ne 2792 . . . . . . . . . . . . . . . 16 (𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅)
44 id 22 . . . . . . . . . . . . . . . . . 18 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4544necon4d 2815 . . . . . . . . . . . . . . . . 17 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
46 id 22 . . . . . . . . . . . . . . . . . 18 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4746necon3d 2812 . . . . . . . . . . . . . . . . 17 (((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅) → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽))
4845, 47impbii 199 . . . . . . . . . . . . . . . 16 ((( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽) ↔ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅))
4943, 48imbi12i 340 . . . . . . . . . . . . . . 15 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
50 pm4.64 387 . . . . . . . . . . . . . . 15 ((¬ 𝑥 = ∅ → ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5149, 50bitri 264 . . . . . . . . . . . . . 14 ((𝑥 ≠ ∅ → (( 𝐽𝑥) ≠ ∅ → (𝑥 𝐽) ≠ 𝐽)) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
5242, 51bitri 264 . . . . . . . . . . . . 13 (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) ↔ (𝑥 = ∅ ∨ ((𝑥 𝐽) = 𝐽 → ( 𝐽𝑥) = ∅)))
53 vex 3198 . . . . . . . . . . . . . 14 𝑥 ∈ V
5453elpr 4189 . . . . . . . . . . . . 13 (𝑥 ∈ {∅, 𝐽} ↔ (𝑥 = ∅ ∨ 𝑥 = 𝐽))
5541, 52, 543imtr4g 285 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((𝑥 ≠ ∅ ∧ ( 𝐽𝑥) ≠ ∅) → (𝑥 𝐽) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5629, 55syld 47 . . . . . . . . . . 11 ((𝐽 ∈ Top ∧ 𝑥 ∈ (Clsd‘𝐽)) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽}))
5756ex 450 . . . . . . . . . 10 (𝐽 ∈ Top → (𝑥 ∈ (Clsd‘𝐽) → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝑥 ∈ {∅, 𝐽})))
5857com23 86 . . . . . . . . 9 (𝐽 ∈ Top → (∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
5958imim2d 57 . . . . . . . 8 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽}))))
60 elin 3788 . . . . . . . . . 10 (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ (𝑥𝐽𝑥 ∈ (Clsd‘𝐽)))
6160imbi1i 339 . . . . . . . . 9 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ ((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
62 impexp 462 . . . . . . . . 9 (((𝑥𝐽𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6361, 62bitri 264 . . . . . . . 8 ((𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}) ↔ (𝑥𝐽 → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ∈ {∅, 𝐽})))
6459, 63syl6ibr 242 . . . . . . 7 (𝐽 ∈ Top → ((𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → (𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
6564alimdv 1843 . . . . . 6 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)) → ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽})))
66 df-ral 2914 . . . . . 6 (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) ↔ ∀𝑥(𝑥𝐽 → ∀𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
67 dfss2 3584 . . . . . 6 ((𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽} ↔ ∀𝑥(𝑥 ∈ (𝐽 ∩ (Clsd‘𝐽)) → 𝑥 ∈ {∅, 𝐽}))
6865, 66, 673imtr4g 285 . . . . 5 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
691isconn2 21198 . . . . . 6 (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7069baib 943 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Conn ↔ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝐽}))
7168, 70sylibrd 249 . . . 4 (𝐽 ∈ Top → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7211, 71syl 17 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽) → 𝐽 ∈ Conn))
7310, 72impbid2 216 . 2 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
74 toponuni 20700 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
7574neeq2d 2851 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → ((𝑥𝑦) ≠ 𝑋 ↔ (𝑥𝑦) ≠ 𝐽))
7675imbi2d 330 . . 3 (𝐽 ∈ (TopOn‘𝑋) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
77762ralbidv 2986 . 2 (𝐽 ∈ (TopOn‘𝑋) → (∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋) ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
7873, 77bitr4d 271 1 (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036  wal 1479   = wceq 1481  wcel 1988  wne 2791  wral 2909  cdif 3564  cun 3565  cin 3566  wss 3567  c0 3907  {cpr 4170   cuni 4427  cfv 5876  Topctop 20679  TopOnctopon 20696  Clsdccld 20801  Conncconn 21195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-iota 5839  df-fun 5878  df-fn 5879  df-fv 5884  df-top 20680  df-topon 20697  df-cld 20804  df-conn 21196
This theorem is referenced by:  connsuba  21204  pconnconn  31187
  Copyright terms: Public domain W3C validator