Step |
Hyp |
Ref |
Expression |
1 |
|
psrbag.d |
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |
2 |
|
simpr1 |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F e. D ) |
3 |
1
|
psrbag |
|- ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) ) |
4 |
3
|
adantr |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) ) |
5 |
2 4
|
mpbid |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) |
6 |
5
|
simpld |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F : I --> NN0 ) |
7 |
6
|
ffnd |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F Fn I ) |
8 |
|
simpr2 |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G : I --> NN0 ) |
9 |
8
|
ffnd |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G Fn I ) |
10 |
|
simpl |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> I e. V ) |
11 |
|
inidm |
|- ( I i^i I ) = I |
12 |
7 9 10 10 11
|
offn |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F oF - G ) Fn I ) |
13 |
|
eqidd |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) ) |
14 |
|
eqidd |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( G ` x ) = ( G ` x ) ) |
15 |
7 9 10 10 11 13 14
|
ofval |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( F oF - G ) ` x ) = ( ( F ` x ) - ( G ` x ) ) ) |
16 |
|
simpr3 |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G oR <_ F ) |
17 |
9 7 10 10 11 14 13
|
ofrfval |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( G oR <_ F <-> A. x e. I ( G ` x ) <_ ( F ` x ) ) ) |
18 |
16 17
|
mpbid |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> A. x e. I ( G ` x ) <_ ( F ` x ) ) |
19 |
18
|
r19.21bi |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( G ` x ) <_ ( F ` x ) ) |
20 |
8
|
ffvelrnda |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( G ` x ) e. NN0 ) |
21 |
6
|
ffvelrnda |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( F ` x ) e. NN0 ) |
22 |
|
nn0sub |
|- ( ( ( G ` x ) e. NN0 /\ ( F ` x ) e. NN0 ) -> ( ( G ` x ) <_ ( F ` x ) <-> ( ( F ` x ) - ( G ` x ) ) e. NN0 ) ) |
23 |
20 21 22
|
syl2anc |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( G ` x ) <_ ( F ` x ) <-> ( ( F ` x ) - ( G ` x ) ) e. NN0 ) ) |
24 |
19 23
|
mpbid |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) e. NN0 ) |
25 |
15 24
|
eqeltrd |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( F oF - G ) ` x ) e. NN0 ) |
26 |
25
|
ralrimiva |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> A. x e. I ( ( F oF - G ) ` x ) e. NN0 ) |
27 |
|
ffnfv |
|- ( ( F oF - G ) : I --> NN0 <-> ( ( F oF - G ) Fn I /\ A. x e. I ( ( F oF - G ) ` x ) e. NN0 ) ) |
28 |
12 26 27
|
sylanbrc |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F oF - G ) : I --> NN0 ) |
29 |
5
|
simprd |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' F " NN ) e. Fin ) |
30 |
20
|
nn0ge0d |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> 0 <_ ( G ` x ) ) |
31 |
|
nn0re |
|- ( ( F ` x ) e. NN0 -> ( F ` x ) e. RR ) |
32 |
|
nn0re |
|- ( ( G ` x ) e. NN0 -> ( G ` x ) e. RR ) |
33 |
|
subge02 |
|- ( ( ( F ` x ) e. RR /\ ( G ` x ) e. RR ) -> ( 0 <_ ( G ` x ) <-> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) ) |
34 |
31 32 33
|
syl2an |
|- ( ( ( F ` x ) e. NN0 /\ ( G ` x ) e. NN0 ) -> ( 0 <_ ( G ` x ) <-> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) ) |
35 |
21 20 34
|
syl2anc |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( 0 <_ ( G ` x ) <-> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) ) |
36 |
30 35
|
mpbid |
|- ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) |
37 |
36
|
ralrimiva |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> A. x e. I ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) |
38 |
12 7 10 10 11 15 13
|
ofrfval |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( ( F oF - G ) oR <_ F <-> A. x e. I ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) ) |
39 |
37 38
|
mpbird |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F oF - G ) oR <_ F ) |
40 |
1
|
psrbaglesuppOLD |
|- ( ( I e. V /\ ( F e. D /\ ( F oF - G ) : I --> NN0 /\ ( F oF - G ) oR <_ F ) ) -> ( `' ( F oF - G ) " NN ) C_ ( `' F " NN ) ) |
41 |
10 2 28 39 40
|
syl13anc |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' ( F oF - G ) " NN ) C_ ( `' F " NN ) ) |
42 |
29 41
|
ssfid |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' ( F oF - G ) " NN ) e. Fin ) |
43 |
1
|
psrbag |
|- ( I e. V -> ( ( F oF - G ) e. D <-> ( ( F oF - G ) : I --> NN0 /\ ( `' ( F oF - G ) " NN ) e. Fin ) ) ) |
44 |
43
|
adantr |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( ( F oF - G ) e. D <-> ( ( F oF - G ) : I --> NN0 /\ ( `' ( F oF - G ) " NN ) e. Fin ) ) ) |
45 |
28 42 44
|
mpbir2and |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F oF - G ) e. D ) |
46 |
45 39
|
jca |
|- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) ) |