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

Theorem frg2woteq 25786
 Description: There is a (simple) path of length 2 from one vertex to another vertex in a friendship graph if and only if there is a (simple) path of length 2 from the other vertex back to the first vertex. (Contributed by Alexander van der Vekens, 14-Feb-2018.)
Assertion
Ref Expression
frg2woteq FriendGrph 2WalksOnOt 2WalksOnOt

Proof of Theorem frg2woteq
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2wlkonot3v 25601 . . . 4 2WalksOnOt
21adantr 466 . . 3 2WalksOnOt 2WalksOnOt
3 el2wlkonot 25595 . . . . . 6 2WalksOnOt Walks
4 pm3.22 450 . . . . . . . 8
54anim2i 571 . . . . . . 7
6 el2wlkonot 25595 . . . . . . 7 2WalksOnOt Walks
75, 6syl 17 . . . . . 6 2WalksOnOt Walks
83, 7anbi12d 715 . . . . 5 2WalksOnOt 2WalksOnOt Walks Walks
983adant3 1025 . . . 4 2WalksOnOt 2WalksOnOt Walks Walks
1053adant3 1025 . . . . . . . . . . . . 13
1110adantr 466 . . . . . . . . . . . 12
1211ad2antrr 730 . . . . . . . . . . 11
13 el2wlkonotot 25599 . . . . . . . . . . . 12 2WalksOnOt Walks
1413bicomd 204 . . . . . . . . . . 11 Walks 2WalksOnOt
1512, 14syl 17 . . . . . . . . . 10 Walks 2WalksOnOt
16 3simpa 1002 . . . . . . . . . . . . . . . 16
1716ad2antrr 730 . . . . . . . . . . . . . . 15
1817ad2antrr 730 . . . . . . . . . . . . . 14
19 el2wlkonotot 25599 . . . . . . . . . . . . . . 15 2WalksOnOt Walks
2019bicomd 204 . . . . . . . . . . . . . 14 Walks 2WalksOnOt
2118, 20syl 17 . . . . . . . . . . . . 13 Walks 2WalksOnOt
22 frg2woteqm 25785 . . . . . . . . . . . . . . . . . . . . 21 FriendGrph 2WalksOnOt 2WalksOnOt
23 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2423fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2524adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25
2625adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24
27 vex 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
28 ot1stg 6821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2927, 28mp3an2 1348 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3029ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25
3130adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24
32 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3332ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3433adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25
35 ot3rdg 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3635adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3736ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3837adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25
3934, 38eqtr2d 2464 . . . . . . . . . . . . . . . . . . . . . . . 24
4026, 31, 393eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . 23
41 eqidd 2423 . . . . . . . . . . . . . . . . . . . . . . 23
42 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4342fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4443ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25
4544adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24
46 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
47 vex 3083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4847a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
49 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5046, 48, 493jca 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5150ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5251adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25
53 ot1stg 6821 . . . . . . . . . . . . . . . . . . . . . . . . 25
5452, 53syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
55 ot3rdg 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5655adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5756ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5857adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . 25
59 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6059adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6160eqcomd 2430 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6261fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . . . . 25
6358, 62eqtr3d 2465 . . . . . . . . . . . . . . . . . . . . . . . 24
6445, 54, 633eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . 23
6540, 41, 643jca 1185 . . . . . . . . . . . . . . . . . . . . . 22
6665ex 435 . . . . . . . . . . . . . . . . . . . . 21
6722, 66syl6 34 . . . . . . . . . . . . . . . . . . . 20 FriendGrph 2WalksOnOt 2WalksOnOt
6867expd 437 . . . . . . . . . . . . . . . . . . 19 FriendGrph 2WalksOnOt 2WalksOnOt
6968com14 91 . . . . . . . . . . . . . . . . . 18 2WalksOnOt 2WalksOnOt FriendGrph
7069ex 435 . . . . . . . . . . . . . . . . 17 2WalksOnOt 2WalksOnOt FriendGrph
7170ex 435 . . . . . . . . . . . . . . . 16 2WalksOnOt 2WalksOnOt FriendGrph
72713ad2ant2 1027 . . . . . . . . . . . . . . 15 2WalksOnOt 2WalksOnOt FriendGrph
7372ad2antrr 730 . . . . . . . . . . . . . 14 2WalksOnOt 2WalksOnOt FriendGrph
7473imp31 433 . . . . . . . . . . . . 13 2WalksOnOt 2WalksOnOt FriendGrph
7521, 74sylbid 218 . . . . . . . . . . . 12 Walks 2WalksOnOt FriendGrph
7675expimpd 606 . . . . . . . . . . 11 Walks 2WalksOnOt FriendGrph
7776com23 81 . . . . . . . . . 10 2WalksOnOt Walks FriendGrph
7815, 77sylbid 218 . . . . . . . . 9 Walks Walks FriendGrph
7978expimpd 606 . . . . . . . 8 Walks Walks FriendGrph
8079rexlimdva 2914 . . . . . . 7 Walks Walks FriendGrph
8180com23 81 . . . . . 6 Walks Walks FriendGrph
8281rexlimdva 2914 . . . . 5 Walks Walks FriendGrph
8382impd 432 . . . 4 Walks Walks FriendGrph
849, 83sylbid 218 . . 3 2WalksOnOt 2WalksOnOt FriendGrph
852, 84mpcom 37 . 2 2WalksOnOt 2WalksOnOt FriendGrph
8685com12 32 1 FriendGrph 2WalksOnOt 2WalksOnOt
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437  wex 1657   wcel 1872   wne 2614  wrex 2772  cvv 3080  cotp 4006   class class class wbr 4423   cxp 4851  cfv 5601  (class class class)co 6305  c1st 6805  c2nd 6806  cc0 9546  c1 9547  c2 10666  chash 12521   Walks cwalk 25224   2WalksOnOt c2wlkonot 25581   FriendGrph cfrgra 25714 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 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623 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 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-ot 4007  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-oadd 7197  df-er 7374  df-map 7485  df-pm 7486  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584  df-card 8381  df-cda 8605  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-nn 10617  df-2 10675  df-n0 10877  df-z 10945  df-uz 11167  df-fz 11792  df-fzo 11923  df-hash 12522  df-word 12668  df-usgra 25058  df-wlk 25234  df-wlkon 25240  df-2wlkonot 25584  df-frgra 25715 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator