This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrbagcon

Description: The analogue of the statement " 0 <_ G <_ F implies 0 <_ F - G <_ F " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014) 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 psrbagcon 
|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 1 psrbagf 
 |-  ( F e. D -> F : I --> NN0 )
3 2 ffnd 
 |-  ( F e. D -> F Fn I )
4 3 3ad2ant1 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F Fn I )
5 simp2 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G : I --> NN0 )
6 5 ffnd 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G Fn I )
7 id 
 |-  ( F e. D -> F e. D )
8 7 3 fndmexd 
 |-  ( F e. D -> I e. _V )
9 8 3ad2ant1 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> I e. _V )
10 inidm 
 |-  ( I i^i I ) = I
11 4 6 9 9 10 offn 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F oF - G ) Fn I )
12 eqidd 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
13 eqidd 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) = ( G ` x ) )
14 4 6 9 9 10 12 13 ofval 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( F oF - G ) ` x ) = ( ( F ` x ) - ( G ` x ) ) )
15 simp3 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G oR <_ F )
16 6 4 9 9 10 13 12 ofrfval 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( G oR <_ F <-> A. x e. I ( G ` x ) <_ ( F ` x ) ) )
17 15 16 mpbid 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> A. x e. I ( G ` x ) <_ ( F ` x ) )
18 17 r19.21bi 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) <_ ( F ` x ) )
19 5 ffvelcdmda 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) e. NN0 )
20 2 3ad2ant1 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F : I --> NN0 )
21 20 ffvelcdmda 
 |-  ( ( ( 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 19 21 22 syl2anc 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( G ` x ) <_ ( F ` x ) <-> ( ( F ` x ) - ( G ` x ) ) e. NN0 ) )
24 18 23 mpbid 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) e. NN0 )
25 14 24 eqeltrd 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( F oF - G ) ` x ) e. NN0 )
26 25 ralrimiva 
 |-  ( ( 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 11 26 27 sylanbrc 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F oF - G ) : I --> NN0 )
29 simp1 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F e. D )
30 1 psrbag 
 |-  ( I e. _V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
31 9 30 syl 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
32 29 31 mpbid 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) )
33 32 simprd 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' F " NN ) e. Fin )
34 19 nn0ge0d 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> 0 <_ ( G ` x ) )
35 21 nn0red 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( F ` x ) e. RR )
36 19 nn0red 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) e. RR )
37 35 36 subge02d 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( 0 <_ ( G ` x ) <-> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) )
38 34 37 mpbid 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) )
39 38 ralrimiva 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> A. x e. I ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) )
40 11 4 9 9 10 14 12 ofrfval 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) oR <_ F <-> A. x e. I ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) )
41 39 40 mpbird 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F oF - G ) oR <_ F )
42 1 psrbaglesupp 
 |-  ( ( F e. D /\ ( F oF - G ) : I --> NN0 /\ ( F oF - G ) oR <_ F ) -> ( `' ( F oF - G ) " NN ) C_ ( `' F " NN ) )
43 29 28 41 42 syl3anc 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' ( F oF - G ) " NN ) C_ ( `' F " NN ) )
44 33 43 ssfid 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' ( F oF - G ) " NN ) e. Fin )
45 1 psrbag 
 |-  ( I e. _V -> ( ( F oF - G ) e. D <-> ( ( F oF - G ) : I --> NN0 /\ ( `' ( F oF - G ) " NN ) e. Fin ) ) )
46 9 45 syl 
 |-  ( ( 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 ) ) )
47 28 44 46 mpbir2and 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F oF - G ) e. D )
48 47 41 jca 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )