Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  spthdifv Unicode version

Theorem spthdifv 28667
Description: The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.)
Assertion
Ref Expression
spthdifv

Proof of Theorem spthdifv
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 spthispth 21609 . . 3
2 pthistrl 21608 . . 3
3 trliswlk 21575 . . . 4
4 wlkbprop 21570 . . . 4
5 3simpc 957 . . . 4
63, 4, 53syl 19 . . 3
71, 2, 63syl 19 . 2
8 isspth 21605 . . 3
9 istrl2 21574 . . . . 5
109anbi1d 687 . . . 4
11 df-f1 5510 . . . . . 6
1211biimpri 199 . . . . 5
13123ad2antl2 1121 . . . 4
1410, 13syl6bi 221 . . 3
158, 14sylbid 208 . 2
167, 15mpcom 35 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  /\w3a 937  =wceq 1654  e.wcel 1728  A.wral 2716   cvv 2969  {cpr 3846   class class class wbr 4247  `'ccnv 4922  domcdm 4923  Funwfun 5499  -->wf 5501  -1-1->wf1 5502  `cfv 5505  (class class class)co 6133  0cc0 9045  1c1 9046   caddc 9048   cn0 10276   cfz 11098   cfzo 11190   chash 11673   cwalk 21542   ctrail 21543   cpath 21544   cspath 21545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428  ax-rep 4358  ax-sep 4368  ax-nul 4376  ax-pow 4420  ax-pr 4446  ax-un 4746  ax-cnex 9101  ax-resscn 9102  ax-1cn 9103  ax-icn 9104  ax-addcl 9105  ax-addrcl 9106  ax-mulcl 9107  ax-mulrcl 9108  ax-mulcom 9109  ax-addass 9110  ax-mulass 9111  ax-distr 9112  ax-i2m1 9113  ax-1ne0 9114  ax-1rid 9115  ax-rnegex 9116  ax-rrecex 9117  ax-cnre 9118  ax-pre-lttri 9119  ax-pre-lttrn 9120  ax-pre-ltadd 9121  ax-pre-mulgt0 9122
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2296  df-mo 2297  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-ne 2612  df-nel 2613  df-ral 2721  df-rex 2722  df-reu 2723  df-rab 2725  df-v 2971  df-sbc 3175  df-csb 3275  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3621  df-if 3770  df-pw 3832  df-sn 3851  df-pr 3852  df-tp 3853  df-op 3854  df-uni 4048  df-int 4084  df-iun 4128  df-br 4248  df-opab 4306  df-mpt 4307  df-tr 4341  df-eprel 4539  df-id 4543  df-po 4548  df-so 4549  df-fr 4586  df-we 4588  df-ord 4629  df-on 4630  df-lim 4631  df-suc 4632  df-om 4891  df-xp 4929  df-rel 4930  df-cnv 4931  df-co 4932  df-dm 4933  df-rn 4934  df-res 4935  df-ima 4936  df-iota 5468  df-fun 5507  df-fn 5508  df-f 5509  df-f1 5510  df-fo 5511  df-f1o 5512  df-fv 5513  df-ov 6136  df-oprab 6137  df-mpt2 6138  df-1st 6403  df-2nd 6404  df-riota 6603  df-recs 6686  df-rdg 6721  df-1o 6777  df-oadd 6781  df-er 6958  df-map 7073  df-pm 7074  df-en 7163  df-dom 7164  df-sdom 7165  df-fin 7166  df-card 7881  df-pnf 9177  df-mnf 9178  df-xr 9179  df-ltxr 9180  df-le 9181  df-sub 9348  df-neg 9349  df-nn 10056  df-n0 10277  df-z 10338  df-uz 10544  df-fz 11099  df-fzo 11191  df-hash 11674  df-word 11778  df-wlk 21552  df-trail 21553  df-pth 21554  df-spth 21555
  Copyright terms: Public domain W3C validator