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 𝑉 = ( Vtx ‘ 𝐺 )
frgrwopreg.d 𝐷 = ( VtxDeg ‘ 𝐺 )
frgrwopreg.a 𝐴 = { 𝑥𝑉 ∣ ( 𝐷𝑥 ) = 𝐾 }
frgrwopreg.b 𝐵 = ( 𝑉𝐴 )
frgrwopreg.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion frgrwopregasn ( ( 𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝐴 = { 𝑋 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 frgrwopreg.v 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrwopreg.d 𝐷 = ( VtxDeg ‘ 𝐺 )
3 frgrwopreg.a 𝐴 = { 𝑥𝑉 ∣ ( 𝐷𝑥 ) = 𝐾 }
4 frgrwopreg.b 𝐵 = ( 𝑉𝐴 )
5 frgrwopreg.e 𝐸 = ( Edg ‘ 𝐺 )
6 1 2 3 4 5 frgrwopreglem4 ( 𝐺 ∈ FriendGraph → ∀ 𝑣𝐴𝑤𝐵 { 𝑣 , 𝑤 } ∈ 𝐸 )
7 snidg ( 𝑋𝑉𝑋 ∈ { 𝑋 } )
8 7 adantr ( ( 𝑋𝑉𝐴 = { 𝑋 } ) → 𝑋 ∈ { 𝑋 } )
9 eleq2 ( 𝐴 = { 𝑋 } → ( 𝑋𝐴𝑋 ∈ { 𝑋 } ) )
10 9 adantl ( ( 𝑋𝑉𝐴 = { 𝑋 } ) → ( 𝑋𝐴𝑋 ∈ { 𝑋 } ) )
11 8 10 mpbird ( ( 𝑋𝑉𝐴 = { 𝑋 } ) → 𝑋𝐴 )
12 preq1 ( 𝑣 = 𝑋 → { 𝑣 , 𝑤 } = { 𝑋 , 𝑤 } )
13 12 eleq1d ( 𝑣 = 𝑋 → ( { 𝑣 , 𝑤 } ∈ 𝐸 ↔ { 𝑋 , 𝑤 } ∈ 𝐸 ) )
14 13 ralbidv ( 𝑣 = 𝑋 → ( ∀ 𝑤𝐵 { 𝑣 , 𝑤 } ∈ 𝐸 ↔ ∀ 𝑤𝐵 { 𝑋 , 𝑤 } ∈ 𝐸 ) )
15 14 rspcv ( 𝑋𝐴 → ( ∀ 𝑣𝐴𝑤𝐵 { 𝑣 , 𝑤 } ∈ 𝐸 → ∀ 𝑤𝐵 { 𝑋 , 𝑤 } ∈ 𝐸 ) )
16 11 15 syl ( ( 𝑋𝑉𝐴 = { 𝑋 } ) → ( ∀ 𝑣𝐴𝑤𝐵 { 𝑣 , 𝑤 } ∈ 𝐸 → ∀ 𝑤𝐵 { 𝑋 , 𝑤 } ∈ 𝐸 ) )
17 difeq2 ( 𝐴 = { 𝑋 } → ( 𝑉𝐴 ) = ( 𝑉 ∖ { 𝑋 } ) )
18 4 17 syl5eq ( 𝐴 = { 𝑋 } → 𝐵 = ( 𝑉 ∖ { 𝑋 } ) )
19 18 adantl ( ( 𝑋𝑉𝐴 = { 𝑋 } ) → 𝐵 = ( 𝑉 ∖ { 𝑋 } ) )
20 19 raleqdv ( ( 𝑋𝑉𝐴 = { 𝑋 } ) → ( ∀ 𝑤𝐵 { 𝑋 , 𝑤 } ∈ 𝐸 ↔ ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
21 16 20 sylibd ( ( 𝑋𝑉𝐴 = { 𝑋 } ) → ( ∀ 𝑣𝐴𝑤𝐵 { 𝑣 , 𝑤 } ∈ 𝐸 → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
22 6 21 syl5com ( 𝐺 ∈ FriendGraph → ( ( 𝑋𝑉𝐴 = { 𝑋 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
23 22 3impib ( ( 𝐺 ∈ FriendGraph ∧ 𝑋𝑉𝐴 = { 𝑋 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 )