Definition 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 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpconn	⊢ PConn
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vx	⊢ 𝑥
4	1	cv	⊢ 𝑗
5	4	cuni	⊢ ∪ 𝑗
6		vy	⊢ 𝑦
7		vf	⊢ 𝑓
8		cii	⊢ II
9		ccn	⊢ Cn
10	8 4 9	co	⊢ ( II Cn 𝑗 )
11	7	cv	⊢ 𝑓
12		cc0	⊢ 0
13	12 11	cfv	⊢ ( 𝑓 ‘ 0 )
14	3	cv	⊢ 𝑥
15	13 14	wceq	⊢ ( 𝑓 ‘ 0 ) = 𝑥
16		c1	⊢ 1
17	16 11	cfv	⊢ ( 𝑓 ‘ 1 )
18	6	cv	⊢ 𝑦
19	17 18	wceq	⊢ ( 𝑓 ‘ 1 ) = 𝑦
20	15 19	wa	⊢ ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
21	20 7 10	wrex	⊢ ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
22	21 6 5	wral	⊢ ∀ 𝑦 ∈ ∪ 𝑗 ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
23	22 3 5	wral	⊢ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 )
24	23 1 2	crab	⊢ { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) }
25	0 24	wceq	⊢ PConn = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∀ 𝑦 ∈ ∪ 𝑗 ∃ 𝑓 ∈ ( II Cn 𝑗 ) ( ( 𝑓 ‘ 0 ) = 𝑥 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) }