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	eqtrid	⊢ ( 𝐴 = { 𝑋 } → 𝐵 = ( 𝑉 ∖ { 𝑋 } ) )
19	18	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 = { 𝑋 } ) → 𝐵 = ( 𝑉 ∖ { 𝑋 } ) )
20	19	raleqdv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 = { 𝑋 } ) → ( ∀ 𝑤 ∈ 𝐵 { 𝑋 , 𝑤 } ∈ 𝐸 ↔ ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
21	16 20	sylibd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 = { 𝑋 } ) → ( ∀ 𝑣 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 { 𝑣 , 𝑤 } ∈ 𝐸 → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
22	6 21	syl5com	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 = { 𝑋 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
23	22	3impib	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝐴 = { 𝑋 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 )