Metamath Proof Explorer

Theorem ltbwe

Description: The finite bag order is a well-order, given a well-order of the index set. (Contributed by Mario Carneiro, 2-Jun-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 )
ltbwe.w 
|- ( ph -> T We I )
Assertion ltbwe 
|- ( ph -> C We D )

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 ltbwe.w 
 |-  ( ph -> T We I )
6 eqid 
 |-  { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } = { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) }
7 breq1 
 |-  ( h = x -> ( h finSupp 0 <-> x finSupp 0 ) )
8 7 cbvrabv 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { x e. ( NN0 ^m I ) | x finSupp 0 }
9 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
10 ltweuz 
 |-  < We ( ZZ>= ` 0 )
11 weeq2 
 |-  ( NN0 = ( ZZ>= ` 0 ) -> ( < We NN0 <-> < We ( ZZ>= ` 0 ) ) )
12 10 11 mpbiri 
 |-  ( NN0 = ( ZZ>= ` 0 ) -> < We NN0 )
13 9 12 mp1i 
 |-  ( ph -> < We NN0 )
14 0nn0 
 |-  0 e. NN0
15 ne0i 
 |-  ( 0 e. NN0 -> NN0 =/= (/) )
16 14 15 mp1i 
 |-  ( ph -> NN0 =/= (/) )
17 eqid 
 |-  OrdIso ( T , I ) = OrdIso ( T , I )
18 0z 
 |-  0 e. ZZ
19 hashgval2 
 |-  ( # |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
20 18 19 om2uzoi 
 |-  ( # |` _om ) = OrdIso ( < , ( ZZ>= ` 0 ) )
21 oieq2 
 |-  ( NN0 = ( ZZ>= ` 0 ) -> OrdIso ( < , NN0 ) = OrdIso ( < , ( ZZ>= ` 0 ) ) )
22 9 21 ax-mp 
 |-  OrdIso ( < , NN0 ) = OrdIso ( < , ( ZZ>= ` 0 ) )
23 20 22 eqtr4i 
 |-  ( # |` _om ) = OrdIso ( < , NN0 )
24 peano1 
 |-  (/) e. _om
25 fvres 
 |-  ( (/) e. _om -> ( ( # |` _om ) ` (/) ) = ( # ` (/) ) )
26 24 25 ax-mp 
 |-  ( ( # |` _om ) ` (/) ) = ( # ` (/) )
27 hash0 
 |-  ( # ` (/) ) = 0
28 26 27 eqtr2i 
 |-  0 = ( ( # |` _om ) ` (/) )
29 6 8 5 13 16 17 23 28 wemapwe 
 |-  ( ph -> { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } We { h e. ( NN0 ^m I ) | h finSupp 0 } )
30 elmapfun 
 |-  ( h e. ( NN0 ^m I ) -> Fun h )
31 30 adantl 
 |-  ( ( ph /\ h e. ( NN0 ^m I ) ) -> Fun h )
32 simpr 
 |-  ( ( ph /\ h e. ( NN0 ^m I ) ) -> h e. ( NN0 ^m I ) )
33 c0ex 
 |-  0 e. _V
34 33 a1i 
 |-  ( ( ph /\ h e. ( NN0 ^m I ) ) -> 0 e. _V )
35 funisfsupp 
 |-  ( ( Fun h /\ h e. ( NN0 ^m I ) /\ 0 e. _V ) -> ( h finSupp 0 <-> ( h supp 0 ) e. Fin ) )
36 31 32 34 35 syl3anc 
 |-  ( ( ph /\ h e. ( NN0 ^m I ) ) -> ( h finSupp 0 <-> ( h supp 0 ) e. Fin ) )
37 elmapi 
 |-  ( h e. ( NN0 ^m I ) -> h : I --> NN0 )
38 frnnn0supp 
 |-  ( ( I e. V /\ h : I --> NN0 ) -> ( h supp 0 ) = ( `' h " NN ) )
39 38 eleq1d 
 |-  ( ( I e. V /\ h : I --> NN0 ) -> ( ( h supp 0 ) e. Fin <-> ( `' h " NN ) e. Fin ) )
40 3 37 39 syl2an 
 |-  ( ( ph /\ h e. ( NN0 ^m I ) ) -> ( ( h supp 0 ) e. Fin <-> ( `' h " NN ) e. Fin ) )
41 36 40 bitr2d 
 |-  ( ( ph /\ h e. ( NN0 ^m I ) ) -> ( ( `' h " NN ) e. Fin <-> h finSupp 0 ) )
42 41 rabbidva 
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | h finSupp 0 } )
43 2 42 syl5eq 
 |-  ( ph -> D = { h e. ( NN0 ^m I ) | h finSupp 0 } )
44 weeq2 
 |-  ( D = { h e. ( NN0 ^m I ) | h finSupp 0 } -> ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } We D <-> { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } We { h e. ( NN0 ^m I ) | h finSupp 0 } ) )
45 43 44 syl 
 |-  ( ph -> ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } We D <-> { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } We { h e. ( NN0 ^m I ) | h finSupp 0 } ) )
46 29 45 mpbird 
 |-  ( ph -> { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } We D )
47 weinxp 
 |-  ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } We D <-> ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } i^i ( D X. D ) ) We D )
48 46 47 sylib 
 |-  ( ph -> ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } i^i ( D X. D ) ) We D )
49 1 2 3 4 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 ) ) ) ) } )
50 df-xp 
 |-  ( D X. D ) = { <. x , y >. | ( x e. D /\ y e. D ) }
51 vex 
 |-  x e. _V
52 vex 
 |-  y e. _V
53 51 52 prss 
 |-  ( ( x e. D /\ y e. D ) <-> { x , y } C_ D )
54 53 opabbii 
 |-  { <. x , y >. | ( x e. D /\ y e. D ) } = { <. x , y >. | { x , y } C_ D }
55 50 54 eqtr2i 
 |-  { <. x , y >. | { x , y } C_ D } = ( D X. D )
56 55 ineq1i 
 |-  ( { <. x , y >. | { x , y } C_ D } i^i { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } ) = ( ( D X. D ) i^i { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } )
57 inopab 
 |-  ( { <. x , y >. | { x , y } C_ D } i^i { <. x , y >. | 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 ) ) ) ) }
58 incom 
 |-  ( ( D X. D ) i^i { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } ) = ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } i^i ( D X. D ) )
59 56 57 58 3eqtr3i 
 |-  { <. 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 ) ) ) ) } = ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } i^i ( D X. D ) )
60 49 59 eqtrdi 
 |-  ( ph -> C = ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } i^i ( D X. D ) ) )
61 weeq1 
 |-  ( C = ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } i^i ( D X. D ) ) -> ( C We D <-> ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } i^i ( D X. D ) ) We D ) )
62 60 61 syl 
 |-  ( ph -> ( C We D <-> ( { <. x , y >. | E. z e. I ( ( x ` z ) < ( y ` z ) /\ A. w e. I ( z T w -> ( x ` w ) = ( y ` w ) ) ) } i^i ( D X. D ) ) We D ) )
63 48 62 mpbird 
 |-  ( ph -> C We D )