Metamath Proof Explorer

Theorem uspgredg2v

Description: In a simple pseudograph, the mapping of edges having a fixed endpoint to the "other" vertex of the edge (which may be the fixed vertex itself in the case of a loop) is a one-to-one function into the set of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 6-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 uspgredg2v.v 
 |-  V = ( Vtx ` G )
2 uspgredg2v.e 
 |-  E = ( Edg ` G )
3 uspgredg2v.a 
 |-  A = { e e. E | N e. e }
4 uspgredg2v.f 
 |-  F = ( y e. A |-> ( iota_ z e. V y = { N , z } ) )
5 1 2 3 uspgredg2vlem 
 |-  ( ( G e. USPGraph /\ y e. A ) -> ( iota_ z e. V y = { N , z } ) e. V )
6 5 ralrimiva 
 |-  ( G e. USPGraph -> A. y e. A ( iota_ z e. V y = { N , z } ) e. V )
7 6 adantr 
 |-  ( ( G e. USPGraph /\ N e. V ) -> A. y e. A ( iota_ z e. V y = { N , z } ) e. V )
8 preq2 
 |-  ( z = n -> { N , z } = { N , n } )
9 8 eqeq2d 
 |-  ( z = n -> ( y = { N , z } <-> y = { N , n } ) )
10 9 cbvriotavw 
 |-  ( iota_ z e. V y = { N , z } ) = ( iota_ n e. V y = { N , n } )
11 8 eqeq2d 
 |-  ( z = n -> ( x = { N , z } <-> x = { N , n } ) )
12 11 cbvriotavw 
 |-  ( iota_ z e. V x = { N , z } ) = ( iota_ n e. V x = { N , n } )
13 simpl 
 |-  ( ( G e. USPGraph /\ N e. V ) -> G e. USPGraph )
14 eleq2w 
 |-  ( e = y -> ( N e. e <-> N e. y ) )
15 14 3 elrab2 
 |-  ( y e. A <-> ( y e. E /\ N e. y ) )
16 2 eleq2i 
 |-  ( y e. E <-> y e. ( Edg ` G ) )
17 16 biimpi 
 |-  ( y e. E -> y e. ( Edg ` G ) )
18 17 anim1i 
 |-  ( ( y e. E /\ N e. y ) -> ( y e. ( Edg ` G ) /\ N e. y ) )
19 15 18 sylbi 
 |-  ( y e. A -> ( y e. ( Edg ` G ) /\ N e. y ) )
20 19 adantr 
 |-  ( ( y e. A /\ x e. A ) -> ( y e. ( Edg ` G ) /\ N e. y ) )
21 13 20 anim12i 
 |-  ( ( ( G e. USPGraph /\ N e. V ) /\ ( y e. A /\ x e. A ) ) -> ( G e. USPGraph /\ ( y e. ( Edg ` G ) /\ N e. y ) ) )
22 3anass 
 |-  ( ( G e. USPGraph /\ y e. ( Edg ` G ) /\ N e. y ) <-> ( G e. USPGraph /\ ( y e. ( Edg ` G ) /\ N e. y ) ) )
23 21 22 sylibr 
 |-  ( ( ( G e. USPGraph /\ N e. V ) /\ ( y e. A /\ x e. A ) ) -> ( G e. USPGraph /\ y e. ( Edg ` G ) /\ N e. y ) )
24 uspgredg2vtxeu 
 |-  ( ( G e. USPGraph /\ y e. ( Edg ` G ) /\ N e. y ) -> E! n e. ( Vtx ` G ) y = { N , n } )
25 reueq1 
 |-  ( V = ( Vtx ` G ) -> ( E! n e. V y = { N , n } <-> E! n e. ( Vtx ` G ) y = { N , n } ) )
26 1 25 ax-mp 
 |-  ( E! n e. V y = { N , n } <-> E! n e. ( Vtx ` G ) y = { N , n } )
27 24 26 sylibr 
 |-  ( ( G e. USPGraph /\ y e. ( Edg ` G ) /\ N e. y ) -> E! n e. V y = { N , n } )
28 23 27 syl 
 |-  ( ( ( G e. USPGraph /\ N e. V ) /\ ( y e. A /\ x e. A ) ) -> E! n e. V y = { N , n } )
29 eleq2w 
 |-  ( e = x -> ( N e. e <-> N e. x ) )
30 29 3 elrab2 
 |-  ( x e. A <-> ( x e. E /\ N e. x ) )
31 2 eleq2i 
 |-  ( x e. E <-> x e. ( Edg ` G ) )
32 31 biimpi 
 |-  ( x e. E -> x e. ( Edg ` G ) )
33 32 anim1i 
 |-  ( ( x e. E /\ N e. x ) -> ( x e. ( Edg ` G ) /\ N e. x ) )
34 30 33 sylbi 
 |-  ( x e. A -> ( x e. ( Edg ` G ) /\ N e. x ) )
35 34 adantl 
 |-  ( ( y e. A /\ x e. A ) -> ( x e. ( Edg ` G ) /\ N e. x ) )
36 13 35 anim12i 
 |-  ( ( ( G e. USPGraph /\ N e. V ) /\ ( y e. A /\ x e. A ) ) -> ( G e. USPGraph /\ ( x e. ( Edg ` G ) /\ N e. x ) ) )
37 3anass 
 |-  ( ( G e. USPGraph /\ x e. ( Edg ` G ) /\ N e. x ) <-> ( G e. USPGraph /\ ( x e. ( Edg ` G ) /\ N e. x ) ) )
38 36 37 sylibr 
 |-  ( ( ( G e. USPGraph /\ N e. V ) /\ ( y e. A /\ x e. A ) ) -> ( G e. USPGraph /\ x e. ( Edg ` G ) /\ N e. x ) )
39 uspgredg2vtxeu 
 |-  ( ( G e. USPGraph /\ x e. ( Edg ` G ) /\ N e. x ) -> E! n e. ( Vtx ` G ) x = { N , n } )
40 reueq1 
 |-  ( V = ( Vtx ` G ) -> ( E! n e. V x = { N , n } <-> E! n e. ( Vtx ` G ) x = { N , n } ) )
41 1 40 ax-mp 
 |-  ( E! n e. V x = { N , n } <-> E! n e. ( Vtx ` G ) x = { N , n } )
42 39 41 sylibr 
 |-  ( ( G e. USPGraph /\ x e. ( Edg ` G ) /\ N e. x ) -> E! n e. V x = { N , n } )
43 38 42 syl 
 |-  ( ( ( G e. USPGraph /\ N e. V ) /\ ( y e. A /\ x e. A ) ) -> E! n e. V x = { N , n } )
44 10 12 28 43 riotaeqimp 
 |-  ( ( ( ( G e. USPGraph /\ N e. V ) /\ ( y e. A /\ x e. A ) ) /\ ( iota_ z e. V y = { N , z } ) = ( iota_ z e. V x = { N , z } ) ) -> y = x )
45 44 ex 
 |-  ( ( ( G e. USPGraph /\ N e. V ) /\ ( y e. A /\ x e. A ) ) -> ( ( iota_ z e. V y = { N , z } ) = ( iota_ z e. V x = { N , z } ) -> y = x ) )
46 45 ralrimivva 
 |-  ( ( G e. USPGraph /\ N e. V ) -> A. y e. A A. x e. A ( ( iota_ z e. V y = { N , z } ) = ( iota_ z e. V x = { N , z } ) -> y = x ) )
47 eqeq1 
 |-  ( y = x -> ( y = { N , z } <-> x = { N , z } ) )
48 47 riotabidv 
 |-  ( y = x -> ( iota_ z e. V y = { N , z } ) = ( iota_ z e. V x = { N , z } ) )
49 4 48 f1mpt 
 |-  ( F : A -1-1-> V <-> ( A. y e. A ( iota_ z e. V y = { N , z } ) e. V /\ A. y e. A A. x e. A ( ( iota_ z e. V y = { N , z } ) = ( iota_ z e. V x = { N , z } ) -> y = x ) ) )
50 7 46 49 sylanbrc 
 |-  ( ( G e. USPGraph /\ N e. V ) -> F : A -1-1-> V )