Metamath Proof Explorer

Theorem uspgrsprf1

Description: The mapping F is a one-to-one function from the "simple pseudographs" with a fixed set of vertices V into the subsets of the set of pairs over the set V . (Contributed by AV, 25-Nov-2021)

Ref Expression
Hypotheses uspgrsprf.p 
|- P = ~P ( Pairs ` V )
uspgrsprf.g 
|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
uspgrsprf.f 
|- F = ( g e. G |-> ( 2nd ` g ) )
Assertion uspgrsprf1 
|- F : G -1-1-> P

Proof

Step Hyp Ref Expression
1 uspgrsprf.p 
 |-  P = ~P ( Pairs ` V )
2 uspgrsprf.g 
 |-  G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
3 uspgrsprf.f 
 |-  F = ( g e. G |-> ( 2nd ` g ) )
4 1 2 3 uspgrsprf 
 |-  F : G --> P
5 1 2 3 uspgrsprfv 
 |-  ( a e. G -> ( F ` a ) = ( 2nd ` a ) )
6 1 2 3 uspgrsprfv 
 |-  ( b e. G -> ( F ` b ) = ( 2nd ` b ) )
7 5 6 eqeqan12d 
 |-  ( ( a e. G /\ b e. G ) -> ( ( F ` a ) = ( F ` b ) <-> ( 2nd ` a ) = ( 2nd ` b ) ) )
8 2 eleq2i 
 |-  ( a e. G <-> a e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } )
9 elopab 
 |-  ( a e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } <-> E. v E. e ( a = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) )
10 opeq12 
 |-  ( ( v = w /\ e = f ) -> <. v , e >. = <. w , f >. )
11 10 eqeq2d 
 |-  ( ( v = w /\ e = f ) -> ( a = <. v , e >. <-> a = <. w , f >. ) )
12 eqeq1 
 |-  ( v = w -> ( v = V <-> w = V ) )
13 12 adantr 
 |-  ( ( v = w /\ e = f ) -> ( v = V <-> w = V ) )
14 eqeq2 
 |-  ( v = w -> ( ( Vtx ` q ) = v <-> ( Vtx ` q ) = w ) )
15 eqeq2 
 |-  ( e = f -> ( ( Edg ` q ) = e <-> ( Edg ` q ) = f ) )
16 14 15 bi2anan9 
 |-  ( ( v = w /\ e = f ) -> ( ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) <-> ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) )
17 16 rexbidv 
 |-  ( ( v = w /\ e = f ) -> ( E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) <-> E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) )
18 13 17 anbi12d 
 |-  ( ( v = w /\ e = f ) -> ( ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) <-> ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) )
19 11 18 anbi12d 
 |-  ( ( v = w /\ e = f ) -> ( ( a = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) <-> ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) ) )
20 19 cbvex2vw 
 |-  ( E. v E. e ( a = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) <-> E. w E. f ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) )
21 8 9 20 3bitri 
 |-  ( a e. G <-> E. w E. f ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) )
22 2 eleq2i 
 |-  ( b e. G <-> b e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } )
23 elopab 
 |-  ( b e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } <-> E. v E. e ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) )
24 22 23 bitri 
 |-  ( b e. G <-> E. v E. e ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) )
25 eqeq2 
 |-  ( w = V -> ( v = w <-> v = V ) )
26 opeq12 
 |-  ( ( w = v /\ f = e ) -> <. w , f >. = <. v , e >. )
27 26 ex 
 |-  ( w = v -> ( f = e -> <. w , f >. = <. v , e >. ) )
28 27 equcoms 
 |-  ( v = w -> ( f = e -> <. w , f >. = <. v , e >. ) )
29 25 28 syl6bir 
 |-  ( w = V -> ( v = V -> ( f = e -> <. w , f >. = <. v , e >. ) ) )
30 29 ad2antrl 
 |-  ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( v = V -> ( f = e -> <. w , f >. = <. v , e >. ) ) )
31 30 com12 
 |-  ( v = V -> ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( f = e -> <. w , f >. = <. v , e >. ) ) )
32 31 ad2antrl 
 |-  ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( f = e -> <. w , f >. = <. v , e >. ) ) )
33 32 imp 
 |-  ( ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) /\ ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) ) -> ( f = e -> <. w , f >. = <. v , e >. ) )
34 vex 
 |-  w e. _V
35 vex 
 |-  f e. _V
36 34 35 op2ndd 
 |-  ( a = <. w , f >. -> ( 2nd ` a ) = f )
37 36 ad2antrl 
 |-  ( ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) /\ ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) ) -> ( 2nd ` a ) = f )
38 vex 
 |-  v e. _V
39 vex 
 |-  e e. _V
40 38 39 op2ndd 
 |-  ( b = <. v , e >. -> ( 2nd ` b ) = e )
41 40 adantr 
 |-  ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( 2nd ` b ) = e )
42 41 adantr 
 |-  ( ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) /\ ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) ) -> ( 2nd ` b ) = e )
43 37 42 eqeq12d 
 |-  ( ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) /\ ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) ) -> ( ( 2nd ` a ) = ( 2nd ` b ) <-> f = e ) )
44 eqeq12 
 |-  ( ( a = <. w , f >. /\ b = <. v , e >. ) -> ( a = b <-> <. w , f >. = <. v , e >. ) )
45 44 ex 
 |-  ( a = <. w , f >. -> ( b = <. v , e >. -> ( a = b <-> <. w , f >. = <. v , e >. ) ) )
46 45 adantr 
 |-  ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( b = <. v , e >. -> ( a = b <-> <. w , f >. = <. v , e >. ) ) )
47 46 com12 
 |-  ( b = <. v , e >. -> ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( a = b <-> <. w , f >. = <. v , e >. ) ) )
48 47 adantr 
 |-  ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( a = b <-> <. w , f >. = <. v , e >. ) ) )
49 48 imp 
 |-  ( ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) /\ ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) ) -> ( a = b <-> <. w , f >. = <. v , e >. ) )
50 33 43 49 3imtr4d 
 |-  ( ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) /\ ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) ) -> ( ( 2nd ` a ) = ( 2nd ` b ) -> a = b ) )
51 50 ex 
 |-  ( ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( ( 2nd ` a ) = ( 2nd ` b ) -> a = b ) ) )
52 51 exlimivv 
 |-  ( E. v E. e ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( ( 2nd ` a ) = ( 2nd ` b ) -> a = b ) ) )
53 52 com12 
 |-  ( ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( E. v E. e ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( ( 2nd ` a ) = ( 2nd ` b ) -> a = b ) ) )
54 53 exlimivv 
 |-  ( E. w E. f ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) -> ( E. v E. e ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( ( 2nd ` a ) = ( 2nd ` b ) -> a = b ) ) )
55 54 imp 
 |-  ( ( E. w E. f ( a = <. w , f >. /\ ( w = V /\ E. q e. USPGraph ( ( Vtx ` q ) = w /\ ( Edg ` q ) = f ) ) ) /\ E. v E. e ( b = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) ) -> ( ( 2nd ` a ) = ( 2nd ` b ) -> a = b ) )
56 21 24 55 syl2anb 
 |-  ( ( a e. G /\ b e. G ) -> ( ( 2nd ` a ) = ( 2nd ` b ) -> a = b ) )
57 7 56 sylbid 
 |-  ( ( a e. G /\ b e. G ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) )
58 57 rgen2 
 |-  A. a e. G A. b e. G ( ( F ` a ) = ( F ` b ) -> a = b )
59 dff13 
 |-  ( F : G -1-1-> P <-> ( F : G --> P /\ A. a e. G A. b e. G ( ( F ` a ) = ( F ` b ) -> a = b ) ) )
60 4 58 59 mpbir2an 
 |-  F : G -1-1-> P