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 0 I | f -1 Fin
psrbagconf1o.s S = y D | y f F
psrbagleadd1.t T = z D | z f F + f G
Assertion psrbagleadd1 F D G D X S X + f G T

Proof

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