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 ⊢V=Vtx⁡G
frgrwopreg.d ⊢D=VtxDeg⁡G
frgrwopreg.a ⊢A=x∈V|D⁡x=K
frgrwopreg.b ⊢B=V∖A
Assertion frgrwopreglem2 ⊢G∈FriendGraph∧1<V∧A≠∅→2≤K

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢V=Vtx⁡G
2 frgrwopreg.d ⊢D=VtxDeg⁡G
3 frgrwopreg.a ⊢A=x∈V|D⁡x=K
4 frgrwopreg.b ⊢B=V∖A
5 n0 ⊢A≠∅↔∃xx∈A
6 3 reqabi ⊢x∈A↔x∈V∧D⁡x=K
7 1 vdgfrgrgt2 ⊢G∈FriendGraph∧x∈V→1<V→2≤VtxDeg⁡G⁡x
8 7 imp ⊢G∈FriendGraph∧x∈V∧1<V→2≤VtxDeg⁡G⁡x
9 breq2 ⊢K=D⁡x→2≤K↔2≤D⁡x
10 2 fveq1i ⊢D⁡x=VtxDeg⁡G⁡x
11 10 breq2i ⊢2≤D⁡x↔2≤VtxDeg⁡G⁡x
12 9 11 bitrdi ⊢K=D⁡x→2≤K↔2≤VtxDeg⁡G⁡x
13 12 eqcoms ⊢D⁡x=K→2≤K↔2≤VtxDeg⁡G⁡x
14 8 13 syl5ibrcom ⊢G∈FriendGraph∧x∈V∧1<V→D⁡x=K→2≤K
15 14 exp31 ⊢G∈FriendGraph→x∈V→1<V→D⁡x=K→2≤K
16 15 com14 ⊢D⁡x=K→x∈V→1<V→G∈FriendGraph→2≤K
17 16 impcom ⊢x∈V∧D⁡x=K→1<V→G∈FriendGraph→2≤K
18 6 17 sylbi ⊢x∈A→1<V→G∈FriendGraph→2≤K
19 18 exlimiv ⊢∃xx∈A→1<V→G∈FriendGraph→2≤K
20 5 19 sylbi ⊢A≠∅→1<V→G∈FriendGraph→2≤K
21 20 3imp31 ⊢G∈FriendGraph∧1<V∧A≠∅→2≤K