Metamath Proof Explorer

Theorem carsgsigalem

Description: Lemma for the following theorems. (Contributed by Thierry Arnoux, 23-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
Assertion carsgsigalem ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) ≤ ( ( 𝑀 ‘ 𝑒 ) +e ( 𝑀 ‘ 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
5 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → 𝑒 = 𝑓 )
6 5 uneq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑒 ∪ 𝑒 ) = ( 𝑒 ∪ 𝑓 ) )
7 unidm ⊢ ( 𝑒 ∪ 𝑒 ) = 𝑒
8 6 7 eqtr3di ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑒 ∪ 𝑓 ) = 𝑒 )
9 8 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) = ( 𝑀 ‘ 𝑒 ) )
10 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
11 simp1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → 𝜑 )
12 11 2 syl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
13 simp2 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → 𝑒 ∈ 𝒫 𝑂 )
14 12 13 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ( 0 [,] +∞ ) )
15 10 14 sselid ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑒 ) ∈ ℝ* )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑀 ‘ 𝑒 ) ∈ ℝ* )
17 5 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑀 ‘ 𝑒 ) = ( 𝑀 ‘ 𝑓 ) )
18 17 16 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑀 ‘ 𝑓 ) ∈ ℝ* )
19 simp3 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → 𝑓 ∈ 𝒫 𝑂 )
20 12 19 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑀 ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) )
22 elxrge0 ⊢ ( ( 𝑀 ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑀 ‘ 𝑓 ) ∈ ℝ* ∧ 0 ≤ ( 𝑀 ‘ 𝑓 ) ) )
23 22 simprbi ⊢ ( ( 𝑀 ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑀 ‘ 𝑓 ) )
24 21 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → 0 ≤ ( 𝑀 ‘ 𝑓 ) )
25 xraddge02 ⊢ ( ( ( 𝑀 ‘ 𝑒 ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝑓 ) ∈ ℝ* ) → ( 0 ≤ ( 𝑀 ‘ 𝑓 ) → ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ 𝑒 ) +e ( 𝑀 ‘ 𝑓 ) ) ) )
26 25 imp ⊢ ( ( ( ( 𝑀 ‘ 𝑒 ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝑓 ) ∈ ℝ* ) ∧ 0 ≤ ( 𝑀 ‘ 𝑓 ) ) → ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ 𝑒 ) +e ( 𝑀 ‘ 𝑓 ) ) )
27 16 18 24 26 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑀 ‘ 𝑒 ) ≤ ( ( 𝑀 ‘ 𝑒 ) +e ( 𝑀 ‘ 𝑓 ) ) )
28 9 27 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 = 𝑓 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) ≤ ( ( 𝑀 ‘ 𝑒 ) +e ( 𝑀 ‘ 𝑓 ) ) )
29 uniprg ⊢ ( ( 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ∪ { 𝑒 , 𝑓 } = ( 𝑒 ∪ 𝑓 ) )
30 29 fveq2d ⊢ ( ( 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { 𝑒 , 𝑓 } ) = ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) )
31 30 3adant1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { 𝑒 , 𝑓 } ) = ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) )
32 prct ⊢ ( ( 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → { 𝑒 , 𝑓 } ≼ ω )
33 32 3adant1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → { 𝑒 , 𝑓 } ≼ ω )
34 prssi ⊢ ( ( 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → { 𝑒 , 𝑓 } ⊆ 𝒫 𝑂 )
35 34 3adant1 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → { 𝑒 , 𝑓 } ⊆ 𝒫 𝑂 )
36 prex ⊢ { 𝑒 , 𝑓 } ∈ V
37 breq1 ⊢ ( 𝑥 = { 𝑒 , 𝑓 } → ( 𝑥 ≼ ω ↔ { 𝑒 , 𝑓 } ≼ ω ) )
38 sseq1 ⊢ ( 𝑥 = { 𝑒 , 𝑓 } → ( 𝑥 ⊆ 𝒫 𝑂 ↔ { 𝑒 , 𝑓 } ⊆ 𝒫 𝑂 ) )
39 37 38 3anbi23d ⊢ ( 𝑥 = { 𝑒 , 𝑓 } → ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) ↔ ( 𝜑 ∧ { 𝑒 , 𝑓 } ≼ ω ∧ { 𝑒 , 𝑓 } ⊆ 𝒫 𝑂 ) ) )
40 unieq ⊢ ( 𝑥 = { 𝑒 , 𝑓 } → ∪ 𝑥 = ∪ { 𝑒 , 𝑓 } )
41 40 fveq2d ⊢ ( 𝑥 = { 𝑒 , 𝑓 } → ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ { 𝑒 , 𝑓 } ) )
42 esumeq1 ⊢ ( 𝑥 = { 𝑒 , 𝑓 } → Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) = Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) )
43 41 42 breq12d ⊢ ( 𝑥 = { 𝑒 , 𝑓 } → ( ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ↔ ( 𝑀 ‘ ∪ { 𝑒 , 𝑓 } ) ≤ Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) ) )
44 39 43 imbi12d ⊢ ( 𝑥 = { 𝑒 , 𝑓 } → ( ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ { 𝑒 , 𝑓 } ≼ ω ∧ { 𝑒 , 𝑓 } ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { 𝑒 , 𝑓 } ) ≤ Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) ) ) )
45 44 4 vtoclg ⊢ ( { 𝑒 , 𝑓 } ∈ V → ( ( 𝜑 ∧ { 𝑒 , 𝑓 } ≼ ω ∧ { 𝑒 , 𝑓 } ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { 𝑒 , 𝑓 } ) ≤ Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) ) )
46 36 45 ax-mp ⊢ ( ( 𝜑 ∧ { 𝑒 , 𝑓 } ≼ ω ∧ { 𝑒 , 𝑓 } ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { 𝑒 , 𝑓 } ) ≤ Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) )
47 11 33 35 46 syl3anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ { 𝑒 , 𝑓 } ) ≤ Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) )
48 31 47 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) ≤ Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) )
49 48 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) ≤ Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) )
50 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑦 = 𝑒 ) → 𝑦 = 𝑒 )
51 50 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑦 = 𝑒 ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑒 ) )
52 51 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) ∧ 𝑦 = 𝑒 ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑒 ) )
53 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑦 = 𝑓 ) → 𝑦 = 𝑓 )
54 53 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑦 = 𝑓 ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑓 ) )
55 54 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) ∧ 𝑦 = 𝑓 ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑓 ) )
56 13 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) → 𝑒 ∈ 𝒫 𝑂 )
57 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) → 𝑓 ∈ 𝒫 𝑂 )
58 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) → ( 𝑀 ‘ 𝑒 ) ∈ ( 0 [,] +∞ ) )
59 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) → ( 𝑀 ‘ 𝑓 ) ∈ ( 0 [,] +∞ ) )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) → 𝑒 ≠ 𝑓 )
61 52 55 56 57 58 59 60 esumpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) → Σ* 𝑦 ∈ { 𝑒 , 𝑓 } ( 𝑀 ‘ 𝑦 ) = ( ( 𝑀 ‘ 𝑒 ) +e ( 𝑀 ‘ 𝑓 ) ) )
62 49 61 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) ∧ 𝑒 ≠ 𝑓 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) ≤ ( ( 𝑀 ‘ 𝑒 ) +e ( 𝑀 ‘ 𝑓 ) ) )
63 28 62 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑓 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑓 ) ) ≤ ( ( 𝑀 ‘ 𝑒 ) +e ( 𝑀 ‘ 𝑓 ) ) )