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 \in Top \| \forall x \in ⋃ j \forall y \in ⋃ j \exists f \in (II Cn j) (f (0) = x \land 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 \land f (1) = y)$
21	20 7 10	wrex	$wff \exists f \in (II Cn j) (f (0) = x \land f (1) = y)$
22	21 6 5	wral	$wff \forall y \in ⋃ j \exists f \in (II Cn j) (f (0) = x \land f (1) = y)$
23	22 3 5	wral	$wff \forall x \in ⋃ j \forall y \in ⋃ j \exists f \in (II Cn j) (f (0) = x \land f (1) = y)$
24	23 1 2	crab	$class \{j \in Top \| \forall x \in ⋃ j \forall y \in ⋃ j \exists f \in (II Cn j) (f (0) = x \land f (1) = y)\}$
25	0 24	wceq	$wff PConn = \{j \in Top \| \forall x \in ⋃ j \forall y \in ⋃ j \exists f \in (II Cn j) (f (0) = x \land f (1) = y)\}$

Metamath Proof Explorer

Definition df-pconn

Detailed syntax breakdown