MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iseupa Structured version   Unicode version

Theorem iseupa 23411
Description: The property " <. F ,  P >. is an Eulerian path on the graph  <. V ,  E >.". An Eulerian path is defined as bijection  F from the edges to a set  1 ... N a function  P :
( 0 ... N
) --> V into the vertices such that for each 
1  <_  k  <_  N,  F ( k ) is an edge from  P ( k  -  1 ) to  P
( k ). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.)
Assertion
Ref Expression
iseupa  |-  ( dom 
E  =  A  -> 
( F ( V EulPaths  E ) P  <->  ( V UMGrph  E  /\  E. n  e. 
NN0  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) ) ) )
Distinct variable groups:    k, n, A    k, E, n    k, F, n    P, k, n   
k, V, n

Proof of Theorem iseupa
Dummy variables  e 
f  p  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-eupa 23409 . . . 4  |- EulPaths  =  ( v  e.  _V , 
e  e.  _V  |->  {
<. f ,  p >.  |  ( v UMGrph  e  /\  E. n  e.  NN0  (
f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n
) ( e `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) } )
21brovmpt2ex 6732 . . 3  |-  ( F ( V EulPaths  E ) P  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) ) )
32a1i 11 . 2  |-  ( dom 
E  =  A  -> 
( F ( V EulPaths  E ) P  -> 
( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) ) ) )
4 relumgra 23073 . . . . 5  |-  Rel UMGrph
5 brrelex12 4865 . . . . 5  |-  ( ( Rel UMGrph  /\  V UMGrph  E )  ->  ( V  e.  _V  /\  E  e.  _V )
)
64, 5mpan 665 . . . 4  |-  ( V UMGrph  E  ->  ( V  e. 
_V  /\  E  e.  _V ) )
7 f1of 5631 . . . . . . . 8  |-  ( F : ( 1 ... n ) -1-1-onto-> A  ->  F :
( 1 ... n
) --> A )
8 ovex 6107 . . . . . . . 8  |-  ( 1 ... n )  e. 
_V
9 fex 5939 . . . . . . . 8  |-  ( ( F : ( 1 ... n ) --> A  /\  ( 1 ... n )  e.  _V )  ->  F  e.  _V )
107, 8, 9sylancl 657 . . . . . . 7  |-  ( F : ( 1 ... n ) -1-1-onto-> A  ->  F  e.  _V )
11 ovex 6107 . . . . . . . 8  |-  ( 0 ... n )  e. 
_V
12 fex 5939 . . . . . . . 8  |-  ( ( P : ( 0 ... n ) --> V  /\  ( 0 ... n )  e.  _V )  ->  P  e.  _V )
1311, 12mpan2 666 . . . . . . 7  |-  ( P : ( 0 ... n ) --> V  ->  P  e.  _V )
1410, 13anim12i 563 . . . . . 6  |-  ( ( F : ( 1 ... n ) -1-1-onto-> A  /\  P : ( 0 ... n ) --> V )  ->  ( F  e. 
_V  /\  P  e.  _V ) )
15143adant3 1003 . . . . 5  |-  ( ( F : ( 1 ... n ) -1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( F `
 k ) )  =  { ( P `
 ( k  - 
1 ) ) ,  ( P `  k
) } )  -> 
( F  e.  _V  /\  P  e.  _V )
)
1615rexlimivw 2829 . . . 4  |-  ( E. n  e.  NN0  ( F : ( 1 ... n ) -1-1-onto-> A  /\  P :
( 0 ... n
) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( F `
 k ) )  =  { ( P `
 ( k  - 
1 ) ) ,  ( P `  k
) } )  -> 
( F  e.  _V  /\  P  e.  _V )
)
176, 16anim12i 563 . . 3  |-  ( ( V UMGrph  E  /\  E. n  e.  NN0  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) )  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) ) )
1817a1i 11 . 2  |-  ( dom 
E  =  A  -> 
( ( V UMGrph  E  /\  E. n  e.  NN0  ( F : ( 1 ... n ) -1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( F `
 k ) )  =  { ( P `
 ( k  - 
1 ) ) ,  ( P `  k
) } ) )  ->  ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) ) ) )
191a1i 11 . . . . . 6  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  -> EulPaths  =  ( v  e. 
_V ,  e  e. 
_V  |->  { <. f ,  p >.  |  (
v UMGrph  e  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) ) } ) )
20 breq12 4287 . . . . . . . . 9  |-  ( ( v  =  V  /\  e  =  E )  ->  ( v UMGrph  e  <->  V UMGrph  E ) )
2120adantl 463 . . . . . . . 8  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( v UMGrph  e  <->  V UMGrph  E ) )
22 simprr 751 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
e  =  E )
2322dmeqd 5031 . . . . . . . . . . . 12  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  ->  dom  e  =  dom  E )
24 simplr 749 . . . . . . . . . . . 12  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  ->  dom  E  =  A )
2523, 24eqtrd 2467 . . . . . . . . . . 11  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  ->  dom  e  =  A
)
26 f1oeq3 5624 . . . . . . . . . . 11  |-  ( dom  e  =  A  -> 
( f : ( 1 ... n ) -1-1-onto-> dom  e  <->  f : ( 1 ... n ) -1-1-onto-> A ) )
2725, 26syl 16 . . . . . . . . . 10  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( f : ( 1 ... n ) -1-1-onto-> dom  e  <->  f : ( 1 ... n ) -1-1-onto-> A ) )
28 feq3 5534 . . . . . . . . . . 11  |-  ( v  =  V  ->  (
p : ( 0 ... n ) --> v  <-> 
p : ( 0 ... n ) --> V ) )
2928ad2antrl 722 . . . . . . . . . 10  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( p : ( 0 ... n ) --> v  <->  p : ( 0 ... n ) --> V ) )
3022fveq1d 5683 . . . . . . . . . . . 12  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( e `  (
f `  k )
)  =  ( E `
 ( f `  k ) ) )
3130eqeq1d 2443 . . . . . . . . . . 11  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( ( e `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) }  <-> 
( E `  (
f `  k )
)  =  { ( p `  ( k  -  1 ) ) ,  ( p `  k ) } ) )
3231ralbidv 2727 . . . . . . . . . 10  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( A. k  e.  ( 1 ... n
) ( e `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) }  <->  A. k  e.  (
1 ... n ) ( E `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) )
3327, 29, 323anbi123d 1284 . . . . . . . . 9  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( ( f : ( 1 ... n
)
-1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } )  <->  ( f : ( 1 ... n ) -1-1-onto-> A  /\  p : ( 0 ... n
) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) ) )
3433rexbidv 2728 . . . . . . . 8  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( E. n  e. 
NN0  ( f : ( 1 ... n
)
-1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } )  <->  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) )
3521, 34anbi12d 705 . . . . . . 7  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  -> 
( ( v UMGrph  e  /\  E. n  e.  NN0  ( f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n
) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) )  <-> 
( V UMGrph  E  /\  E. n  e.  NN0  (
f : ( 1 ... n ) -1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) ) ) )
3635opabbidv 4345 . . . . . 6  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( v  =  V  /\  e  =  E ) )  ->  { <. f ,  p >.  |  ( v UMGrph  e  /\  E. n  e.  NN0  ( f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n
) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) ) }  =  { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) } )
37 simplll 752 . . . . . 6  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  V  e.  _V )
38 simpllr 753 . . . . . 6  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  E  e.  _V )
39 simpr 458 . . . . . . . . . . . . . . 15  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  dom  E  =  A )
40 dmexg 6500 . . . . . . . . . . . . . . . 16  |-  ( E  e.  _V  ->  dom  E  e.  _V )
4138, 40syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  dom  E  e.  _V )
4239, 41eqeltrrd 2510 . . . . . . . . . . . . . 14  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  A  e.  _V )
4342adantr 462 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  A  e.  _V )
44 nnex 10318 . . . . . . . . . . . . . 14  |-  NN  e.  _V
4544a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  NN  e.  _V )
46 simpr1 989 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  f : ( 1 ... n ) -1-1-onto-> A )
47 f1of 5631 . . . . . . . . . . . . . 14  |-  ( f : ( 1 ... n ) -1-1-onto-> A  ->  f :
( 1 ... n
) --> A )
4846, 47syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  f : ( 1 ... n ) --> A )
49 elfznn 11467 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 1 ... n )  ->  k  e.  NN )
5049ssriv 3350 . . . . . . . . . . . . . 14  |-  ( 1 ... n )  C_  NN
5150a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  (
1 ... n )  C_  NN )
52 elpm2r 7220 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  _V  /\  NN  e.  _V )  /\  ( f : ( 1 ... n ) --> A  /\  ( 1 ... n )  C_  NN ) )  ->  f  e.  ( A  ^pm  NN ) )
5343, 45, 48, 51, 52syl22anc 1214 . . . . . . . . . . . 12  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  f  e.  ( A  ^pm  NN ) )
5437adantr 462 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  V  e.  _V )
55 nn0ex 10575 . . . . . . . . . . . . . 14  |-  NN0  e.  _V
5655a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  NN0  e.  _V )
57 simpr2 990 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  p : ( 0 ... n ) --> V )
58 elfznn0 11470 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... n )  ->  k  e.  NN0 )
5958ssriv 3350 . . . . . . . . . . . . . 14  |-  ( 0 ... n )  C_  NN0
6059a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  (
0 ... n )  C_  NN0 )
61 elpm2r 7220 . . . . . . . . . . . . 13  |-  ( ( ( V  e.  _V  /\ 
NN0  e.  _V )  /\  ( p : ( 0 ... n ) --> V  /\  ( 0 ... n )  C_  NN0 ) )  ->  p  e.  ( V  ^pm  NN0 )
)
6254, 56, 57, 60, 61syl22anc 1214 . . . . . . . . . . . 12  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  p  e.  ( V  ^pm  NN0 )
)
6353, 62jca 529 . . . . . . . . . . 11  |-  ( ( ( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  /\  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  (
f  e.  ( A 
^pm  NN )  /\  p  e.  ( V  ^pm  NN0 )
) )
6463ex 434 . . . . . . . . . 10  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  ( ( f : ( 1 ... n ) -1-1-onto-> A  /\  p : ( 0 ... n
) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } )  -> 
( f  e.  ( A  ^pm  NN )  /\  p  e.  ( V  ^pm  NN0 ) ) ) )
6564rexlimdvw 2836 . . . . . . . . 9  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  ( E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } )  ->  ( f  e.  ( A  ^pm  NN )  /\  p  e.  ( V  ^pm  NN0 ) ) ) )
6665adantld 464 . . . . . . . 8  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  ( ( V UMGrph  E  /\  E. n  e. 
NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  ->  (
f  e.  ( A 
^pm  NN )  /\  p  e.  ( V  ^pm  NN0 )
) ) )
6766ssopab2dv 4608 . . . . . . 7  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) }  C_  {
<. f ,  p >.  |  ( f  e.  ( A  ^pm  NN )  /\  p  e.  ( V  ^pm  NN0 ) ) } )
68 df-xp 4835 . . . . . . . 8  |-  ( ( A  ^pm  NN )  X.  ( V  ^pm  NN0 )
)  =  { <. f ,  p >.  |  ( f  e.  ( A 
^pm  NN )  /\  p  e.  ( V  ^pm  NN0 )
) }
69 ovex 6107 . . . . . . . . 9  |-  ( A 
^pm  NN )  e.  _V
70 ovex 6107 . . . . . . . . 9  |-  ( V 
^pm  NN0 )  e.  _V
7169, 70xpex 6499 . . . . . . . 8  |-  ( ( A  ^pm  NN )  X.  ( V  ^pm  NN0 )
)  e.  _V
7268, 71eqeltrri 2506 . . . . . . 7  |-  { <. f ,  p >.  |  ( f  e.  ( A 
^pm  NN )  /\  p  e.  ( V  ^pm  NN0 )
) }  e.  _V
73 ssexg 4428 . . . . . . 7  |-  ( ( { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n ) -1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) }  C_  {
<. f ,  p >.  |  ( f  e.  ( A  ^pm  NN )  /\  p  e.  ( V  ^pm  NN0 ) ) }  /\  { <. f ,  p >.  |  (
f  e.  ( A 
^pm  NN )  /\  p  e.  ( V  ^pm  NN0 )
) }  e.  _V )  ->  { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) }  e.  _V )
7467, 72, 73sylancl 657 . . . . . 6  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) }  e.  _V )
7519, 36, 37, 38, 74ovmpt2d 6209 . . . . 5  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  ( V EulPaths  E )  =  { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) } )
7675breqd 4293 . . . 4  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  ( F ( V EulPaths  E ) P  <->  F { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  (
f : ( 1 ... n ) -1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) ) } P ) )
77 f1oeq1 5622 . . . . . . . . . 10  |-  ( f  =  F  ->  (
f : ( 1 ... n ) -1-1-onto-> A  <->  F :
( 1 ... n
)
-1-1-onto-> A ) )
7877adantr 462 . . . . . . . . 9  |-  ( ( f  =  F  /\  p  =  P )  ->  ( f : ( 1 ... n ) -1-1-onto-> A  <-> 
F : ( 1 ... n ) -1-1-onto-> A ) )
79 feq1 5532 . . . . . . . . . 10  |-  ( p  =  P  ->  (
p : ( 0 ... n ) --> V  <-> 
P : ( 0 ... n ) --> V ) )
8079adantl 463 . . . . . . . . 9  |-  ( ( f  =  F  /\  p  =  P )  ->  ( p : ( 0 ... n ) --> V  <->  P : ( 0 ... n ) --> V ) )
81 fveq1 5680 . . . . . . . . . . . . 13  |-  ( f  =  F  ->  (
f `  k )  =  ( F `  k ) )
8281fveq2d 5685 . . . . . . . . . . . 12  |-  ( f  =  F  ->  ( E `  ( f `  k ) )  =  ( E `  ( F `  k )
) )
8382adantr 462 . . . . . . . . . . 11  |-  ( ( f  =  F  /\  p  =  P )  ->  ( E `  (
f `  k )
)  =  ( E `
 ( F `  k ) ) )
84 simpr 458 . . . . . . . . . . . . 13  |-  ( ( f  =  F  /\  p  =  P )  ->  p  =  P )
8584fveq1d 5683 . . . . . . . . . . . 12  |-  ( ( f  =  F  /\  p  =  P )  ->  ( p `  (
k  -  1 ) )  =  ( P `
 ( k  - 
1 ) ) )
8684fveq1d 5683 . . . . . . . . . . . 12  |-  ( ( f  =  F  /\  p  =  P )  ->  ( p `  k
)  =  ( P `
 k ) )
8785, 86preq12d 3952 . . . . . . . . . . 11  |-  ( ( f  =  F  /\  p  =  P )  ->  { ( p `  ( k  -  1 ) ) ,  ( p `  k ) }  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } )
8883, 87eqeq12d 2449 . . . . . . . . . 10  |-  ( ( f  =  F  /\  p  =  P )  ->  ( ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) }  <-> 
( E `  ( F `  k )
)  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) )
8988ralbidv 2727 . . . . . . . . 9  |-  ( ( f  =  F  /\  p  =  P )  ->  ( A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) }  <->  A. k  e.  (
1 ... n ) ( E `  ( F `
 k ) )  =  { ( P `
 ( k  - 
1 ) ) ,  ( P `  k
) } ) )
9078, 80, 893anbi123d 1284 . . . . . . . 8  |-  ( ( f  =  F  /\  p  =  P )  ->  ( ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } )  <->  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) ) )
9190rexbidv 2728 . . . . . . 7  |-  ( ( f  =  F  /\  p  =  P )  ->  ( E. n  e. 
NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } )  <->  E. n  e.  NN0  ( F : ( 1 ... n ) -1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( F `
 k ) )  =  { ( P `
 ( k  - 
1 ) ) ,  ( P `  k
) } ) ) )
9291anbi2d 698 . . . . . 6  |-  ( ( f  =  F  /\  p  =  P )  ->  ( ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n ) -1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) )  <->  ( V UMGrph  E  /\  E. n  e. 
NN0  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) ) ) )
93 eqid 2435 . . . . . 6  |-  { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) }  =  { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n ) -1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) }
9492, 93brabga 4594 . . . . 5  |-  ( ( F  e.  _V  /\  P  e.  _V )  ->  ( F { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) } P  <->  ( V UMGrph  E  /\  E. n  e.  NN0  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) ) ) )
9594ad2antlr 721 . . . 4  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  ( F { <. f ,  p >.  |  ( V UMGrph  E  /\  E. n  e.  NN0  (
f : ( 1 ... n ) -1-1-onto-> A  /\  p : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n ) ( E `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) ) } P  <->  ( V UMGrph  E  /\  E. n  e. 
NN0  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) ) ) )
9676, 95bitrd 253 . . 3  |-  ( ( ( ( V  e. 
_V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  /\  dom  E  =  A )  ->  ( F ( V EulPaths  E ) P  <->  ( V UMGrph  E  /\  E. n  e. 
NN0  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) ) ) )
9796expcom 435 . 2  |-  ( dom 
E  =  A  -> 
( ( ( V  e.  _V  /\  E  e.  _V )  /\  ( F  e.  _V  /\  P  e.  _V ) )  -> 
( F ( V EulPaths  E ) P  <->  ( V UMGrph  E  /\  E. n  e. 
NN0  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) ) ) ) )
983, 18, 97pm5.21ndd 354 1  |-  ( dom 
E  =  A  -> 
( F ( V EulPaths  E ) P  <->  ( V UMGrph  E  /\  E. n  e. 
NN0  ( F :
( 1 ... n
)
-1-1-onto-> A  /\  P : ( 0 ... n ) --> V  /\  A. k  e.  ( 1 ... n
) ( E `  ( F `  k ) )  =  { ( P `  ( k  -  1 ) ) ,  ( P `  k ) } ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1757   A.wral 2707   E.wrex 2708   _Vcvv 2964    C_ wss 3318   {cpr 3869   class class class wbr 4282   {copab 4339    X. cxp 4827   dom cdm 4829   Rel wrel 4834   -->wf 5404   -1-1-onto->wf1o 5407   ` cfv 5408  (class class class)co 6082    e. cmpt2 6084    ^pm cpm 7205   0cc0 9272   1c1 9273    - cmin 9585   NNcn 10312   NN0cn0 10569   ...cfz 11426   UMGrph cumg 23071   EulPaths ceup 23408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-1st 6568  df-2nd 6569  df-recs 6820  df-rdg 6854  df-er 7091  df-pm 7207  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-nn 10313  df-n0 10570  df-z 10637  df-uz 10852  df-fz 11427  df-umgra 23072  df-eupa 23409
This theorem is referenced by:  eupagra  23412  eupai  23413  eupatrl  23414  eupa0  23420  eupares  23421  eupap1  23422
  Copyright terms: Public domain W3C validator