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	|- V = ( Vtx ` G )
	frcond1.e	|- E = ( Edg ` G )
Assertion	frcond1	|- ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b e. V { { A , b } , { b , C } } C_ E ) )

Proof

Step	Hyp	Ref	Expression
1		frcond1.v	|- V = ( Vtx ` G )
2		frcond1.e	|- E = ( Edg ` G )
3	1 2	isfrgr	|- ( G e. FriendGraph <-> ( G e. USGraph /\ A. k e. V A. l e. ( V \ { k } ) E! b e. V { { b , k } , { b , l } } C_ E ) )
4		preq2	|- ( k = A -> { b , k } = { b , A } )
5	4	preq1d	|- ( k = A -> { { b , k } , { b , l } } = { { b , A } , { b , l } } )
6	5	sseq1d	|- ( k = A -> ( { { b , k } , { b , l } } C_ E <-> { { b , A } , { b , l } } C_ E ) )
7	6	reubidv	|- ( k = A -> ( E! b e. V { { b , k } , { b , l } } C_ E <-> E! b e. V { { b , A } , { b , l } } C_ E ) )
8		preq2	|- ( l = C -> { b , l } = { b , C } )
9	8	preq2d	|- ( l = C -> { { b , A } , { b , l } } = { { b , A } , { b , C } } )
10	9	sseq1d	|- ( l = C -> ( { { b , A } , { b , l } } C_ E <-> { { b , A } , { b , C } } C_ E ) )
11	10	reubidv	|- ( l = C -> ( E! b e. V { { b , A } , { b , l } } C_ E <-> E! b e. V { { b , A } , { b , C } } C_ E ) )
12		simp1	|- ( ( A e. V /\ C e. V /\ A =/= C ) -> A e. V )
13		sneq	|- ( k = A -> { k } = { A } )
14	13	difeq2d	|- ( k = A -> ( V \ { k } ) = ( V \ { A } ) )
15	14	adantl	|- ( ( ( A e. V /\ C e. V /\ A =/= C ) /\ k = A ) -> ( V \ { k } ) = ( V \ { A } ) )
16		necom	|- ( A =/= C <-> C =/= A )
17	16	biimpi	|- ( A =/= C -> C =/= A )
18	17	anim2i	|- ( ( C e. V /\ A =/= C ) -> ( C e. V /\ C =/= A ) )
19	18	3adant1	|- ( ( A e. V /\ C e. V /\ A =/= C ) -> ( C e. V /\ C =/= A ) )
20		eldifsn	|- ( C e. ( V \ { A } ) <-> ( C e. V /\ C =/= A ) )
21	19 20	sylibr	|- ( ( A e. V /\ C e. V /\ A =/= C ) -> C e. ( V \ { A } ) )
22	7 11 12 15 21	rspc2vd	|- ( ( A e. V /\ C e. V /\ A =/= C ) -> ( A. k e. V A. l e. ( V \ { k } ) E! b e. V { { b , k } , { b , l } } C_ E -> E! b e. V { { b , A } , { b , C } } C_ E ) )
23		prcom	|- { b , A } = { A , b }
24	23	preq1i	|- { { b , A } , { b , C } } = { { A , b } , { b , C } }
25	24	sseq1i	|- ( { { b , A } , { b , C } } C_ E <-> { { A , b } , { b , C } } C_ E )
26	25	reubii	|- ( E! b e. V { { b , A } , { b , C } } C_ E <-> E! b e. V { { A , b } , { b , C } } C_ E )
27	26	biimpi	|- ( E! b e. V { { b , A } , { b , C } } C_ E -> E! b e. V { { A , b } , { b , C } } C_ E )
28	22 27	syl6com	|- ( A. k e. V A. l e. ( V \ { k } ) E! b e. V { { b , k } , { b , l } } C_ E -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b e. V { { A , b } , { b , C } } C_ E ) )
29	3 28	simplbiim	|- ( G e. FriendGraph -> ( ( A e. V /\ C e. V /\ A =/= C ) -> E! b e. V { { A , b } , { b , C } } C_ E ) )