Metamath Proof Explorer

Theorem usgredg2v

Description: In a simple graph, the mapping of edges having a fixed endpoint to the other vertex of the edge is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020)

Ref Expression
Hypotheses usgredg2v.v 
|- V = ( Vtx ` G )
usgredg2v.e 
|- E = ( iEdg ` G )
usgredg2v.a 
|- A = { x e. dom E | N e. ( E ` x ) }
usgredg2v.f 
|- F = ( y e. A |-> ( iota_ z e. V ( E ` y ) = { z , N } ) )
Assertion usgredg2v 
|- ( ( G e. USGraph /\ N e. V ) -> F : A -1-1-> V )

Proof

Step Hyp Ref Expression
1 usgredg2v.v 
 |-  V = ( Vtx ` G )
2 usgredg2v.e 
 |-  E = ( iEdg ` G )
3 usgredg2v.a 
 |-  A = { x e. dom E | N e. ( E ` x ) }
4 usgredg2v.f 
 |-  F = ( y e. A |-> ( iota_ z e. V ( E ` y ) = { z , N } ) )
5 1 2 3 usgredg2vlem1 
 |-  ( ( G e. USGraph /\ y e. A ) -> ( iota_ z e. V ( E ` y ) = { z , N } ) e. V )
6 5 ralrimiva 
 |-  ( G e. USGraph -> A. y e. A ( iota_ z e. V ( E ` y ) = { z , N } ) e. V )
7 6 adantr 
 |-  ( ( G e. USGraph /\ N e. V ) -> A. y e. A ( iota_ z e. V ( E ` y ) = { z , N } ) e. V )
8 2 usgrf1 
 |-  ( G e. USGraph -> E : dom E -1-1-> ran E )
9 8 adantr 
 |-  ( ( G e. USGraph /\ N e. V ) -> E : dom E -1-1-> ran E )
10 elrabi 
 |-  ( y e. { x e. dom E | N e. ( E ` x ) } -> y e. dom E )
11 10 3 eleq2s 
 |-  ( y e. A -> y e. dom E )
12 elrabi 
 |-  ( w e. { x e. dom E | N e. ( E ` x ) } -> w e. dom E )
13 12 3 eleq2s 
 |-  ( w e. A -> w e. dom E )
14 11 13 anim12i 
 |-  ( ( y e. A /\ w e. A ) -> ( y e. dom E /\ w e. dom E ) )
15 f1fveq 
 |-  ( ( E : dom E -1-1-> ran E /\ ( y e. dom E /\ w e. dom E ) ) -> ( ( E ` y ) = ( E ` w ) <-> y = w ) )
16 9 14 15 syl2an 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( ( E ` y ) = ( E ` w ) <-> y = w ) )
17 16 bicomd 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( y = w <-> ( E ` y ) = ( E ` w ) ) )
18 17 notbid 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( -. y = w <-> -. ( E ` y ) = ( E ` w ) ) )
19 simpl 
 |-  ( ( G e. USGraph /\ N e. V ) -> G e. USGraph )
20 simpl 
 |-  ( ( y e. A /\ w e. A ) -> y e. A )
21 19 20 anim12i 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( G e. USGraph /\ y e. A ) )
22 preq1 
 |-  ( u = z -> { u , N } = { z , N } )
23 22 eqeq2d 
 |-  ( u = z -> ( ( E ` y ) = { u , N } <-> ( E ` y ) = { z , N } ) )
24 23 cbvriotavw 
 |-  ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ z e. V ( E ` y ) = { z , N } )
25 1 2 3 usgredg2vlem2 
 |-  ( ( G e. USGraph /\ y e. A ) -> ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ z e. V ( E ` y ) = { z , N } ) -> ( E ` y ) = { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } ) )
26 21 24 25 mpisyl 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( E ` y ) = { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } )
27 an3 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( G e. USGraph /\ w e. A ) )
28 22 eqeq2d 
 |-  ( u = z -> ( ( E ` w ) = { u , N } <-> ( E ` w ) = { z , N } ) )
29 28 cbvriotavw 
 |-  ( iota_ u e. V ( E ` w ) = { u , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } )
30 1 2 3 usgredg2vlem2 
 |-  ( ( G e. USGraph /\ w e. A ) -> ( ( iota_ u e. V ( E ` w ) = { u , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) -> ( E ` w ) = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } ) )
31 27 29 30 mpisyl 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( E ` w ) = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } )
32 26 31 eqeq12d 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( ( E ` y ) = ( E ` w ) <-> { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } ) )
33 32 notbid 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( -. ( E ` y ) = ( E ` w ) <-> -. { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } ) )
34 riotaex 
 |-  ( iota_ u e. V ( E ` y ) = { u , N } ) e. _V
35 34 a1i 
 |-  ( N e. V -> ( iota_ u e. V ( E ` y ) = { u , N } ) e. _V )
36 id 
 |-  ( N e. V -> N e. V )
37 riotaex 
 |-  ( iota_ u e. V ( E ` w ) = { u , N } ) e. _V
38 37 a1i 
 |-  ( N e. V -> ( iota_ u e. V ( E ` w ) = { u , N } ) e. _V )
39 preq12bg 
 |-  ( ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) e. _V /\ N e. V ) /\ ( ( iota_ u e. V ( E ` w ) = { u , N } ) e. _V /\ N e. V ) ) -> ( { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } <-> ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) \/ ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) ) )
40 35 36 38 36 39 syl22anc 
 |-  ( N e. V -> ( { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } <-> ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) \/ ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) ) )
41 40 notbid 
 |-  ( N e. V -> ( -. { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } <-> -. ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) \/ ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) ) )
42 41 adantl 
 |-  ( ( G e. USGraph /\ N e. V ) -> ( -. { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } <-> -. ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) \/ ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) ) )
43 ioran 
 |-  ( -. ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) \/ ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) <-> ( -. ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) /\ -. ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) )
44 ianor 
 |-  ( -. ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) <-> ( -. ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) \/ -. N = N ) )
45 24 29 eqeq12i 
 |-  ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) <-> ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) )
46 45 notbii 
 |-  ( -. ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) <-> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) )
47 46 biimpi 
 |-  ( -. ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) )
48 47 a1d 
 |-  ( -. ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) -> ( G e. USGraph -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
49 eqid 
 |-  N = N
50 49 pm2.24i 
 |-  ( -. N = N -> ( G e. USGraph -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
51 48 50 jaoi 
 |-  ( ( -. ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) \/ -. N = N ) -> ( G e. USGraph -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
52 44 51 sylbi 
 |-  ( -. ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) -> ( G e. USGraph -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
53 52 adantr 
 |-  ( ( -. ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) /\ -. ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) -> ( G e. USGraph -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
54 43 53 sylbi 
 |-  ( -. ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) \/ ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) -> ( G e. USGraph -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
55 54 com12 
 |-  ( G e. USGraph -> ( -. ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) \/ ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
56 55 adantr 
 |-  ( ( G e. USGraph /\ N e. V ) -> ( -. ( ( ( iota_ u e. V ( E ` y ) = { u , N } ) = ( iota_ u e. V ( E ` w ) = { u , N } ) /\ N = N ) \/ ( ( iota_ u e. V ( E ` y ) = { u , N } ) = N /\ N = ( iota_ u e. V ( E ` w ) = { u , N } ) ) ) -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
57 42 56 sylbid 
 |-  ( ( G e. USGraph /\ N e. V ) -> ( -. { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
58 57 adantr 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( -. { ( iota_ u e. V ( E ` y ) = { u , N } ) , N } = { ( iota_ u e. V ( E ` w ) = { u , N } ) , N } -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
59 33 58 sylbid 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( -. ( E ` y ) = ( E ` w ) -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
60 18 59 sylbid 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( -. y = w -> -. ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) ) )
61 60 con4d 
 |-  ( ( ( G e. USGraph /\ N e. V ) /\ ( y e. A /\ w e. A ) ) -> ( ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) -> y = w ) )
62 61 ralrimivva 
 |-  ( ( G e. USGraph /\ N e. V ) -> A. y e. A A. w e. A ( ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) -> y = w ) )
63 fveqeq2 
 |-  ( y = w -> ( ( E ` y ) = { z , N } <-> ( E ` w ) = { z , N } ) )
64 63 riotabidv 
 |-  ( y = w -> ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) )
65 4 64 f1mpt 
 |-  ( F : A -1-1-> V <-> ( A. y e. A ( iota_ z e. V ( E ` y ) = { z , N } ) e. V /\ A. y e. A A. w e. A ( ( iota_ z e. V ( E ` y ) = { z , N } ) = ( iota_ z e. V ( E ` w ) = { z , N } ) -> y = w ) ) )
66 7 62 65 sylanbrc 
 |-  ( ( G e. USGraph /\ N e. V ) -> F : A -1-1-> V )