Metamath Proof Explorer

Theorem psrbaglefi

Description: There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 25-Jan-2015)

Ref Expression
Hypothesis psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbaglefi 
|- ( ( I e. V /\ F e. D ) -> { y e. D | y oR <_ F } e. Fin )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 df-rab 
 |-  { y e. D | y oR <_ F } = { y | ( y e. D /\ y oR <_ F ) }
3 1 psrbag 
 |-  ( I e. V -> ( y e. D <-> ( y : I --> NN0 /\ ( `' y " NN ) e. Fin ) ) )
4 3 adantr 
 |-  ( ( I e. V /\ F e. D ) -> ( y e. D <-> ( y : I --> NN0 /\ ( `' y " NN ) e. Fin ) ) )
5 simpl 
 |-  ( ( y : I --> NN0 /\ ( `' y " NN ) e. Fin ) -> y : I --> NN0 )
6 4 5 syl6bi 
 |-  ( ( I e. V /\ F e. D ) -> ( y e. D -> y : I --> NN0 ) )
7 6 adantrd 
 |-  ( ( I e. V /\ F e. D ) -> ( ( y e. D /\ y oR <_ F ) -> y : I --> NN0 ) )
8 ss2ixp 
 |-  ( A. x e. I ( 0 ... ( F ` x ) ) C_ NN0 -> X_ x e. I ( 0 ... ( F ` x ) ) C_ X_ x e. I NN0 )
9 fz0ssnn0 
 |-  ( 0 ... ( F ` x ) ) C_ NN0
10 9 a1i 
 |-  ( x e. I -> ( 0 ... ( F ` x ) ) C_ NN0 )
11 8 10 mprg 
 |-  X_ x e. I ( 0 ... ( F ` x ) ) C_ X_ x e. I NN0
12 11 sseli 
 |-  ( y e. X_ x e. I ( 0 ... ( F ` x ) ) -> y e. X_ x e. I NN0 )
13 vex 
 |-  y e. _V
14 13 elixpconst 
 |-  ( y e. X_ x e. I NN0 <-> y : I --> NN0 )
15 12 14 sylib 
 |-  ( y e. X_ x e. I ( 0 ... ( F ` x ) ) -> y : I --> NN0 )
16 15 a1i 
 |-  ( ( I e. V /\ F e. D ) -> ( y e. X_ x e. I ( 0 ... ( F ` x ) ) -> y : I --> NN0 ) )
17 ffn 
 |-  ( y : I --> NN0 -> y Fn I )
18 17 adantl 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> y Fn I )
19 13 elixp 
 |-  ( y e. X_ x e. I ( 0 ... ( F ` x ) ) <-> ( y Fn I /\ A. x e. I ( y ` x ) e. ( 0 ... ( F ` x ) ) ) )
20 19 baib 
 |-  ( y Fn I -> ( y e. X_ x e. I ( 0 ... ( F ` x ) ) <-> A. x e. I ( y ` x ) e. ( 0 ... ( F ` x ) ) ) )
21 18 20 syl 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> ( y e. X_ x e. I ( 0 ... ( F ` x ) ) <-> A. x e. I ( y ` x ) e. ( 0 ... ( F ` x ) ) ) )
22 ffvelrn 
 |-  ( ( y : I --> NN0 /\ x e. I ) -> ( y ` x ) e. NN0 )
23 22 adantll 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) /\ x e. I ) -> ( y ` x ) e. NN0 )
24 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
25 23 24 eleqtrdi 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) /\ x e. I ) -> ( y ` x ) e. ( ZZ>= ` 0 ) )
26 1 psrbagf 
 |-  ( ( I e. V /\ F e. D ) -> F : I --> NN0 )
27 26 adantr 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> F : I --> NN0 )
28 27 ffvelrnda 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) /\ x e. I ) -> ( F ` x ) e. NN0 )
29 28 nn0zd 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) /\ x e. I ) -> ( F ` x ) e. ZZ )
30 elfz5 
 |-  ( ( ( y ` x ) e. ( ZZ>= ` 0 ) /\ ( F ` x ) e. ZZ ) -> ( ( y ` x ) e. ( 0 ... ( F ` x ) ) <-> ( y ` x ) <_ ( F ` x ) ) )
31 25 29 30 syl2anc 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) /\ x e. I ) -> ( ( y ` x ) e. ( 0 ... ( F ` x ) ) <-> ( y ` x ) <_ ( F ` x ) ) )
32 31 ralbidva 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> ( A. x e. I ( y ` x ) e. ( 0 ... ( F ` x ) ) <-> A. x e. I ( y ` x ) <_ ( F ` x ) ) )
33 27 ffnd 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> F Fn I )
34 simpll 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> I e. V )
35 inidm 
 |-  ( I i^i I ) = I
36 eqidd 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) /\ x e. I ) -> ( y ` x ) = ( y ` x ) )
37 eqidd 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
38 18 33 34 34 35 36 37 ofrfval 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> ( y oR <_ F <-> A. x e. I ( y ` x ) <_ ( F ` x ) ) )
39 32 38 bitr4d 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> ( A. x e. I ( y ` x ) e. ( 0 ... ( F ` x ) ) <-> y oR <_ F ) )
40 1 psrbaglecl 
 |-  ( ( I e. V /\ ( F e. D /\ y : I --> NN0 /\ y oR <_ F ) ) -> y e. D )
41 40 3exp2 
 |-  ( I e. V -> ( F e. D -> ( y : I --> NN0 -> ( y oR <_ F -> y e. D ) ) ) )
42 41 imp31 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> ( y oR <_ F -> y e. D ) )
43 42 pm4.71rd 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> ( y oR <_ F <-> ( y e. D /\ y oR <_ F ) ) )
44 21 39 43 3bitrrd 
 |-  ( ( ( I e. V /\ F e. D ) /\ y : I --> NN0 ) -> ( ( y e. D /\ y oR <_ F ) <-> y e. X_ x e. I ( 0 ... ( F ` x ) ) ) )
45 44 ex 
 |-  ( ( I e. V /\ F e. D ) -> ( y : I --> NN0 -> ( ( y e. D /\ y oR <_ F ) <-> y e. X_ x e. I ( 0 ... ( F ` x ) ) ) ) )
46 7 16 45 pm5.21ndd 
 |-  ( ( I e. V /\ F e. D ) -> ( ( y e. D /\ y oR <_ F ) <-> y e. X_ x e. I ( 0 ... ( F ` x ) ) ) )
47 46 abbi1dv 
 |-  ( ( I e. V /\ F e. D ) -> { y | ( y e. D /\ y oR <_ F ) } = X_ x e. I ( 0 ... ( F ` x ) ) )
48 2 47 syl5eq 
 |-  ( ( I e. V /\ F e. D ) -> { y e. D | y oR <_ F } = X_ x e. I ( 0 ... ( F ` x ) ) )
49 simpr 
 |-  ( ( I e. V /\ F e. D ) -> F e. D )
50 cnveq 
 |-  ( f = F -> `' f = `' F )
51 50 imaeq1d 
 |-  ( f = F -> ( `' f " NN ) = ( `' F " NN ) )
52 51 eleq1d 
 |-  ( f = F -> ( ( `' f " NN ) e. Fin <-> ( `' F " NN ) e. Fin ) )
53 52 1 elrab2 
 |-  ( F e. D <-> ( F e. ( NN0 ^m I ) /\ ( `' F " NN ) e. Fin ) )
54 49 53 sylib 
 |-  ( ( I e. V /\ F e. D ) -> ( F e. ( NN0 ^m I ) /\ ( `' F " NN ) e. Fin ) )
55 54 simprd 
 |-  ( ( I e. V /\ F e. D ) -> ( `' F " NN ) e. Fin )
56 fzfid 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. I ) -> ( 0 ... ( F ` x ) ) e. Fin )
57 simpl 
 |-  ( ( I e. V /\ F e. D ) -> I e. V )
58 57 26 jca 
 |-  ( ( I e. V /\ F e. D ) -> ( I e. V /\ F : I --> NN0 ) )
59 frnnn0supp 
 |-  ( ( I e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )
60 eqimss 
 |-  ( ( F supp 0 ) = ( `' F " NN ) -> ( F supp 0 ) C_ ( `' F " NN ) )
61 58 59 60 3syl 
 |-  ( ( I e. V /\ F e. D ) -> ( F supp 0 ) C_ ( `' F " NN ) )
62 c0ex 
 |-  0 e. _V
63 62 a1i 
 |-  ( ( I e. V /\ F e. D ) -> 0 e. _V )
64 26 61 57 63 suppssr 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( F ` x ) = 0 )
65 64 oveq2d 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( 0 ... ( F ` x ) ) = ( 0 ... 0 ) )
66 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
67 65 66 syl6eq 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( 0 ... ( F ` x ) ) = { 0 } )
68 eqimss 
 |-  ( ( 0 ... ( F ` x ) ) = { 0 } -> ( 0 ... ( F ` x ) ) C_ { 0 } )
69 67 68 syl 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( 0 ... ( F ` x ) ) C_ { 0 } )
70 55 56 69 ixpfi2 
 |-  ( ( I e. V /\ F e. D ) -> X_ x e. I ( 0 ... ( F ` x ) ) e. Fin )
71 48 70 eqeltrd 
 |-  ( ( I e. V /\ F e. D ) -> { y e. D | y oR <_ F } e. Fin )