Theorem frgreu

Description: Variant of frcond2 : Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021) (Proof shortened by AV, 4-Jan-2022)

	Ref	Expression
Hypotheses	frcond1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	frcond1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	frgreu	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frcond1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frcond1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	frcond2	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
4	3	imp	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ∃! 𝑏 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) )
5		frgrusgr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
6	5	adantr	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → 𝐺 ∈ USGraph )
7		simpl	⊢ ( ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) → { 𝐴 , 𝑏 } ∈ 𝐸 )
8	2 1	usgrpredgv	⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ) → ( 𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
9	8	simprd	⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝐴 , 𝑏 } ∈ 𝐸 ) → 𝑏 ∈ 𝑉 )
10	6 7 9	syl2an	⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) → 𝑏 ∈ 𝑉 )
11	10	reueubd	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ( ∃! 𝑏 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ↔ ∃! 𝑏 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )
12	4 11	mpbid	⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ∃! 𝑏 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) )
13	12	ex	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ) )