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

Theorem 2pthfrgra 28055
 Description: Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 6-Dec-2017.)
Assertion
Ref Expression
2pthfrgra FriendGrph PathOn
Distinct variable groups:   ,,,,   ,,,,

Proof of Theorem 2pthfrgra
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 2pthfrgrarn2 28054 . 2 FriendGrph
2 frisusgra 28036 . . . . . . . . . 10 FriendGrph USGrph
3 usgrav 21310 . . . . . . . . . 10 USGrph
42, 3syl 16 . . . . . . . . 9 FriendGrph
54ad2antrr 707 . . . . . . . 8 FriendGrph
65ad2antrr 707 . . . . . . 7 FriendGrph
7 simpr 448 . . . . . . . . . 10 FriendGrph
87ad2antrr 707 . . . . . . . . 9 FriendGrph
9 simpr 448 . . . . . . . . 9 FriendGrph
10 eldifsn 3884 . . . . . . . . . . 11
11 simpl 444 . . . . . . . . . . 11
1210, 11sylbi 188 . . . . . . . . . 10
1312ad2antlr 708 . . . . . . . . 9 FriendGrph
148, 9, 133jca 1134 . . . . . . . 8 FriendGrph
1514adantr 452 . . . . . . 7 FriendGrph
16 simpll 731 . . . . . . . . . . . . . . 15
17 necom 2645 . . . . . . . . . . . . . . . . 17
1817biimpi 187 . . . . . . . . . . . . . . . 16
1918adantl 453 . . . . . . . . . . . . . . 15
20 simplr 732 . . . . . . . . . . . . . . 15
2116, 19, 203jca 1134 . . . . . . . . . . . . . 14
2221ex 424 . . . . . . . . . . . . 13
2322adantl 453 . . . . . . . . . . . 12
2423com12 29 . . . . . . . . . . 11
2524adantl 453 . . . . . . . . . 10
2610, 25sylbi 188 . . . . . . . . 9
2726ad2antlr 708 . . . . . . . 8 FriendGrph
2827imp 419 . . . . . . 7 FriendGrph
29 usgraf1o 21321 . . . . . . . . . 10 USGrph
30 fveq2 5682 . . . . . . . . . . . . . . . . 17
31 simpl 444 . . . . . . . . . . . . . . . . . . . 20
32 simpll 731 . . . . . . . . . . . . . . . . . . . 20
33 f1ocnvfv2 5968 . . . . . . . . . . . . . . . . . . . 20
3431, 32, 33syl2an 464 . . . . . . . . . . . . . . . . . . 19
35 simplr 732 . . . . . . . . . . . . . . . . . . . 20
36 f1ocnvfv2 5968 . . . . . . . . . . . . . . . . . . . 20
3731, 35, 36syl2an 464 . . . . . . . . . . . . . . . . . . 19
3834, 37eqeq12d 2415 . . . . . . . . . . . . . . . . . 18
39 prcom 3839 . . . . . . . . . . . . . . . . . . . . 21
4039eqeq2i 2411 . . . . . . . . . . . . . . . . . . . 20
41 vex 2916 . . . . . . . . . . . . . . . . . . . . 21
42 vex 2916 . . . . . . . . . . . . . . . . . . . . 21
4341, 42preqr1 3928 . . . . . . . . . . . . . . . . . . . 20
4440, 43sylbi 188 . . . . . . . . . . . . . . . . . . 19
45 df-ne 2566 . . . . . . . . . . . . . . . . . . . . . . . . 25
4617, 45bitri 241 . . . . . . . . . . . . . . . . . . . . . . . 24
47 pm2.21 102 . . . . . . . . . . . . . . . . . . . . . . . 24
4846, 47sylbi 188 . . . . . . . . . . . . . . . . . . . . . . 23
4948adantl 453 . . . . . . . . . . . . . . . . . . . . . 22
5010, 49sylbi 188 . . . . . . . . . . . . . . . . . . . . 21
5150adantl 453 . . . . . . . . . . . . . . . . . . . 20
5251ad2antlr 708 . . . . . . . . . . . . . . . . . . 19
5344, 52syl5 30 . . . . . . . . . . . . . . . . . 18
5438, 53sylbid 207 . . . . . . . . . . . . . . . . 17
5530, 54syl5com 28 . . . . . . . . . . . . . . . 16
56 df-ne 2566 . . . . . . . . . . . . . . . . . 18
5756biimpri 198 . . . . . . . . . . . . . . . . 17
5857a1d 23 . . . . . . . . . . . . . . . 16
5955, 58pm2.61i 158 . . . . . . . . . . . . . . 15
6059, 34, 373jca 1134 . . . . . . . . . . . . . 14
6160ex 424 . . . . . . . . . . . . 13
6261expcom 425 . . . . . . . . . . . 12
6362exp31 588 . . . . . . . . . . 11
6463com14 84 . . . . . . . . . 10
652, 29, 643syl 19 . . . . . . . . 9 FriendGrph
6665imp 419 . . . . . . . 8 FriendGrph
6766imp41 577 . . . . . . 7 FriendGrph
68 2pthon3v 21524 . . . . . . 7 PathOn
696, 15, 28, 67, 68syl31anc 1187 . . . . . 6 FriendGrph PathOn
7069ex 424 . . . . 5 FriendGrph PathOn
7170rexlimdva 2787 . . . 4 FriendGrph PathOn
7271ralimdva 2741 . . 3 FriendGrph PathOn
7372ralimdva 2741 . 2 FriendGrph PathOn
741, 73mpd 15 1 FriendGrph PathOn
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359   w3a 936  wex 1547   wceq 1649   wcel 1721   wne 2564  wral 2663  wrex 2664  cvv 2913   cdif 3274  csn 3771  cpr 3772   class class class wbr 4167  ccnv 4831   cdm 4832   crn 4833  wf1o 5407  cfv 5408  (class class class)co 6034  c2 9995  chash 11559   USGrph cusg 21304   PathOn cpthon 21450   FriendGrph cfrgra 28032 This theorem is referenced by:  frconngra  28065 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-oadd 6678  df-er 6855  df-map 6970  df-pm 6971  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-card 7773  df-cda 7995  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-nn 9947  df-2 10004  df-3 10005  df-n0 10168  df-z 10229  df-uz 10435  df-fz 10990  df-fzo 11080  df-hash 11560  df-word 11664  df-usgra 21306  df-wlk 21453  df-trail 21454  df-pth 21455  df-wlkon 21459  df-pthon 21461  df-frgra 28033
 Copyright terms: Public domain W3C validator