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 32530
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 4835 . . . 4 (𝑗 = 𝐽 𝑗 = 𝐽)
2 ispconn.1 . . . 4 𝑋 = 𝐽
31, 2syl6eqr 2877 . . 3 (𝑗 = 𝐽 𝑗 = 𝑋)
4 oveq2 7157 . . . . 5 (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽))
54rexeqdv 3403 . . . 4 (𝑗 = 𝐽 → (∃𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∃𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
63, 5raleqbidv 3392 . . 3 (𝑗 = 𝐽 → (∀𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∀𝑦𝑋𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
73, 6raleqbidv 3392 . 2 (𝑗 = 𝐽 → (∀𝑥 𝑗𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦) ↔ ∀𝑥𝑋𝑦𝑋𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
8 df-pconn 32528 . 2 PConn = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 𝑗𝑓 ∈ (II Cn 𝑗)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)}
97, 8elrab2 3669 1 (𝐽 ∈ PConn ↔ (𝐽 ∈ Top ∧ ∀𝑥𝑋𝑦𝑋𝑓 ∈ (II Cn 𝐽)((𝑓‘0) = 𝑥 ∧ (𝑓‘1) = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1538  wcel 2115  wral 3133  wrex 3134   cuni 4824  cfv 6343  (class class class)co 7149  0cc0 10535  1c1 10536  Topctop 21504   Cn ccn 21835  IIcii 23486  PConncpconn 32526
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-iota 6302  df-fv 6351  df-ov 7152  df-pconn 32528
This theorem is referenced by:  pconncn  32531  pconntop  32532  cnpconn  32537  txpconn  32539  ptpconn  32540  indispconn  32541  connpconn  32542  cvxpconn  32549
  Copyright terms: Public domain W3C validator