Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pconn Structured version   Visualization version   GIF version

Definition df-pconn 31431
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-pconn PConn = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
Distinct variable group:   𝑓,𝑗,𝑥,𝑦

Detailed syntax breakdown of Definition df-pconn
StepHypRef Expression
1 cpconn 31429 . 2 class PConn
2 cc0 10049 . . . . . . . . 9 class 0
3 vf . . . . . . . . . 10 setvar 𝑓
43cv 1595 . . . . . . . . 9 class 𝑓
52, 4cfv 6001 . . . . . . . 8 class (𝑓‘0)
6 vx . . . . . . . . 9 setvar 𝑥
76cv 1595 . . . . . . . 8 class 𝑥
85, 7wceq 1596 . . . . . . 7 wff (𝑓‘0) = 𝑥
9 c1 10050 . . . . . . . . 9 class 1
109, 4cfv 6001 . . . . . . . 8 class (𝑓‘1)
11 vy . . . . . . . . 9 setvar 𝑦
1211cv 1595 . . . . . . . 8 class 𝑦
1310, 12wceq 1596 . . . . . . 7 wff (𝑓‘1) = 𝑦
148, 13wa 383 . . . . . 6 wff ((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
15 cii 22800 . . . . . . 7 class II
16 vj . . . . . . . 8 setvar 𝑗
1716cv 1595 . . . . . . 7 class 𝑗
18 ccn 21151 . . . . . . 7 class Cn
1915, 17, 18co 6765 . . . . . 6 class (II Cn 𝑗)
2014, 3, 19wrex 3015 . . . . 5 wff 𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
2117cuni 4544 . . . . 5 class 𝑗
2220, 11, 21wral 3014 . . . 4 wff 𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
2322, 6, 21wral 3014 . . 3 wff 𝑥 𝑗𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)
24 ctop 20821 . . 3 class Top
2523, 16, 24crab 3018 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
261, 25wceq 1596 1 wff PConn = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  ispconn  31433
  Copyright terms: Public domain W3C validator