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 ≠ ∅ ↔ ∃ x x ∈ A
6 3 rabeq2i ⊢ 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 ⊢ ∃ x x ∈ 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