Metamath Proof Explorer

Theorem frgrregord013

Description: If a finite friendship graph is K-regular, then it must have order 0, 1 or 3. (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Hypothesis frgrreggt1.v ⊢V=Vtx⁡G
Assertion frgrregord013 ⊢G∈FriendGraph∧V∈Fin∧GRegUSGraphK→V=0∨V=1∨V=3

Proof

Step Hyp Ref Expression
1 frgrreggt1.v ⊢V=Vtx⁡G
2 hashcl ⊢V∈Fin→V∈ℕ0
3 ax-1 ⊢V=0∨V=1∨V=3→V∈ℕ0∧V∈Fin∧G∈FriendGraph∧GRegUSGraphK→V=0∨V=1∨V=3
4 3ioran ⊢¬V=0∨V=1∨V=3↔¬V=0∧¬V=1∧¬V=3
5 df-ne ⊢V≠0↔¬V=0
6 hasheq0 ⊢V∈Fin→V=0↔V=∅
7 6 necon3bid ⊢V∈Fin→V≠0↔V≠∅
8 7 biimpa ⊢V∈Fin∧V≠0→V≠∅
9 elnnne0 ⊢V∈ℕ↔V∈ℕ0∧V≠0
10 df-ne ⊢V≠1↔¬V=1
11 eluz2b3 ⊢V∈ℤ≥2↔V∈ℕ∧V≠1
12 hash2prde ⊢V∈Fin∧V=2→∃a∃ba≠b∧V=ab
13 vex ⊢a∈V
14 13 a1i ⊢a≠b→a∈V
15 vex ⊢b∈V
16 15 a1i ⊢a≠b→b∈V
17 id ⊢a≠b→a≠b
18 14 16 17 3jca ⊢a≠b→a∈V∧b∈V∧a≠b
19 1 eqeq1i ⊢V=ab↔Vtx⁡G=ab
20 19 biimpi ⊢V=ab→Vtx⁡G=ab
21 nfrgr2v ⊢a∈V∧b∈V∧a≠b∧Vtx⁡G=ab→G∉FriendGraph
22 18 20 21 syl2an ⊢a≠b∧V=ab→G∉FriendGraph
23 df-nel ⊢G∉FriendGraph↔¬G∈FriendGraph
24 22 23 sylib ⊢a≠b∧V=ab→¬G∈FriendGraph
25 24 pm2.21d ⊢a≠b∧V=ab→G∈FriendGraph→V≠∅→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
26 25 com23 ⊢a≠b∧V=ab→V≠∅→G∈FriendGraph→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
27 26 exlimivv ⊢∃a∃ba≠b∧V=ab→V≠∅→G∈FriendGraph→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
28 12 27 syl ⊢V∈Fin∧V=2→V≠∅→G∈FriendGraph→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
29 28 ex ⊢V∈Fin→V=2→V≠∅→G∈FriendGraph→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
30 29 com23 ⊢V∈Fin→V≠∅→V=2→G∈FriendGraph→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
31 30 com14 ⊢G∈FriendGraph→V≠∅→V=2→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
32 31 a1i ⊢V∈ℤ≥2→G∈FriendGraph→V≠∅→V=2→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
33 32 3imp ⊢V∈ℤ≥2∧G∈FriendGraph∧V≠∅→V=2→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
34 33 com12 ⊢V=2→V∈ℤ≥2∧G∈FriendGraph∧V≠∅→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
35 eqid ⊢VtxDeg⁡G=VtxDeg⁡G
36 1 35 rusgrprop0 ⊢GRegUSGraphK→G∈USGraph∧K∈ℕ0*∧∀v∈VVtxDeg⁡G⁡v=K
37 eluz2gt1 ⊢V∈ℤ≥2→1<V
38 37 anim1ci ⊢V∈ℤ≥2∧G∈FriendGraph→G∈FriendGraph∧1<V
39 1 vdgn0frgrv2 ⊢G∈FriendGraph∧v∈V→1<V→VtxDeg⁡G⁡v≠0
40 39 impancom ⊢G∈FriendGraph∧1<V→v∈V→VtxDeg⁡G⁡v≠0
41 40 ralrimiv ⊢G∈FriendGraph∧1<V→∀v∈VVtxDeg⁡G⁡v≠0
42 eqeq2 ⊢K=0→VtxDeg⁡G⁡v=K↔VtxDeg⁡G⁡v=0
43 42 ralbidv ⊢K=0→∀v∈VVtxDeg⁡G⁡v=K↔∀v∈VVtxDeg⁡G⁡v=0
44 r19.26 ⊢∀v∈VVtxDeg⁡G⁡v=0∧VtxDeg⁡G⁡v≠0↔∀v∈VVtxDeg⁡G⁡v=0∧∀v∈VVtxDeg⁡G⁡v≠0
45 nne ⊢¬VtxDeg⁡G⁡v≠0↔VtxDeg⁡G⁡v=0
46 45 bicomi ⊢VtxDeg⁡G⁡v=0↔¬VtxDeg⁡G⁡v≠0
47 46 anbi1i ⊢VtxDeg⁡G⁡v=0∧VtxDeg⁡G⁡v≠0↔¬VtxDeg⁡G⁡v≠0∧VtxDeg⁡G⁡v≠0
48 ancom ⊢¬VtxDeg⁡G⁡v≠0∧VtxDeg⁡G⁡v≠0↔VtxDeg⁡G⁡v≠0∧¬VtxDeg⁡G⁡v≠0
49 pm3.24 ⊢¬VtxDeg⁡G⁡v≠0∧¬VtxDeg⁡G⁡v≠0
50 49 bifal ⊢VtxDeg⁡G⁡v≠0∧¬VtxDeg⁡G⁡v≠0↔⊥
51 47 48 50 3bitri ⊢VtxDeg⁡G⁡v=0∧VtxDeg⁡G⁡v≠0↔⊥
52 51 ralbii ⊢∀v∈VVtxDeg⁡G⁡v=0∧VtxDeg⁡G⁡v≠0↔∀v∈V⊥
53 r19.3rzv ⊢V≠∅→⊥↔∀v∈V⊥
54 falim ⊢⊥→V=0∨V=1∨V=3
55 53 54 syl6bir ⊢V≠∅→∀v∈V⊥→V=0∨V=1∨V=3
56 55 adantl ⊢V∈Fin∧V≠∅→∀v∈V⊥→V=0∨V=1∨V=3
57 56 com12 ⊢∀v∈V⊥→V∈Fin∧V≠∅→V=0∨V=1∨V=3
58 52 57 sylbi ⊢∀v∈VVtxDeg⁡G⁡v=0∧VtxDeg⁡G⁡v≠0→V∈Fin∧V≠∅→V=0∨V=1∨V=3
59 44 58 sylbir ⊢∀v∈VVtxDeg⁡G⁡v=0∧∀v∈VVtxDeg⁡G⁡v≠0→V∈Fin∧V≠∅→V=0∨V=1∨V=3
60 59 ex ⊢∀v∈VVtxDeg⁡G⁡v=0→∀v∈VVtxDeg⁡G⁡v≠0→V∈Fin∧V≠∅→V=0∨V=1∨V=3
61 43 60 syl6bi ⊢K=0→∀v∈VVtxDeg⁡G⁡v=K→∀v∈VVtxDeg⁡G⁡v≠0→V∈Fin∧V≠∅→V=0∨V=1∨V=3
62 61 com4t ⊢∀v∈VVtxDeg⁡G⁡v≠0→V∈Fin∧V≠∅→K=0→∀v∈VVtxDeg⁡G⁡v=K→V=0∨V=1∨V=3
63 38 41 62 3syl ⊢V∈ℤ≥2∧G∈FriendGraph→V∈Fin∧V≠∅→K=0→∀v∈VVtxDeg⁡G⁡v=K→V=0∨V=1∨V=3
64 63 ex ⊢V∈ℤ≥2→G∈FriendGraph→V∈Fin∧V≠∅→K=0→∀v∈VVtxDeg⁡G⁡v=K→V=0∨V=1∨V=3
65 64 com25 ⊢V∈ℤ≥2→∀v∈VVtxDeg⁡G⁡v=K→V∈Fin∧V≠∅→K=0→G∈FriendGraph→V=0∨V=1∨V=3
66 65 adantl ⊢¬V=3∧¬V=2∧V∈ℤ≥2→∀v∈VVtxDeg⁡G⁡v=K→V∈Fin∧V≠∅→K=0→G∈FriendGraph→V=0∨V=1∨V=3
67 66 com15 ⊢G∈FriendGraph→∀v∈VVtxDeg⁡G⁡v=K→V∈Fin∧V≠∅→K=0→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
68 67 com12 ⊢∀v∈VVtxDeg⁡G⁡v=K→G∈FriendGraph→V∈Fin∧V≠∅→K=0→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
69 68 3ad2ant3 ⊢G∈USGraph∧K∈ℕ0*∧∀v∈VVtxDeg⁡G⁡v=K→G∈FriendGraph→V∈Fin∧V≠∅→K=0→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
70 36 69 syl ⊢GRegUSGraphK→G∈FriendGraph→V∈Fin∧V≠∅→K=0→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
71 70 impcom ⊢G∈FriendGraph∧GRegUSGraphK→V∈Fin∧V≠∅→K=0→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
72 71 impcom ⊢V∈Fin∧V≠∅∧G∈FriendGraph∧GRegUSGraphK→K=0→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
73 1 frrusgrord ⊢V∈Fin∧V≠∅→G∈FriendGraph∧GRegUSGraphK→V=K⁢K−1+1
74 73 imp ⊢V∈Fin∧V≠∅∧G∈FriendGraph∧GRegUSGraphK→V=K⁢K−1+1
75 id ⊢K=2→K=2
76 oveq1 ⊢K=2→K−1=2−1
77 75 76 oveq12d ⊢K=2→K⁢K−1=2⁢2−1
78 77 oveq1d ⊢K=2→K⁢K−1+1=2⁢2−1+1
79 2m1e1 ⊢2−1=1
80 79 oveq2i ⊢2⁢2−1=2⋅1
81 2t1e2 ⊢2⋅1=2
82 80 81 eqtri ⊢2⁢2−1=2
83 82 oveq1i ⊢2⁢2−1+1=2+1
84 2p1e3 ⊢2+1=3
85 83 84 eqtri ⊢2⁢2−1+1=3
86 78 85 eqtrdi ⊢K=2→K⁢K−1+1=3
87 86 eqeq2d ⊢K=2→V=K⁢K−1+1↔V=3
88 pm2.21 ⊢¬V=3→V=3→V=0∨V=1∨V=3
89 88 ad2antrr ⊢¬V=3∧¬V=2∧V∈ℤ≥2→V=3→V=0∨V=1∨V=3
90 89 com12 ⊢V=3→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
91 87 90 syl6bi ⊢K=2→V=K⁢K−1+1→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
92 74 91 syl5com ⊢V∈Fin∧V≠∅∧G∈FriendGraph∧GRegUSGraphK→K=2→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
93 1 frgrreg ⊢V∈Fin∧V≠∅→G∈FriendGraph∧GRegUSGraphK→K=0∨K=2
94 93 imp ⊢V∈Fin∧V≠∅∧G∈FriendGraph∧GRegUSGraphK→K=0∨K=2
95 72 92 94 mpjaod ⊢V∈Fin∧V≠∅∧G∈FriendGraph∧GRegUSGraphK→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
96 95 exp32 ⊢V∈Fin∧V≠∅→G∈FriendGraph→GRegUSGraphK→¬V=3∧¬V=2∧V∈ℤ≥2→V=0∨V=1∨V=3
97 96 com34 ⊢V∈Fin∧V≠∅→G∈FriendGraph→¬V=3∧¬V=2∧V∈ℤ≥2→GRegUSGraphK→V=0∨V=1∨V=3
98 97 com23 ⊢V∈Fin∧V≠∅→¬V=3∧¬V=2∧V∈ℤ≥2→G∈FriendGraph→GRegUSGraphK→V=0∨V=1∨V=3
99 98 exp4c ⊢V∈Fin∧V≠∅→¬V=3→¬V=2→V∈ℤ≥2→G∈FriendGraph→GRegUSGraphK→V=0∨V=1∨V=3
100 99 com34 ⊢V∈Fin∧V≠∅→¬V=3→V∈ℤ≥2→¬V=2→G∈FriendGraph→GRegUSGraphK→V=0∨V=1∨V=3
101 100 com25 ⊢V∈Fin∧V≠∅→G∈FriendGraph→V∈ℤ≥2→¬V=2→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
102 101 ex ⊢V∈Fin→V≠∅→G∈FriendGraph→V∈ℤ≥2→¬V=2→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
103 102 com23 ⊢V∈Fin→G∈FriendGraph→V≠∅→V∈ℤ≥2→¬V=2→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
104 103 com14 ⊢V∈ℤ≥2→G∈FriendGraph→V≠∅→V∈Fin→¬V=2→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
105 104 3imp ⊢V∈ℤ≥2∧G∈FriendGraph∧V≠∅→V∈Fin→¬V=2→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
106 105 com3r ⊢¬V=2→V∈ℤ≥2∧G∈FriendGraph∧V≠∅→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
107 34 106 pm2.61i ⊢V∈ℤ≥2∧G∈FriendGraph∧V≠∅→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
108 107 3exp ⊢V∈ℤ≥2→G∈FriendGraph→V≠∅→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
109 11 108 sylbir ⊢V∈ℕ∧V≠1→G∈FriendGraph→V≠∅→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
110 109 ex ⊢V∈ℕ→V≠1→G∈FriendGraph→V≠∅→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
111 10 110 biimtrrid ⊢V∈ℕ→¬V=1→G∈FriendGraph→V≠∅→V∈Fin→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
112 111 com25 ⊢V∈ℕ→V∈Fin→G∈FriendGraph→V≠∅→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
113 9 112 sylbir ⊢V∈ℕ0∧V≠0→V∈Fin→G∈FriendGraph→V≠∅→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
114 113 ex ⊢V∈ℕ0→V≠0→V∈Fin→G∈FriendGraph→V≠∅→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
115 114 impcomd ⊢V∈ℕ0→V∈Fin∧V≠0→G∈FriendGraph→V≠∅→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
116 115 com14 ⊢V≠∅→V∈Fin∧V≠0→G∈FriendGraph→V∈ℕ0→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
117 8 116 mpcom ⊢V∈Fin∧V≠0→G∈FriendGraph→V∈ℕ0→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
118 117 ex ⊢V∈Fin→V≠0→G∈FriendGraph→V∈ℕ0→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
119 118 com14 ⊢V∈ℕ0→V≠0→G∈FriendGraph→V∈Fin→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
120 5 119 biimtrrid ⊢V∈ℕ0→¬V=0→G∈FriendGraph→V∈Fin→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
121 120 com24 ⊢V∈ℕ0→V∈Fin→G∈FriendGraph→¬V=0→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
122 121 3imp ⊢V∈ℕ0∧V∈Fin∧G∈FriendGraph→¬V=0→¬V=1→¬V=3→GRegUSGraphK→V=0∨V=1∨V=3
123 122 com25 ⊢V∈ℕ0∧V∈Fin∧G∈FriendGraph→GRegUSGraphK→¬V=1→¬V=3→¬V=0→V=0∨V=1∨V=3
124 123 imp ⊢V∈ℕ0∧V∈Fin∧G∈FriendGraph∧GRegUSGraphK→¬V=1→¬V=3→¬V=0→V=0∨V=1∨V=3
125 124 com14 ⊢¬V=0→¬V=1→¬V=3→V∈ℕ0∧V∈Fin∧G∈FriendGraph∧GRegUSGraphK→V=0∨V=1∨V=3
126 125 3imp ⊢¬V=0∧¬V=1∧¬V=3→V∈ℕ0∧V∈Fin∧G∈FriendGraph∧GRegUSGraphK→V=0∨V=1∨V=3
127 4 126 sylbi ⊢¬V=0∨V=1∨V=3→V∈ℕ0∧V∈Fin∧G∈FriendGraph∧GRegUSGraphK→V=0∨V=1∨V=3
128 3 127 pm2.61i ⊢V∈ℕ0∧V∈Fin∧G∈FriendGraph∧GRegUSGraphK→V=0∨V=1∨V=3
129 128 3exp1 ⊢V∈ℕ0→V∈Fin→G∈FriendGraph→GRegUSGraphK→V=0∨V=1∨V=3
130 2 129 mpcom ⊢V∈Fin→G∈FriendGraph→GRegUSGraphK→V=0∨V=1∨V=3
131 130 3imp21 ⊢G∈FriendGraph∧V∈Fin∧GRegUSGraphK→V=0∨V=1∨V=3