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 ∧ G RegUSGraph K → 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 ∧ G RegUSGraph K → 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 ∃ b a ≠ b ∧ V = a b
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 = a b ↔ Vtx ⁡ G = a b
20 19 biimpi ⊢ V = a b → Vtx ⁡ G = a b
21 nfrgr2v ⊢ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ Vtx ⁡ G = a b → G ∉ FriendGraph
22 18 20 21 syl2an ⊢ a ≠ b ∧ V = a b → G ∉ FriendGraph
23 df-nel ⊢ G ∉ FriendGraph ↔ ¬ G ∈ FriendGraph
24 22 23 sylib ⊢ a ≠ b ∧ V = a b → ¬ G ∈ FriendGraph
25 24 pm2.21d ⊢ a ≠ b ∧ V = a b → G ∈ FriendGraph → V ≠ ∅ → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
26 25 com23 ⊢ a ≠ b ∧ V = a b → V ≠ ∅ → G ∈ FriendGraph → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
27 26 exlimivv ⊢ ∃ a ∃ b a ≠ b ∧ V = a b → V ≠ ∅ → G ∈ FriendGraph → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
28 12 27 syl ⊢ V ∈ Fin ∧ V = 2 → V ≠ ∅ → G ∈ FriendGraph → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
29 28 ex ⊢ V ∈ Fin → V = 2 → V ≠ ∅ → G ∈ FriendGraph → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
30 29 com23 ⊢ V ∈ Fin → V ≠ ∅ → V = 2 → G ∈ FriendGraph → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
31 30 com14 ⊢ G ∈ FriendGraph → V ≠ ∅ → V = 2 → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
32 31 a1i ⊢ V ∈ ℤ ≥ 2 → G ∈ FriendGraph → V ≠ ∅ → V = 2 → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
33 32 3imp ⊢ V ∈ ℤ ≥ 2 ∧ G ∈ FriendGraph ∧ V ≠ ∅ → V = 2 → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
34 33 com12 ⊢ V = 2 → V ∈ ℤ ≥ 2 ∧ G ∈ FriendGraph ∧ V ≠ ∅ → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
35 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
36 1 35 rusgrprop0 ⊢ G RegUSGraph K → G ∈ USGraph ∧ K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ 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 ∈ V VtxDeg ⁡ G ⁡ v ≠ 0
42 eqeq2 ⊢ K = 0 → VtxDeg ⁡ G ⁡ v = K ↔ VtxDeg ⁡ G ⁡ v = 0
43 42 ralbidv ⊢ K = 0 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K ↔ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = 0
44 r19.26 ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = 0 ∧ VtxDeg ⁡ G ⁡ v ≠ 0 ↔ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = 0 ∧ ∀ v ∈ V VtxDeg ⁡ 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 ∈ V VtxDeg ⁡ 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 biimtrrdi ⊢ 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 ∈ V VtxDeg ⁡ G ⁡ v = 0 ∧ VtxDeg ⁡ G ⁡ v ≠ 0 → V ∈ Fin ∧ V ≠ ∅ → V = 0 ∨ V = 1 ∨ V = 3
59 44 58 sylbir ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = 0 ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ≠ 0 → V ∈ Fin ∧ V ≠ ∅ → V = 0 ∨ V = 1 ∨ V = 3
60 59 ex ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = 0 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v ≠ 0 → V ∈ Fin ∧ V ≠ ∅ → V = 0 ∨ V = 1 ∨ V = 3
61 43 60 biimtrdi ⊢ K = 0 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → ∀ v ∈ V VtxDeg ⁡ G ⁡ v ≠ 0 → V ∈ Fin ∧ V ≠ ∅ → V = 0 ∨ V = 1 ∨ V = 3
62 61 com4t ⊢ ∀ v ∈ V VtxDeg ⁡ G ⁡ v ≠ 0 → V ∈ Fin ∧ V ≠ ∅ → K = 0 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V = 0 ∨ V = 1 ∨ V = 3
63 38 41 62 3syl ⊢ V ∈ ℤ ≥ 2 ∧ G ∈ FriendGraph → V ∈ Fin ∧ V ≠ ∅ → K = 0 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V = 0 ∨ V = 1 ∨ V = 3
64 63 ex ⊢ V ∈ ℤ ≥ 2 → G ∈ FriendGraph → V ∈ Fin ∧ V ≠ ∅ → K = 0 → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V = 0 ∨ V = 1 ∨ V = 3
65 64 com25 ⊢ V ∈ ℤ ≥ 2 → ∀ v ∈ V VtxDeg ⁡ 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 ∈ V VtxDeg ⁡ G ⁡ v = K → V ∈ Fin ∧ V ≠ ∅ → K = 0 → G ∈ FriendGraph → V = 0 ∨ V = 1 ∨ V = 3
67 66 com15 ⊢ G ∈ FriendGraph → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V ∈ Fin ∧ V ≠ ∅ → K = 0 → ¬ V = 3 ∧ ¬ V = 2 ∧ V ∈ ℤ ≥ 2 → V = 0 ∨ V = 1 ∨ V = 3
68 67 com12 ⊢ ∀ v ∈ V VtxDeg ⁡ 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 ∈ V VtxDeg ⁡ 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 ⊢ G RegUSGraph K → G ∈ FriendGraph → V ∈ Fin ∧ V ≠ ∅ → K = 0 → ¬ V = 3 ∧ ¬ V = 2 ∧ V ∈ ℤ ≥ 2 → V = 0 ∨ V = 1 ∨ V = 3
71 70 impcom ⊢ G ∈ FriendGraph ∧ G RegUSGraph K → 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 ∧ G RegUSGraph K → K = 0 → ¬ V = 3 ∧ ¬ V = 2 ∧ V ∈ ℤ ≥ 2 → V = 0 ∨ V = 1 ∨ V = 3
73 1 frrusgrord ⊢ V ∈ Fin ∧ V ≠ ∅ → G ∈ FriendGraph ∧ G RegUSGraph K → V = K ⁢ K − 1 + 1
74 73 imp ⊢ V ∈ Fin ∧ V ≠ ∅ ∧ G ∈ FriendGraph ∧ G RegUSGraph K → 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 biimtrdi ⊢ 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 ∧ G RegUSGraph K → K = 2 → ¬ V = 3 ∧ ¬ V = 2 ∧ V ∈ ℤ ≥ 2 → V = 0 ∨ V = 1 ∨ V = 3
93 1 frgrreg ⊢ V ∈ Fin ∧ V ≠ ∅ → G ∈ FriendGraph ∧ G RegUSGraph K → K = 0 ∨ K = 2
94 93 imp ⊢ V ∈ Fin ∧ V ≠ ∅ ∧ G ∈ FriendGraph ∧ G RegUSGraph K → K = 0 ∨ K = 2
95 72 92 94 mpjaod ⊢ V ∈ Fin ∧ V ≠ ∅ ∧ G ∈ FriendGraph ∧ G RegUSGraph K → ¬ V = 3 ∧ ¬ V = 2 ∧ V ∈ ℤ ≥ 2 → V = 0 ∨ V = 1 ∨ V = 3
96 95 exp32 ⊢ V ∈ Fin ∧ V ≠ ∅ → G ∈ FriendGraph → G RegUSGraph K → ¬ 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 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
98 97 com23 ⊢ V ∈ Fin ∧ V ≠ ∅ → ¬ V = 3 ∧ ¬ V = 2 ∧ V ∈ ℤ ≥ 2 → G ∈ FriendGraph → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
99 98 exp4c ⊢ V ∈ Fin ∧ V ≠ ∅ → ¬ V = 3 → ¬ V = 2 → V ∈ ℤ ≥ 2 → G ∈ FriendGraph → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
100 99 com34 ⊢ V ∈ Fin ∧ V ≠ ∅ → ¬ V = 3 → V ∈ ℤ ≥ 2 → ¬ V = 2 → G ∈ FriendGraph → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
101 100 com25 ⊢ V ∈ Fin ∧ V ≠ ∅ → G ∈ FriendGraph → V ∈ ℤ ≥ 2 → ¬ V = 2 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
102 101 ex ⊢ V ∈ Fin → V ≠ ∅ → G ∈ FriendGraph → V ∈ ℤ ≥ 2 → ¬ V = 2 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
103 102 com23 ⊢ V ∈ Fin → G ∈ FriendGraph → V ≠ ∅ → V ∈ ℤ ≥ 2 → ¬ V = 2 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
104 103 com14 ⊢ V ∈ ℤ ≥ 2 → G ∈ FriendGraph → V ≠ ∅ → V ∈ Fin → ¬ V = 2 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
105 104 3imp ⊢ V ∈ ℤ ≥ 2 ∧ G ∈ FriendGraph ∧ V ≠ ∅ → V ∈ Fin → ¬ V = 2 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
106 105 com3r ⊢ ¬ V = 2 → V ∈ ℤ ≥ 2 ∧ G ∈ FriendGraph ∧ V ≠ ∅ → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
107 34 106 pm2.61i ⊢ V ∈ ℤ ≥ 2 ∧ G ∈ FriendGraph ∧ V ≠ ∅ → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
108 107 3exp ⊢ V ∈ ℤ ≥ 2 → G ∈ FriendGraph → V ≠ ∅ → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
109 11 108 sylbir ⊢ V ∈ ℕ ∧ V ≠ 1 → G ∈ FriendGraph → V ≠ ∅ → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
110 109 ex ⊢ V ∈ ℕ → V ≠ 1 → G ∈ FriendGraph → V ≠ ∅ → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
111 10 110 biimtrrid ⊢ V ∈ ℕ → ¬ V = 1 → G ∈ FriendGraph → V ≠ ∅ → V ∈ Fin → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
112 111 com25 ⊢ V ∈ ℕ → V ∈ Fin → G ∈ FriendGraph → V ≠ ∅ → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
113 9 112 sylbir ⊢ V ∈ ℕ 0 ∧ V ≠ 0 → V ∈ Fin → G ∈ FriendGraph → V ≠ ∅ → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
114 113 ex ⊢ V ∈ ℕ 0 → V ≠ 0 → V ∈ Fin → G ∈ FriendGraph → V ≠ ∅ → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
115 114 impcomd ⊢ V ∈ ℕ 0 → V ∈ Fin ∧ V ≠ 0 → G ∈ FriendGraph → V ≠ ∅ → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
116 115 com14 ⊢ V ≠ ∅ → V ∈ Fin ∧ V ≠ 0 → G ∈ FriendGraph → V ∈ ℕ 0 → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
117 8 116 mpcom ⊢ V ∈ Fin ∧ V ≠ 0 → G ∈ FriendGraph → V ∈ ℕ 0 → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
118 117 ex ⊢ V ∈ Fin → V ≠ 0 → G ∈ FriendGraph → V ∈ ℕ 0 → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
119 118 com14 ⊢ V ∈ ℕ 0 → V ≠ 0 → G ∈ FriendGraph → V ∈ Fin → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
120 5 119 biimtrrid ⊢ V ∈ ℕ 0 → ¬ V = 0 → G ∈ FriendGraph → V ∈ Fin → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
121 120 com24 ⊢ V ∈ ℕ 0 → V ∈ Fin → G ∈ FriendGraph → ¬ V = 0 → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
122 121 3imp ⊢ V ∈ ℕ 0 ∧ V ∈ Fin ∧ G ∈ FriendGraph → ¬ V = 0 → ¬ V = 1 → ¬ V = 3 → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
123 122 com25 ⊢ V ∈ ℕ 0 ∧ V ∈ Fin ∧ G ∈ FriendGraph → G RegUSGraph K → ¬ V = 1 → ¬ V = 3 → ¬ V = 0 → V = 0 ∨ V = 1 ∨ V = 3
124 123 imp ⊢ V ∈ ℕ 0 ∧ V ∈ Fin ∧ G ∈ FriendGraph ∧ G RegUSGraph K → ¬ 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 ∧ G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
126 125 3imp ⊢ ¬ V = 0 ∧ ¬ V = 1 ∧ ¬ V = 3 → V ∈ ℕ 0 ∧ V ∈ Fin ∧ G ∈ FriendGraph ∧ G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
127 4 126 sylbi ⊢ ¬ V = 0 ∨ V = 1 ∨ V = 3 → V ∈ ℕ 0 ∧ V ∈ Fin ∧ G ∈ FriendGraph ∧ G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
128 3 127 pm2.61i ⊢ V ∈ ℕ 0 ∧ V ∈ Fin ∧ G ∈ FriendGraph ∧ G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
129 128 3exp1 ⊢ V ∈ ℕ 0 → V ∈ Fin → G ∈ FriendGraph → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
130 2 129 mpcom ⊢ V ∈ Fin → G ∈ FriendGraph → G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
131 130 3imp21 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3