Theorem frgrncvvdeqlem6

Description: Lemma 6 for frgrncvvdeq . (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 30-Dec-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	frgrncvvdeqlem6	|- ( ( ph /\ x e. D ) -> { x , ( A ` x ) } e. E )

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		elinsn	|- ( ( ( A ` x ) e. _V /\ ( ( G NeighbVtx x ) i^i N ) = { ( A ` x ) } ) -> ( ( A ` x ) e. ( G NeighbVtx x ) /\ ( A ` x ) e. N ) )
14	12 13	mpan	|- ( ( ( G NeighbVtx x ) i^i N ) = { ( A ` x ) } -> ( ( A ` x ) e. ( G NeighbVtx x ) /\ ( A ` x ) e. N ) )
15		frgrusgr	|- ( G e. FriendGraph -> G e. USGraph )
16	2	nbusgreledg	|- ( G e. USGraph -> ( ( A ` x ) e. ( G NeighbVtx x ) <-> { ( A ` x ) , x } e. E ) )
17		prcom	|- { ( A ` x ) , x } = { x , ( A ` x ) }
18	17	eleq1i	|- ( { ( A ` x ) , x } e. E <-> { x , ( A ` x ) } e. E )
19	16 18	bitrdi	|- ( G e. USGraph -> ( ( A ` x ) e. ( G NeighbVtx x ) <-> { x , ( A ` x ) } e. E ) )
20	19	biimpd	|- ( G e. USGraph -> ( ( A ` x ) e. ( G NeighbVtx x ) -> { x , ( A ` x ) } e. E ) )
21	9 15 20	3syl	|- ( ph -> ( ( A ` x ) e. ( G NeighbVtx x ) -> { x , ( A ` x ) } e. E ) )
22	21	adantr	|- ( ( ph /\ x e. D ) -> ( ( A ` x ) e. ( G NeighbVtx x ) -> { x , ( A ` x ) } e. E ) )
23	22	com12	|- ( ( A ` x ) e. ( G NeighbVtx x ) -> ( ( ph /\ x e. D ) -> { x , ( A ` x ) } e. E ) )
24	23	adantr	|- ( ( ( A ` x ) e. ( G NeighbVtx x ) /\ ( A ` x ) e. N ) -> ( ( ph /\ x e. D ) -> { x , ( A ` x ) } e. E ) )
25	14 24	syl	|- ( ( ( G NeighbVtx x ) i^i N ) = { ( A ` x ) } -> ( ( ph /\ x e. D ) -> { x , ( A ` x ) } e. E ) )
26	25	eqcoms	|- ( { ( A ` x ) } = ( ( G NeighbVtx x ) i^i N ) -> ( ( ph /\ x e. D ) -> { x , ( A ` x ) } e. E ) )
27	11 26	mpcom	|- ( ( ph /\ x e. D ) -> { x , ( A ` x ) } e. E )