Metamath Proof Explorer

Theorem carsgclctunlem2

Description: Lemma for carsgclctun . (Contributed by Thierry Arnoux, 25-May-2020)

Ref Expression
Hypotheses carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
carsgsiga.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
carsgclctunlem2.1 ⊢ ( 𝜑 → Disj 𝑘 ∈ ℕ 𝐴 )
carsgclctunlem2.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
carsgclctunlem2.3 ⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑂 )
carsgclctunlem2.4 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐸 ) ≠ +∞ )
Assertion carsgclctunlem2 ( 𝜑 → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
5 carsgsiga.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
6 carsgclctunlem2.1 ⊢ ( 𝜑 → Disj 𝑘 ∈ ℕ 𝐴 )
7 carsgclctunlem2.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
8 carsgclctunlem2.3 ⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑂 )
9 carsgclctunlem2.4 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐸 ) ≠ +∞ )
10 iunin2 ⊢ ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) = ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 )
11 10 fveq2i ⊢ ( 𝑀 ‘ ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) )
12 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
13 nnex ⊢ ℕ ∈ V
14 13 a1i ⊢ ( 𝜑 → ℕ ∈ V )
15 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐸 ∈ 𝒫 𝑂 )
16 15 elpwincl1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐸 ∩ 𝐴 ) ∈ 𝒫 𝑂 )
17 14 16 elpwiuncl ⊢ ( 𝜑 → ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ∈ 𝒫 𝑂 )
18 2 17 ffvelrnd ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
19 12 18 sseldi ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ) ∈ ℝ* )
20 11 19 eqeltrrid ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* )
21 2 8 ffvelrnd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐸 ) ∈ ( 0 [,] +∞ ) )
22 12 21 sseldi ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐸 ) ∈ ℝ* )
23 8 elpwdifcl ⊢ ( 𝜑 → ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ∈ 𝒫 𝑂 )
24 2 23 ffvelrnd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
25 12 24 sseldi ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* )
26 25 xnegcld ⊢ ( 𝜑 → -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* )
27 22 26 xaddcld ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) ∈ ℝ* )
28 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
29 28 16 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
31 nfcv ⊢ Ⅎ 𝑘 ℕ
32 31 esumcl ⊢ ( ( ℕ ∈ V ∧ ∀ 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
33 14 30 32 syl2anc ⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
34 12 33 sseldi ⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ℝ* )
35 16 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ∈ 𝒫 𝑂 )
36 dfiun3g ⊢ ( ∀ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ∈ 𝒫 𝑂 → ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) = ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) )
37 35 36 syl ⊢ ( 𝜑 → ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) = ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) )
38 37 fveq2d ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ) = ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ) )
39 nnct ⊢ ℕ ≼ ω
40 mptct ⊢ ( ℕ ≼ ω → ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω )
41 rnct ⊢ ( ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω → ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω )
42 39 40 41 mp2b ⊢ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω
43 42 a1i ⊢ ( 𝜑 → ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω )
44 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) = ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) )
45 44 rnmptss ⊢ ( ∀ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ∈ 𝒫 𝑂 → ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ⊆ 𝒫 𝑂 )
46 35 45 syl ⊢ ( 𝜑 → ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ⊆ 𝒫 𝑂 )
47 mptexg ⊢ ( ℕ ∈ V → ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ∈ V )
48 rnexg ⊢ ( ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ∈ V → ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ∈ V )
49 13 47 48 mp2b ⊢ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ∈ V
50 breq1 ⊢ ( 𝑥 = ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) → ( 𝑥 ≼ ω ↔ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω ) )
51 sseq1 ⊢ ( 𝑥 = ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) → ( 𝑥 ⊆ 𝒫 𝑂 ↔ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ⊆ 𝒫 𝑂 ) )
52 50 51 3anbi23d ⊢ ( 𝑥 = ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) → ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) ↔ ( 𝜑 ∧ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω ∧ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ⊆ 𝒫 𝑂 ) ) )
53 unieq ⊢ ( 𝑥 = ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) → ∪ 𝑥 = ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) )
54 53 fveq2d ⊢ ( 𝑥 = ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ) )
55 esumeq1 ⊢ ( 𝑥 = ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) → Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ( 𝑀 ‘ 𝑦 ) )
56 54 55 breq12d ⊢ ( 𝑥 = ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) → ( ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ↔ ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ) ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ( 𝑀 ‘ 𝑦 ) ) )
57 52 56 imbi12d ⊢ ( 𝑥 = ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) → ( ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω ∧ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ) ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ( 𝑀 ‘ 𝑦 ) ) ) )
58 57 4 vtoclg ⊢ ( ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ∈ V → ( ( 𝜑 ∧ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω ∧ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ) ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ( 𝑀 ‘ 𝑦 ) ) )
59 49 58 ax-mp ⊢ ( ( 𝜑 ∧ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ≼ ω ∧ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ) ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ( 𝑀 ‘ 𝑦 ) )
60 43 46 59 mpd3an23 ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ) ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ( 𝑀 ‘ 𝑦 ) )
61 38 60 eqbrtrd ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ) ≤ Σ* 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ( 𝑀 ‘ 𝑦 ) )
62 fveq2 ⊢ ( 𝑦 = ( 𝐸 ∩ 𝐴 ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) )
63 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝐸 ∩ 𝐴 ) = ∅ ) → ( 𝐸 ∩ 𝐴 ) = ∅ )
64 63 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝐸 ∩ 𝐴 ) = ∅ ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) = ( 𝑀 ‘ ∅ ) )
65 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝐸 ∩ 𝐴 ) = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
66 64 65 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝐸 ∩ 𝐴 ) = ∅ ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) = 0 )
67 disjin ⊢ ( Disj 𝑘 ∈ ℕ 𝐴 → Disj 𝑘 ∈ ℕ ( 𝐴 ∩ 𝐸 ) )
68 6 67 syl ⊢ ( 𝜑 → Disj 𝑘 ∈ ℕ ( 𝐴 ∩ 𝐸 ) )
69 incom ⊢ ( 𝐴 ∩ 𝐸 ) = ( 𝐸 ∩ 𝐴 )
70 69 rgenw ⊢ ∀ 𝑘 ∈ ℕ ( 𝐴 ∩ 𝐸 ) = ( 𝐸 ∩ 𝐴 )
71 disjeq2 ⊢ ( ∀ 𝑘 ∈ ℕ ( 𝐴 ∩ 𝐸 ) = ( 𝐸 ∩ 𝐴 ) → ( Disj 𝑘 ∈ ℕ ( 𝐴 ∩ 𝐸 ) ↔ Disj 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ) )
72 70 71 ax-mp ⊢ ( Disj 𝑘 ∈ ℕ ( 𝐴 ∩ 𝐸 ) ↔ Disj 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) )
73 68 72 sylib ⊢ ( 𝜑 → Disj 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) )
74 62 14 29 16 66 73 esumrnmpt2 ⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝐸 ∩ 𝐴 ) ) ( 𝑀 ‘ 𝑦 ) = Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) )
75 61 74 breqtrd ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ) ≤ Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) )
76 difssd ⊢ ( 𝜑 → ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ⊆ 𝐸 )
77 1 2 76 8 5 carsgmon ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ≤ ( 𝑀 ‘ 𝐸 ) )
78 21 24 77 xrge0subcld ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) ∈ ( 0 [,] +∞ ) )
79 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
80 8 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐸 ∈ 𝒫 𝑂 )
81 80 elpwincl1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ 𝒫 𝑂 )
82 79 81 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
83 12 82 sseldi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* )
84 xrge0neqmnf ⊢ ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ( 0 [,] +∞ ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ )
85 82 84 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ )
86 80 elpwdifcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ∈ 𝒫 𝑂 )
87 79 86 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
88 12 87 sseldi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* )
89 xrge0neqmnf ⊢ ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ( 0 [,] +∞ ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ )
90 87 89 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ )
91 88 xnegcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* )
92 xnegneg ⊢ ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* → -𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
93 88 92 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → -𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
94 93 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → -𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
95 xnegeq ⊢ ( -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ → -𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -𝑒 -∞ )
96 95 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → -𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -𝑒 -∞ )
97 xnegmnf ⊢ -𝑒 -∞ = +∞
98 96 97 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → -𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = +∞ )
99 94 98 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = +∞ )
100 99 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 +∞ ) )
101 simpll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝜑 )
102 fz1ssnn ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
103 102 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ )
104 103 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
105 101 104 7 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
106 105 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
107 dfiun3g ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = ∪ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) )
108 106 107 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = ∪ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) )
109 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑂 ∈ 𝑉 )
110 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ∅ ) = 0 )
111 4 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
112 fzfi ⊢ ( 1 ... 𝑛 ) ∈ Fin
113 mptfi ⊢ ( ( 1 ... 𝑛 ) ∈ Fin → ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ∈ Fin )
114 rnfi ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ∈ Fin → ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ∈ Fin )
115 112 113 114 mp2b ⊢ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ∈ Fin
116 115 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ∈ Fin )
117 eqid ⊢ ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) = ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 )
118 117 rnmptss ⊢ ( ∀ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) → ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ⊆ ( toCaraSiga ‘ 𝑀 ) )
119 106 118 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ⊆ ( toCaraSiga ‘ 𝑀 ) )
120 109 79 110 111 116 119 fiunelcarsg ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
121 108 120 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) )
122 109 79 elcarsg ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ∈ ( toCaraSiga ‘ 𝑀 ) ↔ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) ) )
123 121 122 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ⊆ 𝑂 ∧ ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ) )
124 123 simprd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) )
125 ineq1 ⊢ ( 𝑒 = 𝐸 → ( 𝑒 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
126 125 fveq2d ⊢ ( 𝑒 = 𝐸 → ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
127 difeq1 ⊢ ( 𝑒 = 𝐸 → ( 𝑒 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
128 127 fveq2d ⊢ ( 𝑒 = 𝐸 → ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
129 126 128 oveq12d ⊢ ( 𝑒 = 𝐸 → ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) )
130 fveq2 ⊢ ( 𝑒 = 𝐸 → ( 𝑀 ‘ 𝑒 ) = ( 𝑀 ‘ 𝐸 ) )
131 129 130 eqeq12d ⊢ ( 𝑒 = 𝐸 → ( ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) ↔ ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) ) )
132 131 rspcv ⊢ ( 𝐸 ∈ 𝒫 𝑂 → ( ∀ 𝑒 ∈ 𝒫 𝑂 ( ( 𝑀 ‘ ( 𝑒 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝑒 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝑒 ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) ) )
133 80 124 132 sylc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) )
134 133 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) )
135 xaddpnf1 ⊢ ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 +∞ ) = +∞ )
136 83 85 135 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 +∞ ) = +∞ )
137 136 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 +∞ ) = +∞ )
138 100 134 137 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → ( 𝑀 ‘ 𝐸 ) = +∞ )
139 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → ( 𝑀 ‘ 𝐸 ) ≠ +∞ )
140 139 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ ) → ¬ ( 𝑀 ‘ 𝐸 ) = +∞ )
141 138 140 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ¬ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = -∞ )
142 141 neqned ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ )
143 xaddass ⊢ ( ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ ) ∧ ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ ) ∧ ( -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≠ -∞ ) ) → ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) ) )
144 83 85 88 90 91 142 143 syl222anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) ) )
145 xnegid ⊢ ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* → ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = 0 )
146 88 145 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = 0 )
147 146 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 0 ) )
148 xaddid1 ⊢ ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 0 ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
149 83 148 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 0 ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
150 144 147 149 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
151 133 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) = ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) )
152 108 ineq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = ( 𝐸 ∩ ∪ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ) )
153 152 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ) ) )
154 mptss ⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ⊆ ( 𝑘 ∈ ℕ ↦ 𝐴 ) )
155 rnss ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ⊆ ( 𝑘 ∈ ℕ ↦ 𝐴 ) → ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ⊆ ran ( 𝑘 ∈ ℕ ↦ 𝐴 ) )
156 102 154 155 mp2b ⊢ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ⊆ ran ( 𝑘 ∈ ℕ ↦ 𝐴 )
157 156 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ⊆ ran ( 𝑘 ∈ ℕ ↦ 𝐴 ) )
158 disjrnmpt ⊢ ( Disj 𝑘 ∈ ℕ 𝐴 → Disj 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ 𝐴 ) 𝑦 )
159 6 158 syl ⊢ ( 𝜑 → Disj 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ 𝐴 ) 𝑦 )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Disj 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ 𝐴 ) 𝑦 )
161 disjss1 ⊢ ( ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ⊆ ran ( 𝑘 ∈ ℕ ↦ 𝐴 ) → ( Disj 𝑦 ∈ ran ( 𝑘 ∈ ℕ ↦ 𝐴 ) 𝑦 → Disj 𝑦 ∈ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) 𝑦 ) )
162 157 160 161 sylc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Disj 𝑦 ∈ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) 𝑦 )
163 109 79 110 111 116 119 162 80 carsgclctunlem1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ) ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) )
164 ineq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐸 ∩ 𝑦 ) = ( 𝐸 ∩ 𝐴 ) )
165 164 fveq2d ⊢ ( 𝑦 = 𝐴 → ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) )
166 112 elexi ⊢ ( 1 ... 𝑛 ) ∈ V
167 166 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ V )
168 101 104 29 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
169 inss2 ⊢ ( 𝐸 ∩ 𝐴 ) ⊆ 𝐴
170 sseq2 ⊢ ( 𝐴 = ∅ → ( ( 𝐸 ∩ 𝐴 ) ⊆ 𝐴 ↔ ( 𝐸 ∩ 𝐴 ) ⊆ ∅ ) )
171 169 170 mpbii ⊢ ( 𝐴 = ∅ → ( 𝐸 ∩ 𝐴 ) ⊆ ∅ )
172 ss0 ⊢ ( ( 𝐸 ∩ 𝐴 ) ⊆ ∅ → ( 𝐸 ∩ 𝐴 ) = ∅ )
173 171 172 syl ⊢ ( 𝐴 = ∅ → ( 𝐸 ∩ 𝐴 ) = ∅ )
174 173 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝐴 = ∅ ) → ( 𝐸 ∩ 𝐴 ) = ∅ )
175 174 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝐴 = ∅ ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) = ( 𝑀 ‘ ∅ ) )
176 110 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝐴 = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
177 175 176 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ 𝐴 = ∅ ) → ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) = 0 )
178 6 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Disj 𝑘 ∈ ℕ 𝐴 )
179 disjss1 ⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ( Disj 𝑘 ∈ ℕ 𝐴 → Disj 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
180 103 178 179 sylc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Disj 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
181 165 167 168 105 177 180 esumrnmpt2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑦 ∈ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ 𝐴 ) ( 𝑀 ‘ ( 𝐸 ∩ 𝑦 ) ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) )
182 153 163 181 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) )
183 150 151 182 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) = ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) )
184 24 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
185 12 184 sseldi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* )
186 185 xnegcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* )
187 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ 𝐸 ) ∈ ℝ* )
188 iunss1 ⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ⊆ ∪ 𝑘 ∈ ℕ 𝐴 )
189 102 188 mp1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ⊆ ∪ 𝑘 ∈ ℕ 𝐴 )
190 189 sscond ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ⊆ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
191 5 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
192 109 79 190 86 191 carsgmon ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ≤ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) )
193 xleneg ⊢ ( ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* ) → ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ≤ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ↔ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≤ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
194 193 biimpa ⊢ ( ( ( ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* ) ∧ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ≤ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) → -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≤ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) )
195 185 88 192 194 syl21anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≤ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) )
196 xleadd2a ⊢ ( ( ( -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ∈ ℝ* ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝐸 ) ∈ ℝ* ) ∧ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ≤ -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) → ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) ≤ ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
197 91 186 187 195 196 syl31anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ) ) ≤ ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
198 183 197 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ≤ ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
199 78 29 198 esumgect ⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝐸 ∩ 𝐴 ) ) ≤ ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
200 19 34 27 75 199 xrletrd ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑘 ∈ ℕ ( 𝐸 ∩ 𝐴 ) ) ≤ ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
201 11 200 eqbrtrrid ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ≤ ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
202 xleadd1a ⊢ ( ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* ∧ ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ℝ* ) ∧ ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ≤ ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) ≤ ( ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
203 20 27 25 201 202 syl31anc ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) ≤ ( ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) )
204 xrge0npcan ⊢ ( ( ( 𝑀 ‘ 𝐸 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ≤ ( 𝑀 ‘ 𝐸 ) ) → ( ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) )
205 21 24 77 204 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝐸 ) +𝑒 -𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) )
206 203 205 breqtrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑘 ∈ ℕ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )