Metamath Proof Explorer

Theorem ltbval

Description: Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses ltbval.c 
|- C = ( T
ltbval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
ltbval.i 
|- ( ph -> I e. V )
ltbval.t 
|- ( ph -> T e. W )
Assertion ltbval 
|- ( ph -> C = { <. x , y >. | ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 ltbval.c 
 |-  C = ( T
2 ltbval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
3 ltbval.i 
 |-  ( ph -> I e. V )
4 ltbval.t 
 |-  ( ph -> T e. W )
5 elex 
 |-  ( T e. W -> T e. _V )
6 elex 
 |-  ( I e. V -> I e. _V )
7 simpr 
 |-  ( ( r = T /\ i = I ) -> i = I )
8 7 oveq2d 
 |-  ( ( r = T /\ i = I ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
9 rabeq 
 |-  ( ( NN0 ^m i ) = ( NN0 ^m I ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
10 8 9 syl 
 |-  ( ( r = T /\ i = I ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
11 10 2 eqtr4di 
 |-  ( ( r = T /\ i = I ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
12 11 sseq2d 
 |-  ( ( r = T /\ i = I ) -> ( { x , y } C_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } <-> { x , y } C_ D ) )
13 simpl 
 |-  ( ( r = T /\ i = I ) -> r = T )
14 13 breqd 
 |-  ( ( r = T /\ i = I ) -> ( z r w <-> z T w ) )
15 14 imbi1d 
 |-  ( ( r = T /\ i = I ) -> ( ( z r w -> ( x ` w ) = ( y ` w ) ) <-> ( z T w -> ( x ` w ) = ( y ` w ) ) ) )
16 7 15 raleqbidv 
 |-  ( ( r = T /\ i = I ) -> ( A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) )
17 16 anbi2d 
 |-  ( ( r = T /\ i = I ) -> ( ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) )
18 7 17 rexeqbidv 
 |-  ( ( r = T /\ i = I ) -> ( E. z e. i ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) ) <-> E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) )
19 12 18 anbi12d 
 |-  ( ( r = T /\ i = I ) -> ( ( { x , y } C_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } /\ E. z e. i ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) ) ) <-> ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) ) )
20 19 opabbidv 
 |-  ( ( r = T /\ i = I ) -> { <. x , y >. | ( { x , y } C_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } /\ E. z e. i ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) ) ) } = { <. x , y >. | ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } )
21 df-ltbag 
 |-   { <. x , y >. | ( { x , y } C_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } /\ E. z e. i ( ( x ` z ) < ( y ` z ) /\ A. w e. i ( z r w -> ( x ` w ) = ( y ` w ) ) ) ) } )
22 vex 
 |-  x e. _V
23 vex 
 |-  y e. _V
24 22 23 prss 
 |-  ( ( x e. D /\ y e. D ) <-> { x , y } C_ D )
25 24 anbi1i 
 |-  ( ( ( x e. D /\ y e. D ) /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) <-> ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) )
26 25 opabbii 
 |-  { <. x , y >. | ( ( x e. D /\ y e. D ) /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } = { <. x , y >. | ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) }
27 ovex 
 |-  ( NN0 ^m I ) e. _V
28 2 27 rabex2 
 |-  D e. _V
29 28 28 xpex 
 |-  ( D X. D ) e. _V
30 opabssxp 
 |-  { <. x , y >. | ( ( x e. D /\ y e. D ) /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } C_ ( D X. D )
31 29 30 ssexi 
 |-  { <. x , y >. | ( ( x e. D /\ y e. D ) /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } e. _V
32 26 31 eqeltrri 
 |-  { <. x , y >. | ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } e. _V
33 20 21 32 ovmpoa 
 |-  ( ( T e. _V /\ I e. _V ) -> ( T . | ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } )
34 5 6 33 syl2an 
 |-  ( ( T e. W /\ I e. V ) -> ( T . | ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } )
35 4 3 34 syl2anc 
 |-  ( ph -> ( T . | ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } )
36 1 35 syl5eq 
 |-  ( ph -> C = { <. x , y >. | ( { x , y } C_ D /\ E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) ) } )