Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sconpht Structured version   Unicode version

Theorem sconpht 28499
 Description: A closed path in a simply connected space is contractible to a point. (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
sconpht SCon

Proof of Theorem sconpht
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 isscon 28496 . . . 4 SCon PCon
21simprbi 464 . . 3 SCon
3 fveq1 5871 . . . . . 6
4 fveq1 5871 . . . . . 6
53, 4eqeq12d 2489 . . . . 5
6 id 22 . . . . . 6
73sneqd 4045 . . . . . . 7
87xpeq2d 5029 . . . . . 6
96, 8breq12d 4466 . . . . 5
105, 9imbi12d 320 . . . 4
1110rspccv 3216 . . 3
122, 11syl 16 . 2 SCon
13123imp 1190 1 SCon
 Colors of variables: wff setvar class Syntax hints:   wi 4   w3a 973   wceq 1379   wcel 1767  wral 2817  csn 4033   class class class wbr 4453   cxp 5003  cfv 5594  (class class class)co 6295  cc0 9504  c1 9505  cicc 11544   ccn 19593  cii 21247   cphtpc 21337  PConcpcon 28489  SConcscon 28490 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-xp 5011  df-iota 5557  df-fv 5602  df-ov 6298  df-scon 28492 This theorem is referenced by:  sconpht2  28508  sconpi1  28509  txscon  28511
 Copyright terms: Public domain W3C validator