Metamath Proof Explorer

Theorem frgrncvvdeqlem8

Description: Lemma 8 for frgrncvvdeq . This corresponds to statement 2 in Huneke p. 1: "The map is one-to-one since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021) (Revised 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 frgrncvvdeqlem8 
|- ( ph -> A : D -1-1-> N )

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 frgrncvvdeqlem4 
 |-  ( ph -> A : D --> N )
12 simpr 
 |-  ( ( ph /\ A : D --> N ) -> A : D --> N )
13 ffvelrn 
 |-  ( ( A : D --> N /\ u e. D ) -> ( A ` u ) e. N )
14 13 ad2ant2lr 
 |-  ( ( ( ph /\ A : D --> N ) /\ ( u e. D /\ w e. D ) ) -> ( A ` u ) e. N )
15 14 adantr 
 |-  ( ( ( ( ph /\ A : D --> N ) /\ ( u e. D /\ w e. D ) ) /\ ( A ` u ) = ( A ` w ) ) -> ( A ` u ) e. N )
16 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem1 
 |-  ( ph -> X e/ N )
17 preq1 
 |-  ( x = u -> { x , y } = { u , y } )
18 17 eleq1d 
 |-  ( x = u -> ( { x , y } e. E <-> { u , y } e. E ) )
19 18 riotabidv 
 |-  ( x = u -> ( iota_ y e. N { x , y } e. E ) = ( iota_ y e. N { u , y } e. E ) )
20 19 cbvmptv 
 |-  ( x e. D |-> ( iota_ y e. N { x , y } e. E ) ) = ( u e. D |-> ( iota_ y e. N { u , y } e. E ) )
21 10 20 eqtri 
 |-  A = ( u e. D |-> ( iota_ y e. N { u , y } e. E ) )
22 1 2 3 4 5 6 7 8 9 21 frgrncvvdeqlem6 
 |-  ( ( ph /\ u e. D ) -> { u , ( A ` u ) } e. E )
23 preq1 
 |-  ( x = w -> { x , y } = { w , y } )
24 23 eleq1d 
 |-  ( x = w -> ( { x , y } e. E <-> { w , y } e. E ) )
25 24 riotabidv 
 |-  ( x = w -> ( iota_ y e. N { x , y } e. E ) = ( iota_ y e. N { w , y } e. E ) )
26 25 cbvmptv 
 |-  ( x e. D |-> ( iota_ y e. N { x , y } e. E ) ) = ( w e. D |-> ( iota_ y e. N { w , y } e. E ) )
27 10 26 eqtri 
 |-  A = ( w e. D |-> ( iota_ y e. N { w , y } e. E ) )
28 1 2 3 4 5 6 7 8 9 27 frgrncvvdeqlem6 
 |-  ( ( ph /\ w e. D ) -> { w , ( A ` w ) } e. E )
29 22 28 anim12dan 
 |-  ( ( ph /\ ( u e. D /\ w e. D ) ) -> ( { u , ( A ` u ) } e. E /\ { w , ( A ` w ) } e. E ) )
30 preq2 
 |-  ( ( A ` w ) = ( A ` u ) -> { w , ( A ` w ) } = { w , ( A ` u ) } )
31 30 eleq1d 
 |-  ( ( A ` w ) = ( A ` u ) -> ( { w , ( A ` w ) } e. E <-> { w , ( A ` u ) } e. E ) )
32 31 anbi2d 
 |-  ( ( A ` w ) = ( A ` u ) -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` w ) } e. E ) <-> ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) ) )
33 32 eqcoms 
 |-  ( ( A ` u ) = ( A ` w ) -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` w ) } e. E ) <-> ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) ) )
34 33 biimpa 
 |-  ( ( ( A ` u ) = ( A ` w ) /\ ( { u , ( A ` u ) } e. E /\ { w , ( A ` w ) } e. E ) ) -> ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) )
35 df-ne 
 |-  ( u =/= w <-> -. u = w )
36 2 3 frgrnbnb 
 |-  ( ( G e. FriendGraph /\ ( u e. D /\ w e. D ) /\ u =/= w ) -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) -> ( A ` u ) = X ) )
37 9 36 syl3an1 
 |-  ( ( ph /\ ( u e. D /\ w e. D ) /\ u =/= w ) -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) -> ( A ` u ) = X ) )
38 37 3expa 
 |-  ( ( ( ph /\ ( u e. D /\ w e. D ) ) /\ u =/= w ) -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) -> ( A ` u ) = X ) )
39 df-nel 
 |-  ( X e/ N <-> -. X e. N )
40 eleq1 
 |-  ( ( A ` u ) = X -> ( ( A ` u ) e. N <-> X e. N ) )
41 40 biimpa 
 |-  ( ( ( A ` u ) = X /\ ( A ` u ) e. N ) -> X e. N )
42 41 pm2.24d 
 |-  ( ( ( A ` u ) = X /\ ( A ` u ) e. N ) -> ( -. X e. N -> u = w ) )
43 42 expcom 
 |-  ( ( A ` u ) e. N -> ( ( A ` u ) = X -> ( -. X e. N -> u = w ) ) )
44 43 com13 
 |-  ( -. X e. N -> ( ( A ` u ) = X -> ( ( A ` u ) e. N -> u = w ) ) )
45 39 44 sylbi 
 |-  ( X e/ N -> ( ( A ` u ) = X -> ( ( A ` u ) e. N -> u = w ) ) )
46 45 com12 
 |-  ( ( A ` u ) = X -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) )
47 38 46 syl6 
 |-  ( ( ( ph /\ ( u e. D /\ w e. D ) ) /\ u =/= w ) -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) )
48 47 expcom 
 |-  ( u =/= w -> ( ( ph /\ ( u e. D /\ w e. D ) ) -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) )
49 48 com23 
 |-  ( u =/= w -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) -> ( ( ph /\ ( u e. D /\ w e. D ) ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) )
50 35 49 sylbir 
 |-  ( -. u = w -> ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` u ) } e. E ) -> ( ( ph /\ ( u e. D /\ w e. D ) ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) )
51 34 50 syl5com 
 |-  ( ( ( A ` u ) = ( A ` w ) /\ ( { u , ( A ` u ) } e. E /\ { w , ( A ` w ) } e. E ) ) -> ( -. u = w -> ( ( ph /\ ( u e. D /\ w e. D ) ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) )
52 51 expcom 
 |-  ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` w ) } e. E ) -> ( ( A ` u ) = ( A ` w ) -> ( -. u = w -> ( ( ph /\ ( u e. D /\ w e. D ) ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) ) )
53 52 com24 
 |-  ( ( { u , ( A ` u ) } e. E /\ { w , ( A ` w ) } e. E ) -> ( ( ph /\ ( u e. D /\ w e. D ) ) -> ( -. u = w -> ( ( A ` u ) = ( A ` w ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) ) )
54 29 53 mpcom 
 |-  ( ( ph /\ ( u e. D /\ w e. D ) ) -> ( -. u = w -> ( ( A ` u ) = ( A ` w ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) )
55 54 ex 
 |-  ( ph -> ( ( u e. D /\ w e. D ) -> ( -. u = w -> ( ( A ` u ) = ( A ` w ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) ) )
56 55 com3r 
 |-  ( -. u = w -> ( ph -> ( ( u e. D /\ w e. D ) -> ( ( A ` u ) = ( A ` w ) -> ( X e/ N -> ( ( A ` u ) e. N -> u = w ) ) ) ) ) )
57 56 com15 
 |-  ( X e/ N -> ( ph -> ( ( u e. D /\ w e. D ) -> ( ( A ` u ) = ( A ` w ) -> ( -. u = w -> ( ( A ` u ) e. N -> u = w ) ) ) ) ) )
58 16 57 mpcom 
 |-  ( ph -> ( ( u e. D /\ w e. D ) -> ( ( A ` u ) = ( A ` w ) -> ( -. u = w -> ( ( A ` u ) e. N -> u = w ) ) ) ) )
59 58 expd 
 |-  ( ph -> ( u e. D -> ( w e. D -> ( ( A ` u ) = ( A ` w ) -> ( -. u = w -> ( ( A ` u ) e. N -> u = w ) ) ) ) ) )
60 59 adantr 
 |-  ( ( ph /\ A : D --> N ) -> ( u e. D -> ( w e. D -> ( ( A ` u ) = ( A ` w ) -> ( -. u = w -> ( ( A ` u ) e. N -> u = w ) ) ) ) ) )
61 60 imp42 
 |-  ( ( ( ( ph /\ A : D --> N ) /\ ( u e. D /\ w e. D ) ) /\ ( A ` u ) = ( A ` w ) ) -> ( -. u = w -> ( ( A ` u ) e. N -> u = w ) ) )
62 15 61 mpid 
 |-  ( ( ( ( ph /\ A : D --> N ) /\ ( u e. D /\ w e. D ) ) /\ ( A ` u ) = ( A ` w ) ) -> ( -. u = w -> u = w ) )
63 62 pm2.18d 
 |-  ( ( ( ( ph /\ A : D --> N ) /\ ( u e. D /\ w e. D ) ) /\ ( A ` u ) = ( A ` w ) ) -> u = w )
64 63 ex 
 |-  ( ( ( ph /\ A : D --> N ) /\ ( u e. D /\ w e. D ) ) -> ( ( A ` u ) = ( A ` w ) -> u = w ) )
65 64 ralrimivva 
 |-  ( ( ph /\ A : D --> N ) -> A. u e. D A. w e. D ( ( A ` u ) = ( A ` w ) -> u = w ) )
66 dff13 
 |-  ( A : D -1-1-> N <-> ( A : D --> N /\ A. u e. D A. w e. D ( ( A ` u ) = ( A ` w ) -> u = w ) ) )
67 12 65 66 sylanbrc 
 |-  ( ( ph /\ A : D --> N ) -> A : D -1-1-> N )
68 11 67 mpdan 
 |-  ( ph -> A : D -1-1-> N )