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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion frgrregord13 ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 RegUSGraph 𝐾 ) → ( ( ♯ ‘ 𝑉 ) = 1 ∨ ( ♯ ‘ 𝑉 ) = 3 ) )

Proof

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