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 rabeq2i ( 𝑥𝐴 ↔ ( 𝑥𝑉 ∧ ( 𝐷𝑥 ) = 𝐾 ) )
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 ≤ 𝐾 )