Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pconnconn Structured version   Visualization version   GIF version

Theorem pconnconn 32878
Description: A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
pconnconn (𝐽 ∈ PConn → 𝐽 ∈ Conn)

Proof of Theorem pconnconn
Dummy variables 𝑎 𝑏 𝑓 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-3an 1091 . . . 4 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) ↔ ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅))
2 n0 4251 . . . . . . . 8 (𝑥 ≠ ∅ ↔ ∃𝑎 𝑎𝑥)
3 n0 4251 . . . . . . . 8 (𝑦 ≠ ∅ ↔ ∃𝑏 𝑏𝑦)
42, 3anbi12i 630 . . . . . . 7 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ (∃𝑎 𝑎𝑥 ∧ ∃𝑏 𝑏𝑦))
5 exdistrv 1964 . . . . . . 7 (∃𝑎𝑏(𝑎𝑥𝑏𝑦) ↔ (∃𝑎 𝑎𝑥 ∧ ∃𝑏 𝑏𝑦))
64, 5bitr4i 281 . . . . . 6 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ↔ ∃𝑎𝑏(𝑎𝑥𝑏𝑦))
7 simpll 767 . . . . . . . . . 10 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → 𝐽 ∈ PConn)
8 simprll 779 . . . . . . . . . . 11 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → 𝑎𝑥)
9 simplrl 777 . . . . . . . . . . 11 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → 𝑥𝐽)
10 elunii 4814 . . . . . . . . . . 11 ((𝑎𝑥𝑥𝐽) → 𝑎 𝐽)
118, 9, 10syl2anc 587 . . . . . . . . . 10 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → 𝑎 𝐽)
12 simprlr 780 . . . . . . . . . . 11 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → 𝑏𝑦)
13 simplrr 778 . . . . . . . . . . 11 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → 𝑦𝐽)
14 elunii 4814 . . . . . . . . . . 11 ((𝑏𝑦𝑦𝐽) → 𝑏 𝐽)
1512, 13, 14syl2anc 587 . . . . . . . . . 10 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → 𝑏 𝐽)
16 eqid 2734 . . . . . . . . . . 11 𝐽 = 𝐽
1716pconncn 32871 . . . . . . . . . 10 ((𝐽 ∈ PConn ∧ 𝑎 𝐽𝑏 𝐽) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏))
187, 11, 15, 17syl3anc 1373 . . . . . . . . 9 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏))
19 simplrr 778 . . . . . . . . . . . . 13 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑥𝑦) = ∅)
20 simplrr 778 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽) → (𝑓‘1) = 𝑏)
2120adantl 485 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑓‘1) = 𝑏)
22 iiuni 23750 . . . . . . . . . . . . . . . . 17 (0[,]1) = II
23 iiconn 23756 . . . . . . . . . . . . . . . . . 18 II ∈ Conn
2423a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → II ∈ Conn)
25 simprll 779 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑓 ∈ (II Cn 𝐽))
269adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑥𝐽)
27 uncom 4057 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑥) = (𝑥𝑦)
28 simprr 773 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑥𝑦) = 𝐽)
2927, 28syl5eq 2786 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑦𝑥) = 𝐽)
3013adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑦𝐽)
31 elssuni 4841 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝐽𝑦 𝐽)
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑦 𝐽)
33 incom 4105 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝑥) = (𝑥𝑦)
3433, 19syl5eq 2786 . . . . . . . . . . . . . . . . . . . 20 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑦𝑥) = ∅)
35 uneqdifeq 4394 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 𝐽 ∧ (𝑦𝑥) = ∅) → ((𝑦𝑥) = 𝐽 ↔ ( 𝐽𝑦) = 𝑥))
3632, 34, 35syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → ((𝑦𝑥) = 𝐽 ↔ ( 𝐽𝑦) = 𝑥))
3729, 36mpbid 235 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → ( 𝐽𝑦) = 𝑥)
38 pconntop 32872 . . . . . . . . . . . . . . . . . . . 20 (𝐽 ∈ PConn → 𝐽 ∈ Top)
3938ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝐽 ∈ Top)
4016opncld 21902 . . . . . . . . . . . . . . . . . . 19 ((𝐽 ∈ Top ∧ 𝑦𝐽) → ( 𝐽𝑦) ∈ (Clsd‘𝐽))
4139, 30, 40syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → ( 𝐽𝑦) ∈ (Clsd‘𝐽))
4237, 41eqeltrrd 2835 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑥 ∈ (Clsd‘𝐽))
43 0elunit 13040 . . . . . . . . . . . . . . . . . 18 0 ∈ (0[,]1)
4443a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 0 ∈ (0[,]1))
45 simplrl 777 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽) → (𝑓‘0) = 𝑎)
4645adantl 485 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑓‘0) = 𝑎)
478adantr 484 . . . . . . . . . . . . . . . . . 18 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑎𝑥)
4846, 47eqeltrd 2834 . . . . . . . . . . . . . . . . 17 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑓‘0) ∈ 𝑥)
4922, 24, 25, 26, 42, 44, 48conncn 22295 . . . . . . . . . . . . . . . 16 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑓:(0[,]1)⟶𝑥)
50 1elunit 13041 . . . . . . . . . . . . . . . 16 1 ∈ (0[,]1)
51 ffvelrn 6891 . . . . . . . . . . . . . . . 16 ((𝑓:(0[,]1)⟶𝑥 ∧ 1 ∈ (0[,]1)) → (𝑓‘1) ∈ 𝑥)
5249, 50, 51sylancl 589 . . . . . . . . . . . . . . 15 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑓‘1) ∈ 𝑥)
5321, 52eqeltrrd 2835 . . . . . . . . . . . . . 14 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑏𝑥)
5412adantr 484 . . . . . . . . . . . . . 14 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → 𝑏𝑦)
55 inelcm 4369 . . . . . . . . . . . . . 14 ((𝑏𝑥𝑏𝑦) → (𝑥𝑦) ≠ ∅)
5653, 54, 55syl2anc 587 . . . . . . . . . . . . 13 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → (𝑥𝑦) ≠ ∅)
5719, 56pm2.21ddne 3019 . . . . . . . . . . . 12 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ ((𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏)) ∧ (𝑥𝑦) = 𝐽)) → ¬ (𝑥𝑦) = 𝐽)
5857expr 460 . . . . . . . . . . 11 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ (𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏))) → ((𝑥𝑦) = 𝐽 → ¬ (𝑥𝑦) = 𝐽))
5958pm2.01d 193 . . . . . . . . . 10 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ (𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏))) → ¬ (𝑥𝑦) = 𝐽)
6059neqned 2942 . . . . . . . . 9 ((((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) ∧ (𝑓 ∈ (II Cn 𝐽) ∧ ((𝑓‘0) = 𝑎 ∧ (𝑓‘1) = 𝑏))) → (𝑥𝑦) ≠ 𝐽)
6118, 60rexlimddv 3203 . . . . . . . 8 (((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) ∧ ((𝑎𝑥𝑏𝑦) ∧ (𝑥𝑦) = ∅)) → (𝑥𝑦) ≠ 𝐽)
6261exp32 424 . . . . . . 7 ((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) → ((𝑎𝑥𝑏𝑦) → ((𝑥𝑦) = ∅ → (𝑥𝑦) ≠ 𝐽)))
6362exlimdvv 1942 . . . . . 6 ((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) → (∃𝑎𝑏(𝑎𝑥𝑏𝑦) → ((𝑥𝑦) = ∅ → (𝑥𝑦) ≠ 𝐽)))
646, 63syl5bi 245 . . . . 5 ((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) → ((𝑥𝑦) = ∅ → (𝑥𝑦) ≠ 𝐽)))
6564impd 414 . . . 4 ((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) → (((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅) ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
661, 65syl5bi 245 . . 3 ((𝐽 ∈ PConn ∧ (𝑥𝐽𝑦𝐽)) → ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
6766ralrimivva 3105 . 2 (𝐽 ∈ PConn → ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽))
6816toptopon 21786 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘ 𝐽))
6938, 68sylib 221 . . 3 (𝐽 ∈ PConn → 𝐽 ∈ (TopOn‘ 𝐽))
70 dfconn2 22288 . . 3 (𝐽 ∈ (TopOn‘ 𝐽) → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
7169, 70syl 17 . 2 (𝐽 ∈ PConn → (𝐽 ∈ Conn ↔ ∀𝑥𝐽𝑦𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥𝑦) = ∅) → (𝑥𝑦) ≠ 𝐽)))
7267, 71mpbird 260 1 (𝐽 ∈ PConn → 𝐽 ∈ Conn)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wex 1787  wcel 2110  wne 2935  wral 3054  wrex 3055  cdif 3854  cun 3855  cin 3856  wss 3857  c0 4227   cuni 4809  wf 6365  cfv 6369  (class class class)co 7202  0cc0 10712  1c1 10713  [,]cicc 12921  Topctop 21762  TopOnctopon 21779  Clsdccld 21885   Cn ccn 22093  Conncconn 22280  IIcii 23744  PConncpconn 32866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-cnex 10768  ax-resscn 10769  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-addrcl 10773  ax-mulcl 10774  ax-mulrcl 10775  ax-mulcom 10776  ax-addass 10777  ax-mulass 10778  ax-distr 10779  ax-i2m1 10780  ax-1ne0 10781  ax-1rid 10782  ax-rnegex 10783  ax-rrecex 10784  ax-cnre 10785  ax-pre-lttri 10786  ax-pre-lttrn 10787  ax-pre-ltadd 10788  ax-pre-mulgt0 10789  ax-pre-sup 10790
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-int 4850  df-iun 4896  df-br 5044  df-opab 5106  df-mpt 5125  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-pred 6149  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-riota 7159  df-ov 7205  df-oprab 7206  df-mpo 7207  df-om 7634  df-1st 7750  df-2nd 7751  df-wrecs 8036  df-recs 8097  df-rdg 8135  df-er 8380  df-map 8499  df-en 8616  df-dom 8617  df-sdom 8618  df-fin 8619  df-fi 9016  df-sup 9047  df-inf 9048  df-pnf 10852  df-mnf 10853  df-xr 10854  df-ltxr 10855  df-le 10856  df-sub 11047  df-neg 11048  df-div 11473  df-nn 11814  df-2 11876  df-3 11877  df-n0 12074  df-z 12160  df-uz 12422  df-q 12528  df-rp 12570  df-xneg 12687  df-xadd 12688  df-xmul 12689  df-ioo 12922  df-ico 12924  df-icc 12925  df-seq 13558  df-exp 13619  df-cj 14645  df-re 14646  df-im 14647  df-sqrt 14781  df-abs 14782  df-rest 16899  df-topgen 16920  df-psmet 20327  df-xmet 20328  df-met 20329  df-bl 20330  df-mopn 20331  df-top 21763  df-topon 21780  df-bases 21815  df-cld 21888  df-cn 22096  df-conn 22281  df-ii 23746  df-pconn 32868
This theorem is referenced by:  resconn  32893  iinllyconn  32901  cvmlift2lem10  32959  cvmlift3  32975
  Copyright terms: Public domain W3C validator