Metamath Proof Explorer

Theorem frgrncvvdeqlem9

Description: Lemma 9 for frgrncvvdeq . This corresponds to statement 3 in Huneke p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 12-Feb-2022)

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 frgrncvvdeqlem9 
|- ( ph -> A : D -onto-> 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 9 adantr 
 |-  ( ( ph /\ n e. N ) -> G e. FriendGraph )
13 4 eleq2i 
 |-  ( n e. N <-> n e. ( G NeighbVtx Y ) )
14 1 nbgrisvtx 
 |-  ( n e. ( G NeighbVtx Y ) -> n e. V )
15 14 a1i 
 |-  ( ph -> ( n e. ( G NeighbVtx Y ) -> n e. V ) )
16 13 15 biimtrid 
 |-  ( ph -> ( n e. N -> n e. V ) )
17 16 imp 
 |-  ( ( ph /\ n e. N ) -> n e. V )
18 5 adantr 
 |-  ( ( ph /\ n e. N ) -> X e. V )
19 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem1 
 |-  ( ph -> X e/ N )
20 df-nel 
 |-  ( X e/ N <-> -. X e. N )
21 nelelne 
 |-  ( -. X e. N -> ( n e. N -> n =/= X ) )
22 20 21 sylbi 
 |-  ( X e/ N -> ( n e. N -> n =/= X ) )
23 19 22 syl 
 |-  ( ph -> ( n e. N -> n =/= X ) )
24 23 imp 
 |-  ( ( ph /\ n e. N ) -> n =/= X )
25 17 18 24 3jca 
 |-  ( ( ph /\ n e. N ) -> ( n e. V /\ X e. V /\ n =/= X ) )
26 12 25 jca 
 |-  ( ( ph /\ n e. N ) -> ( G e. FriendGraph /\ ( n e. V /\ X e. V /\ n =/= X ) ) )
27 1 2 frcond2 
 |-  ( G e. FriendGraph -> ( ( n e. V /\ X e. V /\ n =/= X ) -> E! m e. V ( { n , m } e. E /\ { m , X } e. E ) ) )
28 27 imp 
 |-  ( ( G e. FriendGraph /\ ( n e. V /\ X e. V /\ n =/= X ) ) -> E! m e. V ( { n , m } e. E /\ { m , X } e. E ) )
29 reurex 
 |-  ( E! m e. V ( { n , m } e. E /\ { m , X } e. E ) -> E. m e. V ( { n , m } e. E /\ { m , X } e. E ) )
30 df-rex 
 |-  ( E. m e. V ( { n , m } e. E /\ { m , X } e. E ) <-> E. m ( m e. V /\ ( { n , m } e. E /\ { m , X } e. E ) ) )
31 29 30 sylib 
 |-  ( E! m e. V ( { n , m } e. E /\ { m , X } e. E ) -> E. m ( m e. V /\ ( { n , m } e. E /\ { m , X } e. E ) ) )
32 26 28 31 3syl 
 |-  ( ( ph /\ n e. N ) -> E. m ( m e. V /\ ( { n , m } e. E /\ { m , X } e. E ) ) )
33 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
34 2 nbusgreledg 
 |-  ( G e. USGraph -> ( m e. ( G NeighbVtx X ) <-> { m , X } e. E ) )
35 34 bicomd 
 |-  ( G e. USGraph -> ( { m , X } e. E <-> m e. ( G NeighbVtx X ) ) )
36 9 33 35 3syl 
 |-  ( ph -> ( { m , X } e. E <-> m e. ( G NeighbVtx X ) ) )
37 36 biimpa 
 |-  ( ( ph /\ { m , X } e. E ) -> m e. ( G NeighbVtx X ) )
38 3 eleq2i 
 |-  ( m e. D <-> m e. ( G NeighbVtx X ) )
39 37 38 sylibr 
 |-  ( ( ph /\ { m , X } e. E ) -> m e. D )
40 39 ad2ant2rl 
 |-  ( ( ( ph /\ n e. N ) /\ ( { n , m } e. E /\ { m , X } e. E ) ) -> m e. D )
41 2 nbusgreledg 
 |-  ( G e. USGraph -> ( n e. ( G NeighbVtx m ) <-> { n , m } e. E ) )
42 41 biimpar 
 |-  ( ( G e. USGraph /\ { n , m } e. E ) -> n e. ( G NeighbVtx m ) )
43 42 a1d 
 |-  ( ( G e. USGraph /\ { n , m } e. E ) -> ( { m , X } e. E -> n e. ( G NeighbVtx m ) ) )
44 43 expimpd 
 |-  ( G e. USGraph -> ( ( { n , m } e. E /\ { m , X } e. E ) -> n e. ( G NeighbVtx m ) ) )
45 9 33 44 3syl 
 |-  ( ph -> ( ( { n , m } e. E /\ { m , X } e. E ) -> n e. ( G NeighbVtx m ) ) )
46 45 adantr 
 |-  ( ( ph /\ n e. N ) -> ( ( { n , m } e. E /\ { m , X } e. E ) -> n e. ( G NeighbVtx m ) ) )
47 46 imp 
 |-  ( ( ( ph /\ n e. N ) /\ ( { n , m } e. E /\ { m , X } e. E ) ) -> n e. ( G NeighbVtx m ) )
48 elin 
 |-  ( n e. ( ( G NeighbVtx m ) i^i N ) <-> ( n e. ( G NeighbVtx m ) /\ n e. N ) )
49 simpl 
 |-  ( ( ph /\ { m , X } e. E ) -> ph )
50 49 39 jca 
 |-  ( ( ph /\ { m , X } e. E ) -> ( ph /\ m e. D ) )
51 preq1 
 |-  ( x = m -> { x , y } = { m , y } )
52 51 eleq1d 
 |-  ( x = m -> ( { x , y } e. E <-> { m , y } e. E ) )
53 52 riotabidv 
 |-  ( x = m -> ( iota_ y e. N { x , y } e. E ) = ( iota_ y e. N { m , y } e. E ) )
54 53 cbvmptv 
 |-  ( x e. D |-> ( iota_ y e. N { x , y } e. E ) ) = ( m e. D |-> ( iota_ y e. N { m , y } e. E ) )
55 10 54 eqtri 
 |-  A = ( m e. D |-> ( iota_ y e. N { m , y } e. E ) )
56 1 2 3 4 5 6 7 8 9 55 frgrncvvdeqlem5 
 |-  ( ( ph /\ m e. D ) -> { ( A ` m ) } = ( ( G NeighbVtx m ) i^i N ) )
57 eleq2 
 |-  ( ( ( G NeighbVtx m ) i^i N ) = { ( A ` m ) } -> ( n e. ( ( G NeighbVtx m ) i^i N ) <-> n e. { ( A ` m ) } ) )
58 57 eqcoms 
 |-  ( { ( A ` m ) } = ( ( G NeighbVtx m ) i^i N ) -> ( n e. ( ( G NeighbVtx m ) i^i N ) <-> n e. { ( A ` m ) } ) )
59 elsni 
 |-  ( n e. { ( A ` m ) } -> n = ( A ` m ) )
60 58 59 biimtrdi 
 |-  ( { ( A ` m ) } = ( ( G NeighbVtx m ) i^i N ) -> ( n e. ( ( G NeighbVtx m ) i^i N ) -> n = ( A ` m ) ) )
61 50 56 60 3syl 
 |-  ( ( ph /\ { m , X } e. E ) -> ( n e. ( ( G NeighbVtx m ) i^i N ) -> n = ( A ` m ) ) )
62 61 expcom 
 |-  ( { m , X } e. E -> ( ph -> ( n e. ( ( G NeighbVtx m ) i^i N ) -> n = ( A ` m ) ) ) )
63 62 com3r 
 |-  ( n e. ( ( G NeighbVtx m ) i^i N ) -> ( { m , X } e. E -> ( ph -> n = ( A ` m ) ) ) )
64 48 63 sylbir 
 |-  ( ( n e. ( G NeighbVtx m ) /\ n e. N ) -> ( { m , X } e. E -> ( ph -> n = ( A ` m ) ) ) )
65 64 ex 
 |-  ( n e. ( G NeighbVtx m ) -> ( n e. N -> ( { m , X } e. E -> ( ph -> n = ( A ` m ) ) ) ) )
66 65 com14 
 |-  ( ph -> ( n e. N -> ( { m , X } e. E -> ( n e. ( G NeighbVtx m ) -> n = ( A ` m ) ) ) ) )
67 66 imp 
 |-  ( ( ph /\ n e. N ) -> ( { m , X } e. E -> ( n e. ( G NeighbVtx m ) -> n = ( A ` m ) ) ) )
68 67 adantld 
 |-  ( ( ph /\ n e. N ) -> ( ( { n , m } e. E /\ { m , X } e. E ) -> ( n e. ( G NeighbVtx m ) -> n = ( A ` m ) ) ) )
69 68 imp 
 |-  ( ( ( ph /\ n e. N ) /\ ( { n , m } e. E /\ { m , X } e. E ) ) -> ( n e. ( G NeighbVtx m ) -> n = ( A ` m ) ) )
70 47 69 mpd 
 |-  ( ( ( ph /\ n e. N ) /\ ( { n , m } e. E /\ { m , X } e. E ) ) -> n = ( A ` m ) )
71 40 70 jca 
 |-  ( ( ( ph /\ n e. N ) /\ ( { n , m } e. E /\ { m , X } e. E ) ) -> ( m e. D /\ n = ( A ` m ) ) )
72 71 ex 
 |-  ( ( ph /\ n e. N ) -> ( ( { n , m } e. E /\ { m , X } e. E ) -> ( m e. D /\ n = ( A ` m ) ) ) )
73 72 adantld 
 |-  ( ( ph /\ n e. N ) -> ( ( m e. V /\ ( { n , m } e. E /\ { m , X } e. E ) ) -> ( m e. D /\ n = ( A ` m ) ) ) )
74 73 eximdv 
 |-  ( ( ph /\ n e. N ) -> ( E. m ( m e. V /\ ( { n , m } e. E /\ { m , X } e. E ) ) -> E. m ( m e. D /\ n = ( A ` m ) ) ) )
75 32 74 mpd 
 |-  ( ( ph /\ n e. N ) -> E. m ( m e. D /\ n = ( A ` m ) ) )
76 df-rex 
 |-  ( E. m e. D n = ( A ` m ) <-> E. m ( m e. D /\ n = ( A ` m ) ) )
77 75 76 sylibr 
 |-  ( ( ph /\ n e. N ) -> E. m e. D n = ( A ` m ) )
78 77 ralrimiva 
 |-  ( ph -> A. n e. N E. m e. D n = ( A ` m ) )
79 dffo3 
 |-  ( A : D -onto-> N <-> ( A : D --> N /\ A. n e. N E. m e. D n = ( A ` m ) ) )
80 11 78 79 sylanbrc 
 |-  ( ph -> A : D -onto-> N )