![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > friendship | Structured version Visualization version GIF version |
Description: The friendship theorem: In every finite (nonempty) friendship graph there is a vertex which is adjacent to all other vertices. This is Metamath 100 proof #83. (Contributed by Alexander van der Vekens, 9-Oct-2018.) |
Ref | Expression |
---|---|
friendship.v | ⊢ 𝑉 = (Vtx‘𝐺) |
Ref | Expression |
---|---|
friendship | ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 1233 | . . . 4 ⊢ ((3 < (♯‘𝑉) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → 𝐺 ∈ FriendGraph ) | |
2 | simpr3 1237 | . . . 4 ⊢ ((3 < (♯‘𝑉) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → 𝑉 ∈ Fin) | |
3 | simpl 468 | . . . 4 ⊢ ((3 < (♯‘𝑉) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → 3 < (♯‘𝑉)) | |
4 | friendship.v | . . . . 5 ⊢ 𝑉 = (Vtx‘𝐺) | |
5 | 4 | friendshipgt3 27590 | . . . 4 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 3 < (♯‘𝑉)) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) |
6 | 1, 2, 3, 5 | syl3anc 1476 | . . 3 ⊢ ((3 < (♯‘𝑉) ∧ (𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin)) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) |
7 | 6 | ex 397 | . 2 ⊢ (3 < (♯‘𝑉) → ((𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
8 | hashcl 13342 | . . . . . . . . 9 ⊢ (𝑉 ∈ Fin → (♯‘𝑉) ∈ ℕ0) | |
9 | simplr 752 | . . . . . . . . . . 11 ⊢ ((((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin) ∧ (¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅)) → 𝑉 ∈ Fin) | |
10 | hashge1 13373 | . . . . . . . . . . . 12 ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 1 ≤ (♯‘𝑉)) | |
11 | 10 | ad2ant2l 740 | . . . . . . . . . . 11 ⊢ ((((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin) ∧ (¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅)) → 1 ≤ (♯‘𝑉)) |
12 | nn0re 11501 | . . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑉) ∈ ℕ0 → (♯‘𝑉) ∈ ℝ) | |
13 | 3re 11294 | . . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℝ | |
14 | lenlt 10316 | . . . . . . . . . . . . . . . . 17 ⊢ (((♯‘𝑉) ∈ ℝ ∧ 3 ∈ ℝ) → ((♯‘𝑉) ≤ 3 ↔ ¬ 3 < (♯‘𝑉))) | |
15 | 12, 13, 14 | sylancl 574 | . . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑉) ∈ ℕ0 → ((♯‘𝑉) ≤ 3 ↔ ¬ 3 < (♯‘𝑉))) |
16 | 15 | biimprd 238 | . . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑉) ∈ ℕ0 → (¬ 3 < (♯‘𝑉) → (♯‘𝑉) ≤ 3)) |
17 | 16 | adantr 466 | . . . . . . . . . . . . . 14 ⊢ (((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin) → (¬ 3 < (♯‘𝑉) → (♯‘𝑉) ≤ 3)) |
18 | 17 | com12 32 | . . . . . . . . . . . . 13 ⊢ (¬ 3 < (♯‘𝑉) → (((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin) → (♯‘𝑉) ≤ 3)) |
19 | 18 | adantr 466 | . . . . . . . . . . . 12 ⊢ ((¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅) → (((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin) → (♯‘𝑉) ≤ 3)) |
20 | 19 | impcom 394 | . . . . . . . . . . 11 ⊢ ((((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin) ∧ (¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅)) → (♯‘𝑉) ≤ 3) |
21 | 9, 11, 20 | 3jca 1122 | . . . . . . . . . 10 ⊢ ((((♯‘𝑉) ∈ ℕ0 ∧ 𝑉 ∈ Fin) ∧ (¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅)) → (𝑉 ∈ Fin ∧ 1 ≤ (♯‘𝑉) ∧ (♯‘𝑉) ≤ 3)) |
22 | 21 | exp31 406 | . . . . . . . . 9 ⊢ ((♯‘𝑉) ∈ ℕ0 → (𝑉 ∈ Fin → ((¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin ∧ 1 ≤ (♯‘𝑉) ∧ (♯‘𝑉) ≤ 3)))) |
23 | 8, 22 | mpcom 38 | . . . . . . . 8 ⊢ (𝑉 ∈ Fin → ((¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅) → (𝑉 ∈ Fin ∧ 1 ≤ (♯‘𝑉) ∧ (♯‘𝑉) ≤ 3))) |
24 | 23 | impcom 394 | . . . . . . 7 ⊢ (((¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅) ∧ 𝑉 ∈ Fin) → (𝑉 ∈ Fin ∧ 1 ≤ (♯‘𝑉) ∧ (♯‘𝑉) ≤ 3)) |
25 | hash1to3 13468 | . . . . . . 7 ⊢ ((𝑉 ∈ Fin ∧ 1 ≤ (♯‘𝑉) ∧ (♯‘𝑉) ≤ 3) → ∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) | |
26 | vex 3354 | . . . . . . . . . 10 ⊢ 𝑎 ∈ V | |
27 | eqid 2771 | . . . . . . . . . . 11 ⊢ (Edg‘𝐺) = (Edg‘𝐺) | |
28 | 4, 27 | 1to3vfriendship 27456 | . . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ (𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐})) → (𝐺 ∈ FriendGraph → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
29 | 26, 28 | mpan 670 | . . . . . . . . 9 ⊢ ((𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}) → (𝐺 ∈ FriendGraph → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
30 | 29 | exlimiv 2010 | . . . . . . . 8 ⊢ (∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}) → (𝐺 ∈ FriendGraph → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
31 | 30 | exlimivv 2012 | . . . . . . 7 ⊢ (∃𝑎∃𝑏∃𝑐(𝑉 = {𝑎} ∨ 𝑉 = {𝑎, 𝑏} ∨ 𝑉 = {𝑎, 𝑏, 𝑐}) → (𝐺 ∈ FriendGraph → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
32 | 24, 25, 31 | 3syl 18 | . . . . . 6 ⊢ (((¬ 3 < (♯‘𝑉) ∧ 𝑉 ≠ ∅) ∧ 𝑉 ∈ Fin) → (𝐺 ∈ FriendGraph → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
33 | 32 | exp31 406 | . . . . 5 ⊢ (¬ 3 < (♯‘𝑉) → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (𝐺 ∈ FriendGraph → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))))) |
34 | 33 | com14 96 | . . . 4 ⊢ (𝐺 ∈ FriendGraph → (𝑉 ≠ ∅ → (𝑉 ∈ Fin → (¬ 3 < (♯‘𝑉) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))))) |
35 | 34 | 3imp 1101 | . . 3 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → (¬ 3 < (♯‘𝑉) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
36 | 35 | com12 32 | . 2 ⊢ (¬ 3 < (♯‘𝑉) → ((𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺))) |
37 | 7, 36 | pm2.61i 176 | 1 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ (Edg‘𝐺)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 382 ∨ w3o 1070 ∧ w3a 1071 = wceq 1631 ∃wex 1852 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 ∃wrex 3062 Vcvv 3351 ∖ cdif 3720 ∅c0 4063 {csn 4316 {cpr 4318 {ctp 4320 class class class wbr 4786 ‘cfv 6029 Fincfn 8107 ℝcr 10135 1c1 10137 < clt 10274 ≤ cle 10275 3c3 11271 ℕ0cn0 11492 ♯chash 13314 Vtxcvtx 26088 Edgcedg 26153 FriendGraph cfrgr 27431 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7094 ax-inf2 8700 ax-ac2 9485 ax-cnex 10192 ax-resscn 10193 ax-1cn 10194 ax-icn 10195 ax-addcl 10196 ax-addrcl 10197 ax-mulcl 10198 ax-mulrcl 10199 ax-mulcom 10200 ax-addass 10201 ax-mulass 10202 ax-distr 10203 ax-i2m1 10204 ax-1ne0 10205 ax-1rid 10206 ax-rnegex 10207 ax-rrecex 10208 ax-cnre 10209 ax-pre-lttri 10210 ax-pre-lttrn 10211 ax-pre-ltadd 10212 ax-pre-mulgt0 10213 ax-pre-sup 10214 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-ifp 1050 df-3or 1072 df-3an 1073 df-tru 1634 df-fal 1637 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-int 4612 df-iun 4656 df-disj 4755 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-se 5209 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5821 df-ord 5867 df-on 5868 df-lim 5869 df-suc 5870 df-iota 5992 df-fun 6031 df-fn 6032 df-f 6033 df-f1 6034 df-fo 6035 df-f1o 6036 df-fv 6037 df-isom 6038 df-riota 6752 df-ov 6794 df-oprab 6795 df-mpt2 6796 df-om 7211 df-1st 7313 df-2nd 7314 df-wrecs 7557 df-recs 7619 df-rdg 7657 df-1o 7711 df-2o 7712 df-3o 7713 df-oadd 7715 df-er 7894 df-ec 7896 df-qs 7900 df-map 8009 df-pm 8010 df-en 8108 df-dom 8109 df-sdom 8110 df-fin 8111 df-sup 8502 df-inf 8503 df-oi 8569 df-card 8963 df-ac 9137 df-cda 9190 df-pnf 10276 df-mnf 10277 df-xr 10278 df-ltxr 10279 df-le 10280 df-sub 10468 df-neg 10469 df-div 10885 df-nn 11221 df-2 11279 df-3 11280 df-n0 11493 df-xnn0 11564 df-z 11578 df-uz 11887 df-rp 12029 df-xadd 12145 df-ico 12379 df-fz 12527 df-fzo 12667 df-fl 12794 df-mod 12870 df-seq 13002 df-exp 13061 df-hash 13315 df-word 13488 df-lsw 13489 df-concat 13490 df-s1 13491 df-substr 13492 df-reps 13495 df-csh 13737 df-s2 13795 df-s3 13796 df-cj 14040 df-re 14041 df-im 14042 df-sqrt 14176 df-abs 14177 df-clim 14420 df-sum 14618 df-dvds 15183 df-gcd 15418 df-prm 15586 df-phi 15671 df-vtx 26090 df-iedg 26091 df-edg 26154 df-uhgr 26167 df-ushgr 26168 df-upgr 26191 df-umgr 26192 df-uspgr 26260 df-usgr 26261 df-fusgr 26425 df-nbgr 26441 df-vtxdg 26590 df-rgr 26681 df-rusgr 26682 df-wlks 26723 df-wlkson 26724 df-trls 26817 df-trlson 26818 df-pths 26840 df-spths 26841 df-pthson 26842 df-spthson 26843 df-wwlks 26951 df-wwlksn 26952 df-wwlksnon 26953 df-wspthsn 26954 df-wspthsnon 26955 df-clwwlk 27125 df-clwwlkn 27169 df-clwwlknon 27253 df-conngr 27360 df-frgr 27432 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |