Metamath Proof Explorer

Theorem frgrwopreglem2

Description: Lemma 2 for frgrwopreg . If the set A of vertices of degree K is not empty in a friendship graph with at least two vertices, then K must be greater than 1 . This is only an observation, which is not required for the proof the friendship theorem. (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 2-Jan-2022)

Ref Expression
Hypotheses frgrwopreg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgrwopreg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
frgrwopreg.a ⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
frgrwopreg.b ⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
Assertion frgrwopreglem2 ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ≠ ∅ ) → 2 ≤ 𝐾 )

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrwopreg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3 frgrwopreg.a ⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
4 frgrwopreg.b ⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
5 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
6 3 reqabi ⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) )
7 1 vdgfrgrgt2 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑥 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) )
8 7 imp ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑥 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
9 breq2 ⊢ ( 𝐾 = ( 𝐷 ‘ 𝑥 ) → ( 2 ≤ 𝐾 ↔ 2 ≤ ( 𝐷 ‘ 𝑥 ) ) )
10 2 fveq1i ⊢ ( 𝐷 ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 )
11 10 breq2i ⊢ ( 2 ≤ ( 𝐷 ‘ 𝑥 ) ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) )
12 9 11 bitrdi ⊢ ( 𝐾 = ( 𝐷 ‘ 𝑥 ) → ( 2 ≤ 𝐾 ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) )
13 12 eqcoms ⊢ ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → ( 2 ≤ 𝐾 ↔ 2 ≤ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) )
14 8 13 syl5ibrcom ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑥 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → 2 ≤ 𝐾 ) )
15 14 exp31 ⊢ ( 𝐺 ∈ FriendGraph → ( 𝑥 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → 2 ≤ 𝐾 ) ) ) )
16 15 com14 ⊢ ( ( 𝐷 ‘ 𝑥 ) = 𝐾 → ( 𝑥 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) ) )
17 16 impcom ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑥 ) = 𝐾 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) )
18 6 17 sylbi ⊢ ( 𝑥 ∈ 𝐴 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) )
19 18 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) )
20 5 19 sylbi ⊢ ( 𝐴 ≠ ∅ → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → 2 ≤ 𝐾 ) ) )
21 20 3imp31 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ≠ ∅ ) → 2 ≤ 𝐾 )