Theorem 1to3vfriendship

Description: The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017) (Revised by AV, 31-Mar-2021)

	Ref	Expression
Hypotheses	3vfriswmgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	3vfriswmgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	1to3vfriendship	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		3vfriswmgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		3vfriswmgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	1to3vfriswmgr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) ( { 𝑤 , 𝑣 } ∈ 𝐸 ∧ ∃! 𝑥 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑤 , 𝑥 } ∈ 𝐸 ) ) )
4		prcom	⊢ { 𝑤 , 𝑣 } = { 𝑣 , 𝑤 }
5	4	eleq1i	⊢ ( { 𝑤 , 𝑣 } ∈ 𝐸 ↔ { 𝑣 , 𝑤 } ∈ 𝐸 )
6	5	biimpi	⊢ ( { 𝑤 , 𝑣 } ∈ 𝐸 → { 𝑣 , 𝑤 } ∈ 𝐸 )
7	6	adantr	⊢ ( ( { 𝑤 , 𝑣 } ∈ 𝐸 ∧ ∃! 𝑥 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑤 , 𝑥 } ∈ 𝐸 ) → { 𝑣 , 𝑤 } ∈ 𝐸 )
8	7	ralimi	⊢ ( ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) ( { 𝑤 , 𝑣 } ∈ 𝐸 ∧ ∃! 𝑥 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑤 , 𝑥 } ∈ 𝐸 ) → ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )
9	8	reximi	⊢ ( ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) ( { 𝑤 , 𝑣 } ∈ 𝐸 ∧ ∃! 𝑥 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑤 , 𝑥 } ∈ 𝐸 ) → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 )
10	3 9	syl6	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑉 = { 𝐴 } ∨ 𝑉 = { 𝐴 , 𝐵 } ∨ 𝑉 = { 𝐴 , 𝐵 , 𝐶 } ) ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) )