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 e. Top | A. x e. U. j A. y e. U. j E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpconn	|- PConn
1		vj	|- j
2		ctop	|- Top
3		vx	|- x
4	1	cv	|- j
5	4	cuni	|- U. j
6		vy	|- y
7		vf	|- f
8		cii	|- II
9		ccn	|- Cn
10	8 4 9	co	|- ( II Cn j )
11	7	cv	|- f
12		cc0	|- 0
13	12 11	cfv	|- ( f ` 0 )
14	3	cv	|- x
15	13 14	wceq	|- ( f ` 0 ) = x
16		c1	|- 1
17	16 11	cfv	|- ( f ` 1 )
18	6	cv	|- y
19	17 18	wceq	|- ( f ` 1 ) = y
20	15 19	wa	|- ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
21	20 7 10	wrex	|- E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
22	21 6 5	wral	|- A. y e. U. j E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
23	22 3 5	wral	|- A. x e. U. j A. y e. U. j E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
24	23 1 2	crab	|- { j e. Top | A. x e. U. j A. y e. U. j E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) }
25	0 24	wceq	|- PConn = { j e. Top | A. x e. U. j A. y e. U. j E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) }