Theorem frgrwopreg2

Description: According to statement 5 in Huneke p. 2: "If ... B 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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frgrwopreg.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
	frgrwopreg.a	⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
	frgrwopreg.b	⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
	frgrwopreg.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	frgrwopreg2	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )

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	frgrwopreglem1	⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V )
7	6	simpri	⊢ 𝐵 ∈ V
8		hash1snb	⊢ ( 𝐵 ∈ V → ( ( ♯ ‘ 𝐵 ) = 1 ↔ ∃ 𝑣 𝐵 = { 𝑣 } ) )
9	7 8	ax-mp	⊢ ( ( ♯ ‘ 𝐵 ) = 1 ↔ ∃ 𝑣 𝐵 = { 𝑣 } )
10		exsnrex	⊢ ( ∃ 𝑣 𝐵 = { 𝑣 } ↔ ∃ 𝑣 ∈ 𝐵 𝐵 = { 𝑣 } )
11		difss	⊢ ( 𝑉 ∖ 𝐴 ) ⊆ 𝑉
12	4 11	eqsstri	⊢ 𝐵 ⊆ 𝑉
13		ssrexv	⊢ ( 𝐵 ⊆ 𝑉 → ( ∃ 𝑣 ∈ 𝐵 𝐵 = { 𝑣 } → ∃ 𝑣 ∈ 𝑉 𝐵 = { 𝑣 } ) )
14	12 13	ax-mp	⊢ ( ∃ 𝑣 ∈ 𝐵 𝐵 = { 𝑣 } → ∃ 𝑣 ∈ 𝑉 𝐵 = { 𝑣 } )
15	1 2 3 4 5	frgrwopregbsn	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉 ∧ 𝐵 = { 𝑣 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )
16	15	3expia	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉 ) → ( 𝐵 = { 𝑣 } → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
17	16	reximdva	⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑣 ∈ 𝑉 𝐵 = { 𝑣 } → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
18	14 17	syl5com	⊢ ( ∃ 𝑣 ∈ 𝐵 𝐵 = { 𝑣 } → ( 𝐺 ∈ FriendGraph → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
19	10 18	sylbi	⊢ ( ∃ 𝑣 𝐵 = { 𝑣 } → ( 𝐺 ∈ FriendGraph → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
20	19	com12	⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑣 𝐵 = { 𝑣 } → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
21	9 20	biimtrid	⊢ ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝐵 ) = 1 → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
22	21	imp	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )