Description: Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the closed unit interval) that goes from x to y for any points x , y in the space. (Contributed by Mario Carneiro, 11-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-pconn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cpconn | |
|
1 | vj | |
|
2 | ctop | |
|
3 | vx | |
|
4 | 1 | cv | |
5 | 4 | cuni | |
6 | vy | |
|
7 | vf | |
|
8 | cii | |
|
9 | ccn | |
|
10 | 8 4 9 | co | |
11 | 7 | cv | |
12 | cc0 | |
|
13 | 12 11 | cfv | |
14 | 3 | cv | |
15 | 13 14 | wceq | |
16 | c1 | |
|
17 | 16 11 | cfv | |
18 | 6 | cv | |
19 | 17 18 | wceq | |
20 | 15 19 | wa | |
21 | 20 7 10 | wrex | |
22 | 21 6 5 | wral | |
23 | 22 3 5 | wral | |
24 | 23 1 2 | crab | |
25 | 0 24 | wceq | |