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) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

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