Theorem frcond1

Description: The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 29-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		frcond1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		frcond1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	isfrgr	⊢ ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑘 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 ) )
4		preq2	⊢ ( 𝑘 = 𝐴 → { 𝑏 , 𝑘 } = { 𝑏 , 𝐴 } )
5	4	preq1d	⊢ ( 𝑘 = 𝐴 → { { 𝑏 , 𝑘 } , { 𝑏 , 𝑙 } } = { { 𝑏 , 𝐴 } , { 𝑏 , 𝑙 } } )
6	5	sseq1d	⊢ ( 𝑘 = 𝐴 → ( { { 𝑏 , 𝑘 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑏 , 𝐴 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 ) )
7	6	reubidv	⊢ ( 𝑘 = 𝐴 → ( ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑘 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝐴 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 ) )
8		preq2	⊢ ( 𝑙 = 𝐶 → { 𝑏 , 𝑙 } = { 𝑏 , 𝐶 } )
9	8	preq2d	⊢ ( 𝑙 = 𝐶 → { { 𝑏 , 𝐴 } , { 𝑏 , 𝑙 } } = { { 𝑏 , 𝐴 } , { 𝑏 , 𝐶 } } )
10	9	sseq1d	⊢ ( 𝑙 = 𝐶 → ( { { 𝑏 , 𝐴 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 ↔ { { 𝑏 , 𝐴 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) )
11	10	reubidv	⊢ ( 𝑙 = 𝐶 → ( ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝐴 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 ↔ ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝐴 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) )
12		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ 𝑉 )
13		sneq	⊢ ( 𝑘 = 𝐴 → { 𝑘 } = { 𝐴 } )
14	13	difeq2d	⊢ ( 𝑘 = 𝐴 → ( 𝑉 ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝐴 } ) )
15	14	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑘 = 𝐴 ) → ( 𝑉 ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝐴 } ) )
16		necom	⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
17	16	biimpi	⊢ ( 𝐴 ≠ 𝐶 → 𝐶 ≠ 𝐴 )
18	17	anim2i	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐴 ) )
19	18	3adant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐴 ) )
20		eldifsn	⊢ ( 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) ↔ ( 𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐴 ) )
21	19 20	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) )
22	7 11 12 15 21	rspc2vd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑘 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 → ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝐴 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) )
23		prcom	⊢ { 𝑏 , 𝐴 } = { 𝐴 , 𝑏 }
24	23	preq1i	⊢ { { 𝑏 , 𝐴 } , { 𝑏 , 𝐶 } } = { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } }
25	24	sseq1i	⊢ ( { { 𝑏 , 𝐴 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ↔ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 )
26	25	reubii	⊢ ( ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝐴 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ↔ ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 )
27	26	biimpi	⊢ ( ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝐴 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 → ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 )
28	22 27	syl6com	⊢ ( ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑏 ∈ 𝑉 { { 𝑏 , 𝑘 } , { 𝑏 , 𝑙 } } ⊆ 𝐸 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) )
29	3 28	simplbiim	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) )