Metamath Proof Explorer

Theorem sge0lempt

Description: If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0lempt.xph ⊢Ⅎxφ
sge0lempt.a ⊢φ→A∈V
sge0lempt.b ⊢φ∧x∈A→B∈0+∞
sge0lempt.c ⊢φ∧x∈A→C∈0+∞
sge0lempt.le ⊢φ∧x∈A→B≤C
Assertion sge0lempt ⊢φ→sum^⁡x∈A⟼B≤sum^⁡x∈A⟼C

Proof

Step Hyp Ref Expression
1 sge0lempt.xph ⊢Ⅎxφ
2 sge0lempt.a ⊢φ→A∈V
3 sge0lempt.b ⊢φ∧x∈A→B∈0+∞
4 sge0lempt.c ⊢φ∧x∈A→C∈0+∞
5 sge0lempt.le ⊢φ∧x∈A→B≤C
6 eqid ⊢x∈A⟼B=x∈A⟼B
7 1 3 6 fmptdf ⊢φ→x∈A⟼B:A⟶0+∞
8 eqid ⊢x∈A⟼C=x∈A⟼C
9 1 4 8 fmptdf ⊢φ→x∈A⟼C:A⟶0+∞
10 nfv ⊢Ⅎxy∈A
11 1 10 nfan ⊢Ⅎxφ∧y∈A
12 nfcv ⊢Ⅎ_xy
13 12 nfcsb1 ⊢Ⅎ_x⦋y/x⦌B
14 nfcv ⊢Ⅎ_x≤
15 12 nfcsb1 ⊢Ⅎ_x⦋y/x⦌C
16 13 14 15 nfbr ⊢Ⅎx⦋y/x⦌B≤⦋y/x⦌C
17 11 16 nfim ⊢Ⅎxφ∧y∈A→⦋y/x⦌B≤⦋y/x⦌C
18 eleq1w ⊢x=y→x∈A↔y∈A
19 18 anbi2d ⊢x=y→φ∧x∈A↔φ∧y∈A
20 csbeq1a ⊢x=y→B=⦋y/x⦌B
21 csbeq1a ⊢x=y→C=⦋y/x⦌C
22 20 21 breq12d ⊢x=y→B≤C↔⦋y/x⦌B≤⦋y/x⦌C
23 19 22 imbi12d ⊢x=y→φ∧x∈A→B≤C↔φ∧y∈A→⦋y/x⦌B≤⦋y/x⦌C
24 17 23 5 chvarfv ⊢φ∧y∈A→⦋y/x⦌B≤⦋y/x⦌C
25 simpr ⊢φ∧y∈A→y∈A
26 13 nfel1 ⊢Ⅎx⦋y/x⦌B∈0+∞
27 11 26 nfim ⊢Ⅎxφ∧y∈A→⦋y/x⦌B∈0+∞
28 20 eleq1d ⊢x=y→B∈0+∞↔⦋y/x⦌B∈0+∞
29 19 28 imbi12d ⊢x=y→φ∧x∈A→B∈0+∞↔φ∧y∈A→⦋y/x⦌B∈0+∞
30 27 29 3 chvarfv ⊢φ∧y∈A→⦋y/x⦌B∈0+∞
31 12 13 20 6 fvmptf ⊢y∈A∧⦋y/x⦌B∈0+∞→x∈A⟼B⁡y=⦋y/x⦌B
32 25 30 31 syl2anc ⊢φ∧y∈A→x∈A⟼B⁡y=⦋y/x⦌B
33 nfcv ⊢Ⅎ_x0+∞
34 15 33 nfel ⊢Ⅎx⦋y/x⦌C∈0+∞
35 11 34 nfim ⊢Ⅎxφ∧y∈A→⦋y/x⦌C∈0+∞
36 21 eleq1d ⊢x=y→C∈0+∞↔⦋y/x⦌C∈0+∞
37 19 36 imbi12d ⊢x=y→φ∧x∈A→C∈0+∞↔φ∧y∈A→⦋y/x⦌C∈0+∞
38 35 37 4 chvarfv ⊢φ∧y∈A→⦋y/x⦌C∈0+∞
39 12 15 21 8 fvmptf ⊢y∈A∧⦋y/x⦌C∈0+∞→x∈A⟼C⁡y=⦋y/x⦌C
40 25 38 39 syl2anc ⊢φ∧y∈A→x∈A⟼C⁡y=⦋y/x⦌C
41 32 40 breq12d ⊢φ∧y∈A→x∈A⟼B⁡y≤x∈A⟼C⁡y↔⦋y/x⦌B≤⦋y/x⦌C
42 24 41 mpbird ⊢φ∧y∈A→x∈A⟼B⁡y≤x∈A⟼C⁡y
43 2 7 9 42 sge0le ⊢φ→sum^⁡x∈A⟼B≤sum^⁡x∈A⟼C