Definition df-pconn 35215

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 𝑥 to 𝑦 for any points 𝑥, 𝑦 in the space. (Contributed by Mario Carneiro, 11-Feb-2015.)

Assertion

Ref	Expression
df-pconn	⊢ PConn = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}

Distinct variable group:   𝑓,𝑗,𝑥,𝑦

Detailed syntax breakdown of Definition df-pconn

Step	Hyp	Ref	Expression
1		cpconn 35213	. 2 class PConn
2		cc0 11075	. . . . . . . . 9 class 0
3		vf	. . . . . . . . . 10 setvar 𝑓
4	3	cv 1539	. . . . . . . . 9 class 𝑓
5	2, 4	cfv 6514	. . . . . . . 8 class (𝑓‘0)
6		vx	. . . . . . . . 9 setvar 𝑥
7	6	cv 1539	. . . . . . . 8 class 𝑥
8	5, 7	wceq 1540	. . . . . . 7 wff (𝑓‘0) = 𝑥
9		c1 11076	. . . . . . . . 9 class 1
10	9, 4	cfv 6514	. . . . . . . 8 class (𝑓‘1)
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1539	. . . . . . . 8 class 𝑦
13	10, 12	wceq 1540	. . . . . . 7 wff (𝑓‘1) = 𝑦
14	8, 13	wa 395	. . . . . 6 wff ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
15		cii 24775	. . . . . . 7 class II
16		vj	. . . . . . . 8 setvar 𝑗
17	16	cv 1539	. . . . . . 7 class 𝑗
18		ccn 23118	. . . . . . 7 class Cn
19	15, 17, 18	co 7390	. . . . . 6 class (II Cn 𝑗)
20	14, 3, 19	wrex 3054	. . . . 5 wff ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
21	17	cuni 4874	. . . . 5 class ∪ 𝑗
22	20, 11, 21	wral 3045	. . . 4 wff ∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
23	22, 6, 21	wral 3045	. . 3 wff ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
24		ctop 22787	. . 3 class Top
25	23, 16, 24	crab 3408	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
26	1, 25	wceq 1540	1 wff PConn = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}

This definition is referenced by:  ispconn  35217