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 ) |