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

Theorem ispconn 33904
Description: The property of being a path-connected topological space. (Contributed by Mario Carneiro, 11-Feb-2015.)
Hypothesis
Ref Expression
ispconn.1 𝑋 = 𝐽
Assertion
Ref Expression
ispconn (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥𝑋𝑦𝑋𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
Distinct variable groups:   𝑥,𝑓,𝑦,𝐽   𝑥,𝑋,𝑦
Allowed substitution hint:   𝑋(𝑓)

Proof of Theorem ispconn
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 unieq 4881 . . . 4 (𝑗 = 𝐽 𝑗 = 𝐽)
2 ispconn.1 . . . 4 𝑋 = 𝐽
31, 2eqtr4di 2789 . . 3 (𝑗 = 𝐽 𝑗 = 𝑋)
4 oveq2 7370 . . . . 5 (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽))
54rexeqdv 3312 . . . 4 (𝑗 = 𝐽 → (∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
63, 5raleqbidv 3317 . . 3 (𝑗 = 𝐽 → (∀𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∀𝑦𝑋𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
73, 6raleqbidv 3317 . 2 (𝑗 = 𝐽 → (∀𝑥 𝑗𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∀𝑥𝑋𝑦𝑋𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
8 df-pconn 33902 . 2 PConn = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
97, 8elrab2 3651 1 (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥𝑋𝑦𝑋𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3060  wrex 3069   cuni 4870  cfv 6501  (class class class)co 7362  0cc0 11060  1c1 11061  Topctop 22279   Cn ccn 22612  IIcii 24275  PConncpconn 33900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-pconn 33902
This theorem is referenced by:  pconncn  33905  pconntop  33906  cnpconn  33911  txpconn  33913  ptpconn  33914  indispconn  33915  connpconn  33916  cvxpconn  33923
  Copyright terms: Public domain W3C validator