Metamath Proof Explorer

Theorem uspgrsprfo

Description: The mapping F is a function from the "simple pseudographs" with a fixed set of vertices V onto 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 uspgrsprfo 
|- ( V e. W -> F : G -onto-> 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 4 a1i 
 |-  ( V e. W -> F : G --> P )
6 1 eleq2i 
 |-  ( a e. P <-> a e. ~P ( Pairs ` V ) )
7 velpw 
 |-  ( a e. ~P ( Pairs ` V ) <-> a C_ ( Pairs ` V ) )
8 6 7 bitri 
 |-  ( a e. P <-> a C_ ( Pairs ` V ) )
9 eqidd 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> V = V )
10 vex 
 |-  a e. _V
11 10 a1i 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> a e. _V )
12 f1oi 
 |-  ( _I |` a ) : a -1-1-onto-> a
13 12 a1i 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( _I |` a ) : a -1-1-onto-> a )
14 dmresi 
 |-  dom ( _I |` a ) = a
15 f1oeq2 
 |-  ( dom ( _I |` a ) = a -> ( ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> a <-> ( _I |` a ) : a -1-1-onto-> a ) )
16 14 15 ax-mp 
 |-  ( ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> a <-> ( _I |` a ) : a -1-1-onto-> a )
17 13 16 sylibr 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> a )
18 sprvalpwle2 
 |-  ( V e. W -> ( Pairs ` V ) = { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )
19 18 sseq2d 
 |-  ( V e. W -> ( a C_ ( Pairs ` V ) <-> a C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )
20 19 biimpac 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> a C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )
21 17 20 jca 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> a /\ a C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )
22 f1oeq3 
 |-  ( f = a -> ( ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> f <-> ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> a ) )
23 sseq1 
 |-  ( f = a -> ( f C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } <-> a C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )
24 22 23 anbi12d 
 |-  ( f = a -> ( ( ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> f /\ f C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) <-> ( ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> a /\ a C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) ) )
25 11 21 24 spcedv 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> E. f ( ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> f /\ f C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )
26 resiexg 
 |-  ( a e. _V -> ( _I |` a ) e. _V )
27 10 26 ax-mp 
 |-  ( _I |` a ) e. _V
28 27 f11o 
 |-  ( ( _I |` a ) : dom ( _I |` a ) -1-1-> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } <-> E. f ( ( _I |` a ) : dom ( _I |` a ) -1-1-onto-> f /\ f C_ { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )
29 25 28 sylibr 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( _I |` a ) : dom ( _I |` a ) -1-1-> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } )
30 10 a1i 
 |-  ( a C_ ( Pairs ` V ) -> a e. _V )
31 30 resiexd 
 |-  ( a C_ ( Pairs ` V ) -> ( _I |` a ) e. _V )
32 31 anim1ci 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( V e. W /\ ( _I |` a ) e. _V ) )
33 isuspgrop 
 |-  ( ( V e. W /\ ( _I |` a ) e. _V ) -> ( <. V , ( _I |` a ) >. e. USPGraph <-> ( _I |` a ) : dom ( _I |` a ) -1-1-> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )
34 32 33 syl 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( <. V , ( _I |` a ) >. e. USPGraph <-> ( _I |` a ) : dom ( _I |` a ) -1-1-> { p e. ( ~P V \ { (/) } ) | ( # ` p ) <_ 2 } ) )
35 29 34 mpbird 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> <. V , ( _I |` a ) >. e. USPGraph )
36 fveqeq2 
 |-  ( q = <. V , ( _I |` a ) >. -> ( ( Vtx ` q ) = V <-> ( Vtx ` <. V , ( _I |` a ) >. ) = V ) )
37 fveqeq2 
 |-  ( q = <. V , ( _I |` a ) >. -> ( ( Edg ` q ) = a <-> ( Edg ` <. V , ( _I |` a ) >. ) = a ) )
38 36 37 anbi12d 
 |-  ( q = <. V , ( _I |` a ) >. -> ( ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) <-> ( ( Vtx ` <. V , ( _I |` a ) >. ) = V /\ ( Edg ` <. V , ( _I |` a ) >. ) = a ) ) )
39 38 adantl 
 |-  ( ( ( a C_ ( Pairs ` V ) /\ V e. W ) /\ q = <. V , ( _I |` a ) >. ) -> ( ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) <-> ( ( Vtx ` <. V , ( _I |` a ) >. ) = V /\ ( Edg ` <. V , ( _I |` a ) >. ) = a ) ) )
40 opvtxfv 
 |-  ( ( V e. W /\ ( _I |` a ) e. _V ) -> ( Vtx ` <. V , ( _I |` a ) >. ) = V )
41 31 40 sylan2 
 |-  ( ( V e. W /\ a C_ ( Pairs ` V ) ) -> ( Vtx ` <. V , ( _I |` a ) >. ) = V )
42 edgopval 
 |-  ( ( V e. W /\ ( _I |` a ) e. _V ) -> ( Edg ` <. V , ( _I |` a ) >. ) = ran ( _I |` a ) )
43 31 42 sylan2 
 |-  ( ( V e. W /\ a C_ ( Pairs ` V ) ) -> ( Edg ` <. V , ( _I |` a ) >. ) = ran ( _I |` a ) )
44 rnresi 
 |-  ran ( _I |` a ) = a
45 43 44 eqtrdi 
 |-  ( ( V e. W /\ a C_ ( Pairs ` V ) ) -> ( Edg ` <. V , ( _I |` a ) >. ) = a )
46 41 45 jca 
 |-  ( ( V e. W /\ a C_ ( Pairs ` V ) ) -> ( ( Vtx ` <. V , ( _I |` a ) >. ) = V /\ ( Edg ` <. V , ( _I |` a ) >. ) = a ) )
47 46 ancoms 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( ( Vtx ` <. V , ( _I |` a ) >. ) = V /\ ( Edg ` <. V , ( _I |` a ) >. ) = a ) )
48 35 39 47 rspcedvd 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> E. q e. USPGraph ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) )
49 9 48 jca 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( V = V /\ E. q e. USPGraph ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) ) )
50 2 eleq2i 
 |-  ( <. V , a >. e. G <-> <. V , a >. e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } )
51 30 anim1ci 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( V e. W /\ a e. _V ) )
52 eqeq1 
 |-  ( v = V -> ( v = V <-> V = V ) )
53 52 adantr 
 |-  ( ( v = V /\ e = a ) -> ( v = V <-> V = V ) )
54 eqeq2 
 |-  ( v = V -> ( ( Vtx ` q ) = v <-> ( Vtx ` q ) = V ) )
55 eqeq2 
 |-  ( e = a -> ( ( Edg ` q ) = e <-> ( Edg ` q ) = a ) )
56 54 55 bi2anan9 
 |-  ( ( v = V /\ e = a ) -> ( ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) <-> ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) ) )
57 56 rexbidv 
 |-  ( ( v = V /\ e = a ) -> ( E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) <-> E. q e. USPGraph ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) ) )
58 53 57 anbi12d 
 |-  ( ( v = V /\ e = a ) -> ( ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) <-> ( V = V /\ E. q e. USPGraph ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) ) ) )
59 58 opelopabga 
 |-  ( ( V e. W /\ a e. _V ) -> ( <. V , a >. e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } <-> ( V = V /\ E. q e. USPGraph ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) ) ) )
60 51 59 syl 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( <. V , a >. e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } <-> ( V = V /\ E. q e. USPGraph ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) ) ) )
61 50 60 syl5bb 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( <. V , a >. e. G <-> ( V = V /\ E. q e. USPGraph ( ( Vtx ` q ) = V /\ ( Edg ` q ) = a ) ) ) )
62 49 61 mpbird 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> <. V , a >. e. G )
63 fveq2 
 |-  ( b = <. V , a >. -> ( 2nd ` b ) = ( 2nd ` <. V , a >. ) )
64 63 eqeq2d 
 |-  ( b = <. V , a >. -> ( a = ( 2nd ` b ) <-> a = ( 2nd ` <. V , a >. ) ) )
65 64 adantl 
 |-  ( ( ( a C_ ( Pairs ` V ) /\ V e. W ) /\ b = <. V , a >. ) -> ( a = ( 2nd ` b ) <-> a = ( 2nd ` <. V , a >. ) ) )
66 op2ndg 
 |-  ( ( V e. W /\ a e. _V ) -> ( 2nd ` <. V , a >. ) = a )
67 66 elvd 
 |-  ( V e. W -> ( 2nd ` <. V , a >. ) = a )
68 67 adantl 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> ( 2nd ` <. V , a >. ) = a )
69 68 eqcomd 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> a = ( 2nd ` <. V , a >. ) )
70 62 65 69 rspcedvd 
 |-  ( ( a C_ ( Pairs ` V ) /\ V e. W ) -> E. b e. G a = ( 2nd ` b ) )
71 70 ex 
 |-  ( a C_ ( Pairs ` V ) -> ( V e. W -> E. b e. G a = ( 2nd ` b ) ) )
72 8 71 sylbi 
 |-  ( a e. P -> ( V e. W -> E. b e. G a = ( 2nd ` b ) ) )
73 72 impcom 
 |-  ( ( V e. W /\ a e. P ) -> E. b e. G a = ( 2nd ` b ) )
74 1 2 3 uspgrsprfv 
 |-  ( b e. G -> ( F ` b ) = ( 2nd ` b ) )
75 74 adantl 
 |-  ( ( ( V e. W /\ a e. P ) /\ b e. G ) -> ( F ` b ) = ( 2nd ` b ) )
76 75 eqeq2d 
 |-  ( ( ( V e. W /\ a e. P ) /\ b e. G ) -> ( a = ( F ` b ) <-> a = ( 2nd ` b ) ) )
77 76 rexbidva 
 |-  ( ( V e. W /\ a e. P ) -> ( E. b e. G a = ( F ` b ) <-> E. b e. G a = ( 2nd ` b ) ) )
78 73 77 mpbird 
 |-  ( ( V e. W /\ a e. P ) -> E. b e. G a = ( F ` b ) )
79 78 ralrimiva 
 |-  ( V e. W -> A. a e. P E. b e. G a = ( F ` b ) )
80 dffo3 
 |-  ( F : G -onto-> P <-> ( F : G --> P /\ A. a e. P E. b e. G a = ( F ` b ) ) )
81 5 79 80 sylanbrc 
 |-  ( V e. W -> F : G -onto-> P )