Metamath Proof Explorer

Theorem frgrwopreg2

Description: According to statement 5 in Huneke p. 2: "If ... B is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018) (Proof shortened by AV, 4-Feb-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
frgrwopreg.e ⊢ E = Edg ⁡ G
Assertion frgrwopreg2 ⊢ G ∈ FriendGraph ∧ B = 1 → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E

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 frgrwopreg.e ⊢ E = Edg ⁡ G
6 1 2 3 4 frgrwopreglem1 ⊢ A ∈ V ∧ B ∈ V
7 6 simpri ⊢ B ∈ V
8 hash1snb ⊢ B ∈ V → B = 1 ↔ ∃ v B = v
9 7 8 ax-mp ⊢ B = 1 ↔ ∃ v B = v
10 exsnrex ⊢ ∃ v B = v ↔ ∃ v ∈ B B = v
11 difss ⊢ V ∖ A ⊆ V
12 4 11 eqsstri ⊢ B ⊆ V
13 ssrexv ⊢ B ⊆ V → ∃ v ∈ B B = v → ∃ v ∈ V B = v
14 12 13 ax-mp ⊢ ∃ v ∈ B B = v → ∃ v ∈ V B = v
15 1 2 3 4 5 frgrwopregbsn ⊢ G ∈ FriendGraph ∧ v ∈ V ∧ B = v → ∀ w ∈ V ∖ v v w ∈ E
16 15 3expia ⊢ G ∈ FriendGraph ∧ v ∈ V → B = v → ∀ w ∈ V ∖ v v w ∈ E
17 16 reximdva ⊢ G ∈ FriendGraph → ∃ v ∈ V B = v → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
18 14 17 syl5com ⊢ ∃ v ∈ B B = v → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
19 10 18 sylbi ⊢ ∃ v B = v → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
20 19 com12 ⊢ G ∈ FriendGraph → ∃ v B = v → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
21 9 20 biimtrid ⊢ G ∈ FriendGraph → B = 1 → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
22 21 imp ⊢ G ∈ FriendGraph ∧ B = 1 → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E