Metamath Proof Explorer

Theorem frgrregord13

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

Ref Expression
Hypothesis frgrreggt1.v ⊢ V = Vtx ⁡ G
Assertion frgrregord13 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V = 1 ∨ V = 3

Proof

Step Hyp Ref Expression
1 frgrreggt1.v ⊢ V = Vtx ⁡ G
2 simpl1 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → G ∈ FriendGraph
3 simpl2 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V ∈ Fin
4 simpr ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → G RegUSGraph K
5 1 frgrregord013 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
6 2 3 4 5 syl3anc ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V = 0 ∨ V = 1 ∨ V = 3
7 hasheq0 ⊢ V ∈ Fin → V = 0 ↔ V = ∅
8 eqneqall ⊢ V = ∅ → V ≠ ∅ → V = 1 ∨ V = 3
9 7 8 syl6bi ⊢ V ∈ Fin → V = 0 → V ≠ ∅ → V = 1 ∨ V = 3
10 9 com23 ⊢ V ∈ Fin → V ≠ ∅ → V = 0 → V = 1 ∨ V = 3
11 10 a1i ⊢ G ∈ FriendGraph → V ∈ Fin → V ≠ ∅ → V = 0 → V = 1 ∨ V = 3
12 11 3imp ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → V = 0 → V = 1 ∨ V = 3
13 12 adantr ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V = 0 → V = 1 ∨ V = 3
14 13 com12 ⊢ V = 0 → G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V = 1 ∨ V = 3
15 orc ⊢ V = 1 → V = 1 ∨ V = 3
16 15 a1d ⊢ V = 1 → G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V = 1 ∨ V = 3
17 olc ⊢ V = 3 → V = 1 ∨ V = 3
18 17 a1d ⊢ V = 3 → G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V = 1 ∨ V = 3
19 14 16 18 3jaoi ⊢ V = 0 ∨ V = 1 ∨ V = 3 → G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V = 1 ∨ V = 3
20 6 19 mpcom ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ G RegUSGraph K → V = 1 ∨ V = 3