Theorem frgrwopregbsn

Description: According to statement 5 in Huneke p. 2: "If ... B is a singleton, then that singleton is a universal friend". This version of frgrwopreg2 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 AV, 4-Feb-2022)

	Ref	Expression
Hypotheses	frgrwopreg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrwopreg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
	frgrwopreg.a	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
	frgrwopreg.b	⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
	frgrwopreg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	frgrwopregbsn	⊢ ( ( 𝐺 ∈ 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		ralcom	⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 { 𝑤 , 𝑣 } ∈ 𝐸 ↔ ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐴 { 𝑤 , 𝑣 } ∈ 𝐸 )
8		snidg	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
9	8	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → 𝑋 ∈ { 𝑋 } )
10		eleq2	⊢ ( 𝐵 = { 𝑋 } → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ { 𝑋 } ) )
11	10	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ { 𝑋 } ) )
12	9 11	mpbird	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → 𝑋 ∈ 𝐵 )
13		preq2	⊢ ( 𝑣 = 𝑋 → { 𝑤 , 𝑣 } = { 𝑤 , 𝑋 } )
14		prcom	⊢ { 𝑤 , 𝑋 } = { 𝑋 , 𝑤 }
15	13 14	eqtrdi	⊢ ( 𝑣 = 𝑋 → { 𝑤 , 𝑣 } = { 𝑋 , 𝑤 } )
16	15	eleq1d	⊢ ( 𝑣 = 𝑋 → ( { 𝑤 , 𝑣 } ∈ 𝐸 ↔ { 𝑋 , 𝑤 } ∈ 𝐸 ) )
17	16	ralbidv	⊢ ( 𝑣 = 𝑋 → ( ∀ 𝑤 ∈ 𝐴 { 𝑤 , 𝑣 } ∈ 𝐸 ↔ ∀ 𝑤 ∈ 𝐴 { 𝑋 , 𝑤 } ∈ 𝐸 ) )
18	17	rspcv	⊢ ( 𝑋 ∈ 𝐵 → ( ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐴 { 𝑤 , 𝑣 } ∈ 𝐸 → ∀ 𝑤 ∈ 𝐴 { 𝑋 , 𝑤 } ∈ 𝐸 ) )
19	12 18	syl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → ( ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐴 { 𝑤 , 𝑣 } ∈ 𝐸 → ∀ 𝑤 ∈ 𝐴 { 𝑋 , 𝑤 } ∈ 𝐸 ) )
20	3	ssrab3	⊢ 𝐴 ⊆ 𝑉
21		ssdifim	⊢ ( ( 𝐴 ⊆ 𝑉 ∧ 𝐵 = ( 𝑉 ∖ 𝐴 ) ) → 𝐴 = ( 𝑉 ∖ 𝐵 ) )
22	20 4 21	mp2an	⊢ 𝐴 = ( 𝑉 ∖ 𝐵 )
23		difeq2	⊢ ( 𝐵 = { 𝑋 } → ( 𝑉 ∖ 𝐵 ) = ( 𝑉 ∖ { 𝑋 } ) )
24	23	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → ( 𝑉 ∖ 𝐵 ) = ( 𝑉 ∖ { 𝑋 } ) )
25	22 24	syl5eq	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → 𝐴 = ( 𝑉 ∖ { 𝑋 } ) )
26	25	raleqdv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → ( ∀ 𝑤 ∈ 𝐴 { 𝑋 , 𝑤 } ∈ 𝐸 ↔ ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
27	19 26	sylibd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → ( ∀ 𝑣 ∈ 𝐵 ∀ 𝑤 ∈ 𝐴 { 𝑤 , 𝑣 } ∈ 𝐸 → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
28	7 27	syl5bi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 { 𝑤 , 𝑣 } ∈ 𝐸 → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
29	6 28	syl5com	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 ) )
30	29	3impib	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝐵 = { 𝑋 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑋 } ) { 𝑋 , 𝑤 } ∈ 𝐸 )