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

Theorem friendshipgt3 25720
 Description: The friendship theorem for big graphs: In every finite friendship graph with order greater than 3 there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 9-Oct-2018.)
Assertion
Ref Expression
friendshipgt3 FriendGrph
Distinct variable groups:   ,,   ,,

Proof of Theorem friendshipgt3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frgraregorufrg 25671 . . 3 FriendGrph VDeg RegUSGrph
213ad2ant1 1026 . 2 FriendGrph VDeg RegUSGrph
3 frgraogt3nreg 25719 . 2 FriendGrph RegUSGrph
4 frisusgra 25591 . . . . 5 FriendGrph USGrph
543ad2ant1 1026 . . . 4 FriendGrph USGrph
6 simp2 1006 . . . 4 FriendGrph
7 0red 9633 . . . . . . . 8
8 3re 10672 . . . . . . . . 9
98a1i 11 . . . . . . . 8
10 hashcl 12524 . . . . . . . . . 10
1110nn0red 10915 . . . . . . . . 9
1211adantr 466 . . . . . . . 8
13 3pos 10692 . . . . . . . . 9
1413a1i 11 . . . . . . . 8
15 simpr 462 . . . . . . . 8
167, 9, 12, 14, 15lttrd 9785 . . . . . . 7
1716gt0ne0d 10167 . . . . . 6
18 hasheq0 12530 . . . . . . . 8
1918adantr 466 . . . . . . 7
2019necon3bid 2680 . . . . . 6
2117, 20mpbid 213 . . . . 5
22213adant1 1023 . . . 4 FriendGrph
23 usgn0fidegnn0 25628 . . . 4 USGrph VDeg
245, 6, 22, 23syl3anc 1264 . . 3 FriendGrph VDeg
25 r19.26 2953 . . . . . . . 8 VDeg RegUSGrph RegUSGrph VDeg RegUSGrph RegUSGrph
26 simpllr 767 . . . . . . . . . 10 VDeg FriendGrph
27 fveq2 5872 . . . . . . . . . . . . . . . . 17 VDeg VDeg
2827eqeq1d 2422 . . . . . . . . . . . . . . . 16 VDeg VDeg
2928rspcev 3179 . . . . . . . . . . . . . . 15 VDeg VDeg
3029adantlr 719 . . . . . . . . . . . . . 14 VDeg VDeg
3130adantr 466 . . . . . . . . . . . . 13 VDeg FriendGrph VDeg
32 ornld 906 . . . . . . . . . . . . 13 VDeg VDeg RegUSGrph RegUSGrph
3331, 32syl 17 . . . . . . . . . . . 12 VDeg FriendGrph VDeg RegUSGrph RegUSGrph
3433adantr 466 . . . . . . . . . . 11 VDeg FriendGrph VDeg RegUSGrph RegUSGrph
35 eqeq2 2435 . . . . . . . . . . . . . . . 16 VDeg VDeg
3635rexbidv 2937 . . . . . . . . . . . . . . 15 VDeg VDeg
37 breq2 4421 . . . . . . . . . . . . . . . 16 RegUSGrph RegUSGrph
3837orbi1d 707 . . . . . . . . . . . . . . 15 RegUSGrph RegUSGrph
3936, 38imbi12d 321 . . . . . . . . . . . . . 14 VDeg RegUSGrph VDeg RegUSGrph
4037notbid 295 . . . . . . . . . . . . . 14 RegUSGrph RegUSGrph
4139, 40anbi12d 715 . . . . . . . . . . . . 13 VDeg RegUSGrph RegUSGrph VDeg RegUSGrph RegUSGrph
4241imbi1d 318 . . . . . . . . . . . 12 VDeg RegUSGrph RegUSGrph VDeg RegUSGrph RegUSGrph
4342adantl 467 . . . . . . . . . . 11 VDeg FriendGrph VDeg RegUSGrph RegUSGrph VDeg RegUSGrph RegUSGrph
4434, 43mpbird 235 . . . . . . . . . 10 VDeg FriendGrph VDeg RegUSGrph RegUSGrph
4526, 44rspcimdv 3180 . . . . . . . . 9 VDeg FriendGrph VDeg RegUSGrph RegUSGrph
4645com12 32 . . . . . . . 8 VDeg RegUSGrph RegUSGrph VDeg FriendGrph
4725, 46sylbir 216 . . . . . . 7 VDeg RegUSGrph RegUSGrph VDeg FriendGrph
4847expcom 436 . . . . . 6 RegUSGrph VDeg RegUSGrph VDeg FriendGrph
4948com13 83 . . . . 5 VDeg FriendGrph VDeg RegUSGrph RegUSGrph
5049exp31 607 . . . 4 VDeg FriendGrph VDeg RegUSGrph RegUSGrph
5150rexlimivv 2920 . . 3 VDeg FriendGrph VDeg RegUSGrph RegUSGrph
5224, 51mpcom 37 . 2 FriendGrph VDeg RegUSGrph RegUSGrph
532, 3, 52mp2d 46 1 FriendGrph
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370   w3a 982   wceq 1437   wcel 1867   wne 2616  wral 2773  wrex 2774   cdif 3430  c0 3758  csn 3993  cpr 3995  cop 3999   class class class wbr 4417   crn 4846  cfv 5592  (class class class)co 6296  cfn 7568  cr 9527  cc0 9528   clt 9664  c3 10649  cn0 10858  chash 12501   USGrph cusg 24929   VDeg cvdg 25492   RegUSGrph crusgra 25522   FriendGrph cfrgra 25587 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4529  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-inf2 8137  ax-cnex 9584  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604  ax-pre-mulgt0 9605  ax-pre-sup 9606 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-ot 4002  df-uni 4214  df-int 4250  df-iun 4295  df-disj 4389  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-se 4805  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-isom 5601  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-1o 7181  df-2o 7182  df-oadd 7185  df-er 7362  df-ec 7364  df-qs 7368  df-map 7473  df-pm 7474  df-en 7569  df-dom 7570  df-sdom 7571  df-fin 7572  df-sup 7953  df-inf 7954  df-oi 8016  df-card 8363  df-cda 8587  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670  df-sub 9851  df-neg 9852  df-div 10259  df-nn 10599  df-2 10657  df-3 10658  df-n0 10859  df-z 10927  df-uz 11149  df-rp 11292  df-xadd 11399  df-ico 11630  df-fz 11772  df-fzo 11903  df-fl 12014  df-mod 12083  df-seq 12200  df-exp 12259  df-hash 12502  df-word 12640  df-lsw 12641  df-concat 12642  df-s1 12643  df-substr 12644  df-reps 12647  df-csh 12865  df-s2 12918  df-cj 13130  df-re 13131  df-im 13132  df-sqrt 13266  df-abs 13267  df-clim 13519  df-sum 13720  df-dvds 14273  df-gcd 14432  df-prm 14583  df-phi 14672  df-usgra 24932  df-nbgra 25019  df-wlk 25107  df-trail 25108  df-pth 25109  df-spth 25110  df-wlkon 25113  df-spthon 25116  df-wwlk 25278  df-wwlkn 25279  df-clwwlk 25350  df-clwwlkn 25351  df-2wlkonot 25457  df-2spthonot 25459  df-2spthsot 25460  df-vdgr 25493  df-rgra 25523  df-rusgra 25524  df-frgra 25588 This theorem is referenced by:  friendship  25721
 Copyright terms: Public domain W3C validator