Metamath Proof Explorer

Theorem uspgrsprf

Description: The mapping F is a 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, 24-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 uspgrsprf 
|- F : G --> 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 2 eleq2i 
 |-  ( g e. G <-> g e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } )
5 elopab 
 |-  ( g e. { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } <-> E. v E. e ( g = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) )
6 4 5 bitri 
 |-  ( g e. G <-> E. v E. e ( g = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) )
7 uspgrupgr 
 |-  ( q e. USPGraph -> q e. UPGraph )
8 upgredgssspr 
 |-  ( q e. UPGraph -> ( Edg ` q ) C_ ( Pairs ` ( Vtx ` q ) ) )
9 7 8 syl 
 |-  ( q e. USPGraph -> ( Edg ` q ) C_ ( Pairs ` ( Vtx ` q ) ) )
10 9 adantr 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) -> ( Edg ` q ) C_ ( Pairs ` ( Vtx ` q ) ) )
11 simpr 
 |-  ( ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) -> ( Edg ` q ) = e )
12 fveq2 
 |-  ( ( Vtx ` q ) = v -> ( Pairs ` ( Vtx ` q ) ) = ( Pairs ` v ) )
13 12 adantr 
 |-  ( ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) -> ( Pairs ` ( Vtx ` q ) ) = ( Pairs ` v ) )
14 11 13 sseq12d 
 |-  ( ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) -> ( ( Edg ` q ) C_ ( Pairs ` ( Vtx ` q ) ) <-> e C_ ( Pairs ` v ) ) )
15 14 adantl 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) -> ( ( Edg ` q ) C_ ( Pairs ` ( Vtx ` q ) ) <-> e C_ ( Pairs ` v ) ) )
16 10 15 mpbid 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) -> e C_ ( Pairs ` v ) )
17 16 rexlimiva 
 |-  ( E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) -> e C_ ( Pairs ` v ) )
18 17 adantl 
 |-  ( ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) -> e C_ ( Pairs ` v ) )
19 fveq2 
 |-  ( v = V -> ( Pairs ` v ) = ( Pairs ` V ) )
20 19 sseq2d 
 |-  ( v = V -> ( e C_ ( Pairs ` v ) <-> e C_ ( Pairs ` V ) ) )
21 20 adantr 
 |-  ( ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) -> ( e C_ ( Pairs ` v ) <-> e C_ ( Pairs ` V ) ) )
22 18 21 mpbid 
 |-  ( ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) -> e C_ ( Pairs ` V ) )
23 22 adantl 
 |-  ( ( g = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> e C_ ( Pairs ` V ) )
24 vex 
 |-  v e. _V
25 vex 
 |-  e e. _V
26 24 25 op2ndd 
 |-  ( g = <. v , e >. -> ( 2nd ` g ) = e )
27 26 sseq1d 
 |-  ( g = <. v , e >. -> ( ( 2nd ` g ) C_ ( Pairs ` V ) <-> e C_ ( Pairs ` V ) ) )
28 27 adantr 
 |-  ( ( g = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( ( 2nd ` g ) C_ ( Pairs ` V ) <-> e C_ ( Pairs ` V ) ) )
29 23 28 mpbird 
 |-  ( ( g = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( 2nd ` g ) C_ ( Pairs ` V ) )
30 1 eleq2i 
 |-  ( ( 2nd ` g ) e. P <-> ( 2nd ` g ) e. ~P ( Pairs ` V ) )
31 fvex 
 |-  ( 2nd ` g ) e. _V
32 31 elpw 
 |-  ( ( 2nd ` g ) e. ~P ( Pairs ` V ) <-> ( 2nd ` g ) C_ ( Pairs ` V ) )
33 30 32 bitri 
 |-  ( ( 2nd ` g ) e. P <-> ( 2nd ` g ) C_ ( Pairs ` V ) )
34 29 33 sylibr 
 |-  ( ( g = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( 2nd ` g ) e. P )
35 34 exlimivv 
 |-  ( E. v E. e ( g = <. v , e >. /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> ( 2nd ` g ) e. P )
36 6 35 sylbi 
 |-  ( g e. G -> ( 2nd ` g ) e. P )
37 3 36 fmpti 
 |-  F : G --> P