Metamath Proof Explorer


Definition df-pconn

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 PConn=jTop|xjyjfIICnjf0=xf1=y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpconn classPConn
1 vj setvarj
2 ctop classTop
3 vx setvarx
4 1 cv setvarj
5 4 cuni classj
6 vy setvary
7 vf setvarf
8 cii classII
9 ccn classCn
10 8 4 9 co classIICnj
11 7 cv setvarf
12 cc0 class0
13 12 11 cfv classf0
14 3 cv setvarx
15 13 14 wceq wfff0=x
16 c1 class1
17 16 11 cfv classf1
18 6 cv setvary
19 17 18 wceq wfff1=y
20 15 19 wa wfff0=xf1=y
21 20 7 10 wrex wfffIICnjf0=xf1=y
22 21 6 5 wral wffyjfIICnjf0=xf1=y
23 22 3 5 wral wffxjyjfIICnjf0=xf1=y
24 23 1 2 crab classjTop|xjyjfIICnjf0=xf1=y
25 0 24 wceq wffPConn=jTop|xjyjfIICnjf0=xf1=y