Metamath Proof Explorer

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 = j ∈ Top | ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∃ f ∈ II Cn j f ⁡ 0 = x ∧ 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 ∧ f ⁡ 1 = y
21 20 7 10 wrex wff ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y
22 21 6 5 wral wff ∀ y ∈ ⋃ j ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y
23 22 3 5 wral wff ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y
24 23 1 2 crab class j ∈ Top | ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y
25 0 24 wceq wff PConn = j ∈ Top | ∀ x ∈ ⋃ j ∀ y ∈ ⋃ j ∃ f ∈ II Cn j f ⁡ 0 = x ∧ f ⁡ 1 = y