Theorem frgrncvvdeqlem7

Description: Lemma 7 for frgrncvvdeq . This corresponds to statement 1 in Huneke p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021)

	Ref	Expression
Hypotheses	frgrncvvdeq.v1	|- V = ( Vtx ` G )
	frgrncvvdeq.e	|- E = ( Edg ` G )
	frgrncvvdeq.nx	|- D = ( G NeighbVtx X )
	frgrncvvdeq.ny	|- N = ( G NeighbVtx Y )
	frgrncvvdeq.x	|- ( ph -> X e. V )
	frgrncvvdeq.y	|- ( ph -> Y e. V )
	frgrncvvdeq.ne	|- ( ph -> X =/= Y )
	frgrncvvdeq.xy	|- ( ph -> Y e/ D )
	frgrncvvdeq.f	|- ( ph -> G e. FriendGraph )
	frgrncvvdeq.a	|- A = ( x e. D |-> ( iota_ y e. N { x , y } e. E ) )
Assertion	frgrncvvdeqlem7	|- ( ph -> A. x e. D ( A ` x ) =/= X )

Proof

Step	Hyp	Ref	Expression
1		frgrncvvdeq.v1	|- V = ( Vtx ` G )
2		frgrncvvdeq.e	|- E = ( Edg ` G )
3		frgrncvvdeq.nx	|- D = ( G NeighbVtx X )
4		frgrncvvdeq.ny	|- N = ( G NeighbVtx Y )
5		frgrncvvdeq.x	|- ( ph -> X e. V )
6		frgrncvvdeq.y	|- ( ph -> Y e. V )
7		frgrncvvdeq.ne	|- ( ph -> X =/= Y )
8		frgrncvvdeq.xy	|- ( ph -> Y e/ D )
9		frgrncvvdeq.f	|- ( ph -> G e. FriendGraph )
10		frgrncvvdeq.a	|- A = ( x e. D |-> ( iota_ y e. N { x , y } e. E ) )
11	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem5	|- ( ( ph /\ x e. D ) -> { ( A ` x ) } = ( ( G NeighbVtx x ) i^i N ) )
12		fvex	|- ( A ` x ) e. _V
13	12	snid	|- ( A ` x ) e. { ( A ` x ) }
14		eleq2	|- ( { ( A ` x ) } = ( ( G NeighbVtx x ) i^i N ) -> ( ( A ` x ) e. { ( A ` x ) } <-> ( A ` x ) e. ( ( G NeighbVtx x ) i^i N ) ) )
15	14	biimpa	|- ( ( { ( A ` x ) } = ( ( G NeighbVtx x ) i^i N ) /\ ( A ` x ) e. { ( A ` x ) } ) -> ( A ` x ) e. ( ( G NeighbVtx x ) i^i N ) )
16		elin	|- ( ( A ` x ) e. ( ( G NeighbVtx x ) i^i N ) <-> ( ( A ` x ) e. ( G NeighbVtx x ) /\ ( A ` x ) e. N ) )
17	1 2 3 4 5 6 7 8 9 10	frgrncvvdeqlem1	|- ( ph -> X e/ N )
18		df-nel	|- ( X e/ N <-> -. X e. N )
19		nelelne	|- ( -. X e. N -> ( ( A ` x ) e. N -> ( A ` x ) =/= X ) )
20	18 19	sylbi	|- ( X e/ N -> ( ( A ` x ) e. N -> ( A ` x ) =/= X ) )
21	17 20	syl	|- ( ph -> ( ( A ` x ) e. N -> ( A ` x ) =/= X ) )
22	21	adantr	|- ( ( ph /\ x e. D ) -> ( ( A ` x ) e. N -> ( A ` x ) =/= X ) )
23	22	com12	|- ( ( A ` x ) e. N -> ( ( ph /\ x e. D ) -> ( A ` x ) =/= X ) )
24	16 23	simplbiim	|- ( ( A ` x ) e. ( ( G NeighbVtx x ) i^i N ) -> ( ( ph /\ x e. D ) -> ( A ` x ) =/= X ) )
25	15 24	syl	|- ( ( { ( A ` x ) } = ( ( G NeighbVtx x ) i^i N ) /\ ( A ` x ) e. { ( A ` x ) } ) -> ( ( ph /\ x e. D ) -> ( A ` x ) =/= X ) )
26	13 25	mpan2	|- ( { ( A ` x ) } = ( ( G NeighbVtx x ) i^i N ) -> ( ( ph /\ x e. D ) -> ( A ` x ) =/= X ) )
27	11 26	mpcom	|- ( ( ph /\ x e. D ) -> ( A ` x ) =/= X )
28	27	ralrimiva	|- ( ph -> A. x e. D ( A ` x ) =/= X )