Metamath Proof Explorer


Theorem psrbaglefiOLD

Description: Obsolete version of psrbaglefi as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 25-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis psrbag.d
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbaglefiOLD
|- ( ( 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 psrbagfOLD
 |-  ( ( 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 psrbagleclOLD
 |-  ( ( 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 eqtrdi
 |-  ( ( ( 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 )