Metamath Proof Explorer

Theorem frgrwopreg1

Description: According to statement 5 in Huneke p. 2: "If A ... 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 frgrwopreg1 ⊢ G ∈ FriendGraph ∧ A = 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 fvexi ⊢ V ∈ V
7 3 6 rabex2 ⊢ A ∈ V
8 hash1snb ⊢ A ∈ V → A = 1 ↔ ∃ v A = v
9 7 8 ax-mp ⊢ A = 1 ↔ ∃ v A = v
10 exsnrex ⊢ ∃ v A = v ↔ ∃ v ∈ A A = v
11 3 ssrab3 ⊢ A ⊆ V
12 ssrexv ⊢ A ⊆ V → ∃ v ∈ A A = v → ∃ v ∈ V A = v
13 11 12 ax-mp ⊢ ∃ v ∈ A A = v → ∃ v ∈ V A = v
14 1 2 3 4 5 frgrwopregasn ⊢ G ∈ FriendGraph ∧ v ∈ V ∧ A = v → ∀ w ∈ V ∖ v v w ∈ E
15 14 3expia ⊢ G ∈ FriendGraph ∧ v ∈ V → A = v → ∀ w ∈ V ∖ v v w ∈ E
16 15 reximdva ⊢ G ∈ FriendGraph → ∃ v ∈ V A = v → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
17 13 16 syl5com ⊢ ∃ v ∈ A A = v → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
18 10 17 sylbi ⊢ ∃ v A = v → G ∈ FriendGraph → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
19 18 com12 ⊢ G ∈ FriendGraph → ∃ v A = v → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
20 9 19 syl5bi ⊢ G ∈ FriendGraph → A = 1 → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E
21 20 imp ⊢ G ∈ FriendGraph ∧ A = 1 → ∃ v ∈ V ∀ w ∈ V ∖ v v w ∈ E