Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  el2spthonot Structured version   Unicode version

Theorem el2spthonot 25533
 Description: A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
Assertion
Ref Expression
el2spthonot 2SPathOnOt SPaths
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,

Proof of Theorem el2spthonot
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 2spthonot 25529 . . . 4 2SPathOnOt SPathOn
21eleq2d 2485 . . 3 2SPathOnOt SPathOn
3 fveq2 5818 . . . . . . . . 9
43fveq2d 5822 . . . . . . . 8
54eqeq1d 2424 . . . . . . 7
63fveq2d 5822 . . . . . . . 8
76eqeq1d 2424 . . . . . . 7
8 fveq2 5818 . . . . . . . 8
98eqeq1d 2424 . . . . . . 7
105, 7, 93anbi123d 1335 . . . . . 6
11103anbi3d 1341 . . . . 5 SPathOn SPathOn
12112exbidv 1764 . . . 4 SPathOn SPathOn
1312elrab 3164 . . 3 SPathOn SPathOn
142, 13syl6bb 264 . 2 2SPathOnOt SPathOn
15 vex 3019 . . . . . . . . . 10
16 vex 3019 . . . . . . . . . 10
1715, 16pm3.2i 456 . . . . . . . . 9
18 isspthon 25248 . . . . . . . . 9 SPathOn WalkOn SPaths
1917, 18mp3an2 1348 . . . . . . . 8 SPathOn WalkOn SPaths
20193anbi1d 1339 . . . . . . 7 SPathOn WalkOn SPaths
2120anbi2d 708 . . . . . 6 SPathOn WalkOn SPaths
22 simpl 458 . . . . . . . . . . . . . . . 16
2322ad2antll 733 . . . . . . . . . . . . . . 15 WalkOn SPaths
24 spthispth 25238 . . . . . . . . . . . . . . . . . . 19 SPaths Paths
25 pthistrl 25237 . . . . . . . . . . . . . . . . . . 19 Paths Trails
26 trliswlk 25204 . . . . . . . . . . . . . . . . . . 19 Trails Walks
27 el2wlkonotlem 25525 . . . . . . . . . . . . . . . . . . . 20 Walks
2827ex 435 . . . . . . . . . . . . . . . . . . 19 Walks
2924, 25, 26, 284syl 19 . . . . . . . . . . . . . . . . . 18 SPaths
3029adantl 467 . . . . . . . . . . . . . . . . 17 WalkOn SPaths
3130imp 430 . . . . . . . . . . . . . . . 16 WalkOn SPaths
3231adantr 466 . . . . . . . . . . . . . . 15 WalkOn SPaths
33 simpr 462 . . . . . . . . . . . . . . . 16
3433ad2antll 733 . . . . . . . . . . . . . . 15 WalkOn SPaths
35 el2xptp0 6788 . . . . . . . . . . . . . . 15
3623, 32, 34, 35syl3anc 1264 . . . . . . . . . . . . . 14 WalkOn SPaths
37 oteq2 4133 . . . . . . . . . . . . . . . . . . . 20
3837eqcoms 2430 . . . . . . . . . . . . . . . . . . 19
3938eqeq2d 2432 . . . . . . . . . . . . . . . . . 18
4039biimpd 210 . . . . . . . . . . . . . . . . 17
4140adantl 467 . . . . . . . . . . . . . . . 16 WalkOn SPaths
42 simpllr 767 . . . . . . . . . . . . . . . . . 18 WalkOn SPaths SPaths
4342adantr 466 . . . . . . . . . . . . . . . . 17 WalkOn SPaths SPaths
44 simpllr 767 . . . . . . . . . . . . . . . . 17 WalkOn SPaths
45 iswlkon 25197 . . . . . . . . . . . . . . . . . . . . . 22 WalkOn Walks
4617, 45mp3an2 1348 . . . . . . . . . . . . . . . . . . . . 21 WalkOn Walks
47 fveq2 5818 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4847eqeq1d 2424 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4948anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . 25
50 eqcom 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5150biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5251adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5352adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
54 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
55 eqcom 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5655biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5756adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
5857adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5953, 54, 583jca 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6059ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
6249, 61sylbid 218 . . . . . . . . . . . . . . . . . . . . . . . 24
6362com12 32 . . . . . . . . . . . . . . . . . . . . . . 23
64633adant1 1023 . . . . . . . . . . . . . . . . . . . . . 22 Walks
6564a1i 11 . . . . . . . . . . . . . . . . . . . . 21 Walks
6646, 65sylbid 218 . . . . . . . . . . . . . . . . . . . 20 WalkOn
6766com3l 84 . . . . . . . . . . . . . . . . . . 19 WalkOn
6867adantr 466 . . . . . . . . . . . . . . . . . 18 WalkOn SPaths
6968imp41 596 . . . . . . . . . . . . . . . . 17 WalkOn SPaths
7043, 44, 693jca 1185 . . . . . . . . . . . . . . . 16 WalkOn SPaths SPaths
7141, 70jctird 546 . . . . . . . . . . . . . . 15 WalkOn SPaths SPaths
7232, 71rspcimedv 3120 . . . . . . . . . . . . . 14 WalkOn SPaths SPaths
7336, 72sylbid 218 . . . . . . . . . . . . 13 WalkOn SPaths SPaths
7473exp4b 610 . . . . . . . . . . . 12 WalkOn SPaths SPaths
7574com24 90 . . . . . . . . . . 11 WalkOn SPaths SPaths
7675ex 435 . . . . . . . . . 10 WalkOn SPaths SPaths
77763imp 1199 . . . . . . . . 9 WalkOn SPaths SPaths
7877impcom 431 . . . . . . . 8 WalkOn SPaths SPaths
7978com12 32 . . . . . . 7 WalkOn SPaths SPaths
8022adantr 466 . . . . . . . . . . . . . . . . . 18
81 simpr 462 . . . . . . . . . . . . . . . . . 18
8233adantr 466 . . . . . . . . . . . . . . . . . 18
8380, 81, 823jca 1185 . . . . . . . . . . . . . . . . 17
84 otel3xp 4825 . . . . . . . . . . . . . . . . 17
8583, 84sylan2 476 . . . . . . . . . . . . . . . 16
8685ex 435 . . . . . . . . . . . . . . 15
8786adantr 466 . . . . . . . . . . . . . 14 SPaths
8887com12 32 . . . . . . . . . . . . 13 SPaths
8988ex 435 . . . . . . . . . . . 12 SPaths
9089adantl 467 . . . . . . . . . . 11 SPaths
9190imp31 433 . . . . . . . . . 10 SPaths
9224, 25, 263syl 18 . . . . . . . . . . . . . . 15 SPaths Walks
93923ad2ant1 1026 . . . . . . . . . . . . . 14 SPaths Walks
9493ad2antll 733 . . . . . . . . . . . . 13 SPaths Walks
95 eqcom 2429 . . . . . . . . . . . . . . . . 17
9695biimpi 197 . . . . . . . . . . . . . . . 16
97963ad2ant1 1026 . . . . . . . . . . . . . . 15
98973ad2ant3 1028 . . . . . . . . . . . . . 14 SPaths
9998ad2antll 733 . . . . . . . . . . . . 13 SPaths
100 eqcom 2429 . . . . . . . . . . . . . . . . . . 19
101100biimpi 197 . . . . . . . . . . . . . . . . . 18
1021013ad2ant3 1028 . . . . . . . . . . . . . . . . 17
103102, 48syl5ibr 224 . . . . . . . . . . . . . . . 16
104103a1i 11 . . . . . . . . . . . . . . 15 SPaths
1051043imp 1199 . . . . . . . . . . . . . 14 SPaths
106105ad2antll 733 . . . . . . . . . . . . 13 SPaths
10746adantr 466 . . . . . . . . . . . . . 14 WalkOn Walks
108107adantr 466 . . . . . . . . . . . . 13 SPaths WalkOn Walks
10994, 99, 106, 108mpbir3and 1188 . . . . . . . . . . . 12 SPaths WalkOn
110 id 22 . . . . . . . . . . . . . 14 SPaths SPaths
1111103ad2ant1 1026 . . . . . . . . . . . . 13 SPaths SPaths
112111ad2antll 733 . . . . . . . . . . . 12 SPaths SPaths
113109, 112jca 534 . . . . . . . . . . 11 SPaths WalkOn SPaths
114 id 22 . . . . . . . . . . . . 13
1151143ad2ant2 1027 . . . . . . . . . . . 12 SPaths
116115ad2antll 733 . . . . . . . . . . 11 SPaths
11722adantl 467 . . . . . . . . . . . . . . . . . . . 20
118117adantr 466 . . . . . . . . . . . . . . . . . . 19
119 simpr 462 . . . . . . . . . . . . . . . . . . 19
12033adantl 467 . . . . . . . . . . . . . . . . . . . 20
121120adantr 466 . . . . . . . . . . . . . . . . . . 19
122118, 119, 1213jca 1185 . . . . . . . . . . . . . . . . . 18
123 oteqimp 6763 . . . . . . . . . . . . . . . . . . 19
124123imp 430 . . . . . . . . . . . . . . . . . 18
125122, 124sylan2 476 . . . . . . . . . . . . . . . . 17
126125ex 435 . . . . . . . . . . . . . . . 16
127 eqeq2 2433 . . . . . . . . . . . . . . . . . . 19
128127eqcoms 2430 . . . . . . . . . . . . . . . . . 18
1291283anbi2d 1340 . . . . . . . . . . . . . . . . 17
130129imbi2d 317 . . . . . . . . . . . . . . . 16
131126, 130syl5ibr 224 . . . . . . . . . . . . . . 15
1321313ad2ant2 1027 . . . . . . . . . . . . . 14
1331323ad2ant3 1028 . . . . . . . . . . . . 13 SPaths
134133impcom 431 . . . . . . . . . . . 12 SPaths
135134impcom 431 . . . . . . . . . . 11 SPaths
136113, 116, 1353jca 1185 . . . . . . . . . 10 SPaths WalkOn SPaths
13791, 136jca 534 . . . . . . . . 9 SPaths WalkOn SPaths
138137ex 435 . . . . . . . 8 SPaths WalkOn SPaths
139138rexlimdva 2850 . . . . . . 7 SPaths WalkOn SPaths
14079, 139impbid 193 . . . . . 6 WalkOn SPaths SPaths
14121, 140bitrd 256 . . . . 5 SPathOn SPaths
1421412exbidv 1764 . . . 4 SPathOn SPaths
143 19.42vv 1829 . . . 4 SPathOn SPathOn
144 rexcom4 3037 . . . . 5 SPaths SPaths
145 rexcom4 3037 . . . . . 6 SPaths SPaths
146145exbii 1712 . . . . 5 SPaths SPaths
147144, 146bitr2i 253 . . . 4 SPaths SPaths
148142, 143, 1473bitr3g 290 . . 3 SPathOn SPaths
149 19.42vv 1829 . . . 4 SPaths SPaths
150149rexbii 2860 . . 3 SPaths SPaths
151148, 150syl6bb 264 . 2 SPathOn SPaths
15214, 151bitrd 256 1 2SPathOnOt SPaths
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437  wex 1657   wcel 1872  wrex 2709  crab 2712  cvv 3016  cotp 3942   class class class wbr 4359   cxp 4787  cfv 5537  (class class class)co 6242  c1st 6742  c2nd 6743  cc0 9483  c1 9484  c2 10603  chash 12458   Walks cwalk 25161   Trails ctrail 25162   Paths cpath 25163   SPaths cspath 25164   WalkOn cwlkon 25165   SPathOn cspthon 25168   2SPathOnOt c2pthonot 25520 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-ot 3943  df-uni 4156  df-int 4192  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-om 6644  df-1st 6744  df-2nd 6745  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-card 8318  df-cda 8542  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-nn 10554  df-2 10612  df-n0 10814  df-z 10882  df-uz 11104  df-fz 11729  df-fzo 11860  df-hash 12459  df-word 12605  df-wlk 25171  df-trail 25172  df-pth 25173  df-spth 25174  df-wlkon 25177  df-spthon 25180  df-2spthonot 25523 This theorem is referenced by:  el2spthonot0  25534  el2pthsot  25544  2spontn0vne  25550  2spotiundisj  25725
 Copyright terms: Public domain W3C validator