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≠∅∧GRegUSGraphK→V=1∨V=3

Proof

Step Hyp Ref Expression
1 frgrreggt1.v ⊢V=Vtx⁡G
2 simpl1 ⊢G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→G∈FriendGraph
3 simpl2 ⊢G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→V∈Fin
4 simpr ⊢G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→GRegUSGraphK
5 1 frgrregord013 ⊢G∈FriendGraph∧V∈Fin∧GRegUSGraphK→V=0∨V=1∨V=3
6 2 3 4 5 syl3anc ⊢G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→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≠∅∧GRegUSGraphK→V=0→V=1∨V=3
14 13 com12 ⊢V=0→G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→V=1∨V=3
15 orc ⊢V=1→V=1∨V=3
16 15 a1d ⊢V=1→G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→V=1∨V=3
17 olc ⊢V=3→V=1∨V=3
18 17 a1d ⊢V=3→G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→V=1∨V=3
19 14 16 18 3jaoi ⊢V=0∨V=1∨V=3→G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→V=1∨V=3
20 6 19 mpcom ⊢G∈FriendGraph∧V∈Fin∧V≠∅∧GRegUSGraphK→V=1∨V=3