Definition df-pconn 32468

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 32466	. 2 class PConn
2		cc0 10537	. . . . . . . . 9 class 0
3		vf	. . . . . . . . . 10 setvar 𝑓
4	3	cv 1536	. . . . . . . . 9 class 𝑓
5	2, 4	cfv 6355	. . . . . . . 8 class (𝑓‘0)
6		vx	. . . . . . . . 9 setvar 𝑥
7	6	cv 1536	. . . . . . . 8 class 𝑥
8	5, 7	wceq 1537	. . . . . . 7 wff (𝑓‘0) = 𝑥
9		c1 10538	. . . . . . . . 9 class 1
10	9, 4	cfv 6355	. . . . . . . 8 class (𝑓‘1)
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1536	. . . . . . . 8 class 𝑦
13	10, 12	wceq 1537	. . . . . . 7 wff (𝑓‘1) = 𝑦
14	8, 13	wa 398	. . . . . 6 wff ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
15		cii 23483	. . . . . . 7 class II
16		vj	. . . . . . . 8 setvar 𝑗
17	16	cv 1536	. . . . . . 7 class 𝑗
18		ccn 21832	. . . . . . 7 class Cn
19	15, 17, 18	co 7156	. . . . . 6 class (II Cn 𝑗)
20	14, 3, 19	wrex 3139	. . . . 5 wff ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
21	17	cuni 4838	. . . . 5 class ∪ 𝑗
22	20, 11, 21	wral 3138	. . . 4 wff ∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
23	22, 6, 21	wral 3138	. . 3 wff ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
24		ctop 21501	. . 3 class Top
25	23, 16, 24	crab 3142	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
26	1, 25	wceq 1537	1 wff PConn = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}

This definition is referenced by:  ispconn  32470