Definition df-pconn 31203

Description: Define the class of path-connected topologies. A topology is path-connected if there is a path (a continuous function from the unit interval) that goes from x to y for any points x , y in the space. (Contributed by Mario Carneiro, 11-Feb-2015.)

Assertion

Ref	Expression
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 ) }

Distinct variable group:   f, j, x, y

Detailed syntax breakdown of Definition df-pconn

Step	Hyp	Ref	Expression
1		cpconn 31201	. 2 class PConn
2		cc0 9936	. . . . . . . . 9 class 0
3		vf	. . . . . . . . . 10 setvar f
4	3	cv 1482	. . . . . . . . 9 class f
5	2, 4	cfv 5888	. . . . . . . 8 class ( f ` 0 )
6		vx	. . . . . . . . 9 setvar x
7	6	cv 1482	. . . . . . . 8 class x
8	5, 7	wceq 1483	. . . . . . 7 wff ( f ` 0 ) = x
9		c1 9937	. . . . . . . . 9 class 1
10	9, 4	cfv 5888	. . . . . . . 8 class ( f ` 1 )
11		vy	. . . . . . . . 9 setvar y
12	11	cv 1482	. . . . . . . 8 class y
13	10, 12	wceq 1483	. . . . . . 7 wff ( f ` 1 ) = y
14	8, 13	wa 384	. . . . . 6 wff ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
15		cii 22678	. . . . . . 7 class II
16		vj	. . . . . . . 8 setvar j
17	16	cv 1482	. . . . . . 7 class j
18		ccn 21028	. . . . . . 7 class Cn
19	15, 17, 18	co 6650	. . . . . 6 class ( II Cn j )
20	14, 3, 19	wrex 2913	. . . . 5 wff E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
21	17	cuni 4436	. . . . 5 class U. j
22	20, 11, 21	wral 2912	. . . 4 wff A. y e. U. j E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
23	22, 6, 21	wral 2912	. . 3 wff A. x e. U. j A. y e. U. j E. f e. ( II Cn j ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
24		ctop 20698	. . 3 class Top
25	23, 16, 24	crab 2916	. 2 class { 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 ) }
26	1, 25	wceq 1483	1 wff 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 ) }

This definition is referenced by:  ispconn  31205