Metamath Proof Explorer

Theorem psrbagleadd1

Description: The analogue of " X <_ F implies X + G <_ F + G " (compare leadd1d ) for bags. (Contributed by SN, 2-May-2025)

Ref Expression
Hypotheses psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrbagconf1o.s 
|- S = { y e. D | y oR <_ F }
psrbagleadd1.t 
|- T = { z e. D | z oR <_ ( F oF + G ) }
Assertion psrbagleadd1 
|- ( ( F e. D /\ G e. D /\ X e. S ) -> ( X oF + G ) e. T )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 psrbagconf1o.s 
 |-  S = { y e. D | y oR <_ F }
3 psrbagleadd1.t 
 |-  T = { z e. D | z oR <_ ( F oF + G ) }
4 elrabi 
 |-  ( X e. { y e. D | y oR <_ F } -> X e. D )
5 4 2 eleq2s 
 |-  ( X e. S -> X e. D )
6 5 3ad2ant3 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> X e. D )
7 simp2 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> G e. D )
8 1 psrbagaddcl 
 |-  ( ( X e. D /\ G e. D ) -> ( X oF + G ) e. D )
9 6 7 8 syl2anc 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> ( X oF + G ) e. D )
10 1 psrbagf 
 |-  ( X e. D -> X : I --> NN0 )
11 6 10 syl 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> X : I --> NN0 )
12 11 ffvelcdmda 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( X ` x ) e. NN0 )
13 12 nn0red 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( X ` x ) e. RR )
14 1 psrbagf 
 |-  ( F e. D -> F : I --> NN0 )
15 14 3ad2ant1 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> F : I --> NN0 )
16 15 ffvelcdmda 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( F ` x ) e. NN0 )
17 16 nn0red 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( F ` x ) e. RR )
18 1 psrbagf 
 |-  ( G e. D -> G : I --> NN0 )
19 18 3ad2ant2 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> G : I --> NN0 )
20 19 ffvelcdmda 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( G ` x ) e. NN0 )
21 20 nn0red 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( G ` x ) e. RR )
22 breq1 
 |-  ( y = X -> ( y oR <_ F <-> X oR <_ F ) )
23 22 2 elrab2 
 |-  ( X e. S <-> ( X e. D /\ X oR <_ F ) )
24 23 simprbi 
 |-  ( X e. S -> X oR <_ F )
25 24 3ad2ant3 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> X oR <_ F )
26 10 ffnd 
 |-  ( X e. D -> X Fn I )
27 5 26 syl 
 |-  ( X e. S -> X Fn I )
28 27 3ad2ant3 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> X Fn I )
29 14 ffnd 
 |-  ( F e. D -> F Fn I )
30 29 3ad2ant1 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> F Fn I )
31 id 
 |-  ( F e. D -> F e. D )
32 31 29 fndmexd 
 |-  ( F e. D -> I e. _V )
33 32 3ad2ant1 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> I e. _V )
34 inidm 
 |-  ( I i^i I ) = I
35 eqidd 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( X ` x ) = ( X ` x ) )
36 eqidd 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
37 28 30 33 33 34 35 36 ofrfval 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> ( X oR <_ F <-> A. x e. I ( X ` x ) <_ ( F ` x ) ) )
38 25 37 mpbid 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> A. x e. I ( X ` x ) <_ ( F ` x ) )
39 38 r19.21bi 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( X ` x ) <_ ( F ` x ) )
40 13 17 21 39 leadd1dd 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( ( X ` x ) + ( G ` x ) ) <_ ( ( F ` x ) + ( G ` x ) ) )
41 40 ralrimiva 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> A. x e. I ( ( X ` x ) + ( G ` x ) ) <_ ( ( F ` x ) + ( G ` x ) ) )
42 1 psrbagf 
 |-  ( ( X oF + G ) e. D -> ( X oF + G ) : I --> NN0 )
43 42 ffnd 
 |-  ( ( X oF + G ) e. D -> ( X oF + G ) Fn I )
44 9 43 syl 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> ( X oF + G ) Fn I )
45 1 psrbagaddcl 
 |-  ( ( F e. D /\ G e. D ) -> ( F oF + G ) e. D )
46 45 3adant3 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> ( F oF + G ) e. D )
47 1 psrbagf 
 |-  ( ( F oF + G ) e. D -> ( F oF + G ) : I --> NN0 )
48 47 ffnd 
 |-  ( ( F oF + G ) e. D -> ( F oF + G ) Fn I )
49 46 48 syl 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> ( F oF + G ) Fn I )
50 18 ffnd 
 |-  ( G e. D -> G Fn I )
51 50 3ad2ant2 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> G Fn I )
52 eqidd 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( G ` x ) = ( G ` x ) )
53 28 51 33 33 34 35 52 ofval 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( ( X oF + G ) ` x ) = ( ( X ` x ) + ( G ` x ) ) )
54 30 51 33 33 34 36 52 ofval 
 |-  ( ( ( F e. D /\ G e. D /\ X e. S ) /\ x e. I ) -> ( ( F oF + G ) ` x ) = ( ( F ` x ) + ( G ` x ) ) )
55 44 49 33 33 34 53 54 ofrfval 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> ( ( X oF + G ) oR <_ ( F oF + G ) <-> A. x e. I ( ( X ` x ) + ( G ` x ) ) <_ ( ( F ` x ) + ( G ` x ) ) ) )
56 41 55 mpbird 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> ( X oF + G ) oR <_ ( F oF + G ) )
57 breq1 
 |-  ( z = ( X oF + G ) -> ( z oR <_ ( F oF + G ) <-> ( X oF + G ) oR <_ ( F oF + G ) ) )
58 57 3 elrab2 
 |-  ( ( X oF + G ) e. T <-> ( ( X oF + G ) e. D /\ ( X oF + G ) oR <_ ( F oF + G ) ) )
59 9 56 58 sylanbrc 
 |-  ( ( F e. D /\ G e. D /\ X e. S ) -> ( X oF + G ) e. T )