Theorem frgrwopreg1

Description: According to statement 5 in Huneke p. 2: "If A ... 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	frgrwopreg1	⊢ ( ( 𝐺 ∈ 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	fvexi	⊢ 𝑉 ∈ V
7	3 6	rabex2	⊢ 𝐴 ∈ V
8		hash1snb	⊢ ( 𝐴 ∈ V → ( ( ♯ ‘ 𝐴 ) = 1 ↔ ∃ 𝑣 𝐴 = { 𝑣 } ) )
9	7 8	ax-mp	⊢ ( ( ♯ ‘ 𝐴 ) = 1 ↔ ∃ 𝑣 𝐴 = { 𝑣 } )
10		exsnrex	⊢ ( ∃ 𝑣 𝐴 = { 𝑣 } ↔ ∃ 𝑣 ∈ 𝐴 𝐴 = { 𝑣 } )
11	3	ssrab3	⊢ 𝐴 ⊆ 𝑉
12		ssrexv	⊢ ( 𝐴 ⊆ 𝑉 → ( ∃ 𝑣 ∈ 𝐴 𝐴 = { 𝑣 } → ∃ 𝑣 ∈ 𝑉 𝐴 = { 𝑣 } ) )
13	11 12	ax-mp	⊢ ( ∃ 𝑣 ∈ 𝐴 𝐴 = { 𝑣 } → ∃ 𝑣 ∈ 𝑉 𝐴 = { 𝑣 } )
14	1 2 3 4 5	frgrwopregasn	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉 ∧ 𝐴 = { 𝑣 } ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )
15	14	3expia	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑣 ∈ 𝑉 ) → ( 𝐴 = { 𝑣 } → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
16	15	reximdva	⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑣 ∈ 𝑉 𝐴 = { 𝑣 } → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
17	13 16	syl5com	⊢ ( ∃ 𝑣 ∈ 𝐴 𝐴 = { 𝑣 } → ( 𝐺 ∈ FriendGraph → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
18	10 17	sylbi	⊢ ( ∃ 𝑣 𝐴 = { 𝑣 } → ( 𝐺 ∈ FriendGraph → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
19	18	com12	⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑣 𝐴 = { 𝑣 } → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
20	9 19	biimtrid	⊢ ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝐴 ) = 1 → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )
21	20	imp	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ♯ ‘ 𝐴 ) = 1 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )