Metamath Proof Explorer

Theorem frgrwopregasn

Description: According to statement 5 in Huneke p. 2: "If A ... is a singleton, then that singleton is a universal friend". This version of frgrwopreg1 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by Alexander van der Vekens, 1-Jan-2018) (Revised 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 frgrwopregasn ⊢ G ∈ FriendGraph ∧ X ∈ V ∧ A = X → ∀ w ∈ V ∖ X X 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 5 frgrwopreglem4 ⊢ G ∈ FriendGraph → ∀ v ∈ A ∀ w ∈ B v w ∈ E
7 snidg ⊢ X ∈ V → X ∈ X
8 7 adantr ⊢ X ∈ V ∧ A = X → X ∈ X
9 eleq2 ⊢ A = X → X ∈ A ↔ X ∈ X
10 9 adantl ⊢ X ∈ V ∧ A = X → X ∈ A ↔ X ∈ X
11 8 10 mpbird ⊢ X ∈ V ∧ A = X → X ∈ A
12 preq1 ⊢ v = X → v w = X w
13 12 eleq1d ⊢ v = X → v w ∈ E ↔ X w ∈ E
14 13 ralbidv ⊢ v = X → ∀ w ∈ B v w ∈ E ↔ ∀ w ∈ B X w ∈ E
15 14 rspcv ⊢ X ∈ A → ∀ v ∈ A ∀ w ∈ B v w ∈ E → ∀ w ∈ B X w ∈ E
16 11 15 syl ⊢ X ∈ V ∧ A = X → ∀ v ∈ A ∀ w ∈ B v w ∈ E → ∀ w ∈ B X w ∈ E
17 difeq2 ⊢ A = X → V ∖ A = V ∖ X
18 4 17 eqtrid ⊢ A = X → B = V ∖ X
19 18 adantl ⊢ X ∈ V ∧ A = X → B = V ∖ X
20 19 raleqdv ⊢ X ∈ V ∧ A = X → ∀ w ∈ B X w ∈ E ↔ ∀ w ∈ V ∖ X X w ∈ E
21 16 20 sylibd ⊢ X ∈ V ∧ A = X → ∀ v ∈ A ∀ w ∈ B v w ∈ E → ∀ w ∈ V ∖ X X w ∈ E
22 6 21 syl5com ⊢ G ∈ FriendGraph → X ∈ V ∧ A = X → ∀ w ∈ V ∖ X X w ∈ E
23 22 3impib ⊢ G ∈ FriendGraph ∧ X ∈ V ∧ A = X → ∀ w ∈ V ∖ X X w ∈ E