Definition df-pcon 30457

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

Assertion

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

Distinct variable group:   𝑓,𝑗,𝑥,𝑦

Detailed syntax breakdown of Definition df-pcon

Step	Hyp	Ref	Expression
1		cpcon 30455	. 2 class PCon
2		cc0 9815	. . . . . . . . 9 class 0
3		vf	. . . . . . . . . 10 setvar 𝑓
4	3	cv 1474	. . . . . . . . 9 class 𝑓
5	2, 4	cfv 5804	. . . . . . . 8 class (𝑓‘0)
6		vx	. . . . . . . . 9 setvar 𝑥
7	6	cv 1474	. . . . . . . 8 class 𝑥
8	5, 7	wceq 1475	. . . . . . 7 wff (𝑓‘0) = 𝑥
9		c1 9816	. . . . . . . . 9 class 1
10	9, 4	cfv 5804	. . . . . . . 8 class (𝑓‘1)
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1474	. . . . . . . 8 class 𝑦
13	10, 12	wceq 1475	. . . . . . 7 wff (𝑓‘1) = 𝑦
14	8, 13	wa 383	. . . . . 6 wff ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
15		cii 22486	. . . . . . 7 class II
16		vj	. . . . . . . 8 setvar 𝑗
17	16	cv 1474	. . . . . . 7 class 𝑗
18		ccn 20838	. . . . . . 7 class Cn
19	15, 17, 18	co 6549	. . . . . 6 class (II Cn 𝑗)
20	14, 3, 19	wrex 2897	. . . . 5 wff ∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
21	17	cuni 4372	. . . . 5 class ∪ 𝑗
22	20, 11, 21	wral 2896	. . . 4 wff ∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
23	22, 6, 21	wral 2896	. . 3 wff ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
24		ctop 20517	. . 3 class Top
25	23, 16, 24	crab 2900	. 2 class {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
26	1, 25	wceq 1475	1 wff PCon = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∀𝑦 ∈ ∪ 𝑗∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}

This definition is referenced by:  ispcon  30459