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 = j Top | x j y j f II Cn j f 0 = x f 1 = y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpconn class PConn
1 vj setvar j
2 ctop class Top
3 vx setvar x
4 1 cv setvar j
5 4 cuni class j
6 vy setvar y
7 vf setvar f
8 cii class II
9 ccn class Cn
10 8 4 9 co class II Cn j
11 7 cv setvar f
12 cc0 class 0
13 12 11 cfv class f 0
14 3 cv setvar x
15 13 14 wceq wff f 0 = x
16 c1 class 1
17 16 11 cfv class f 1
18 6 cv setvar y
19 17 18 wceq wff f 1 = y
20 15 19 wa wff f 0 = x f 1 = y
21 20 7 10 wrex wff f II Cn j f 0 = x f 1 = y
22 21 6 5 wral wff y j f II Cn j f 0 = x f 1 = y
23 22 3 5 wral wff x j y j f II Cn j f 0 = x f 1 = y
24 23 1 2 crab class j Top | x j y j f II Cn j f 0 = x f 1 = y
25 0 24 wceq wff PConn = j Top | x j y j f II Cn j f 0 = x f 1 = y