Metamath Proof Explorer

Theorem carsgclctunlem3

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

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

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
5 carsgsiga.3 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
6 carsgclctun.1 ⊢ ( 𝜑 → 𝐴 ≼ ω )
7 carsgclctun.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
8 carsgclctunlem3.1 ⊢ ( 𝜑 → 𝐸 ∈ 𝒫 𝑂 )
9 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
10 8 elpwincl1 ⊢ ( 𝜑 → ( 𝐸 ∩ ∪ 𝐴 ) ∈ 𝒫 𝑂 )
11 2 10 ffvelrnd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
12 9 11 sselid ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) ∈ ℝ* )
13 8 elpwdifcl ⊢ ( 𝜑 → ( 𝐸 ∖ ∪ 𝐴 ) ∈ 𝒫 𝑂 )
14 2 13 ffvelrnd ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
15 9 14 sselid ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ∈ ℝ* )
16 12 15 xaddcld ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ∈ ℝ* )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) = +∞ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ∈ ℝ* )
18 pnfge ⊢ ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ∈ ℝ* → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ +∞ )
19 17 18 syl ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) = +∞ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ +∞ )
20 simpr ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) = +∞ ) → ( 𝑀 ‘ 𝐸 ) = +∞ )
21 19 20 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) = +∞ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )
22 unieq ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∪ ∅ )
23 uni0 ⊢ ∪ ∅ = ∅
24 22 23 eqtrdi ⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∅ )
25 24 ineq2d ⊢ ( 𝐴 = ∅ → ( 𝐸 ∩ ∪ 𝐴 ) = ( 𝐸 ∩ ∅ ) )
26 in0 ⊢ ( 𝐸 ∩ ∅ ) = ∅
27 25 26 eqtrdi ⊢ ( 𝐴 = ∅ → ( 𝐸 ∩ ∪ 𝐴 ) = ∅ )
28 27 fveq2d ⊢ ( 𝐴 = ∅ → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) = ( 𝑀 ‘ ∅ ) )
29 24 difeq2d ⊢ ( 𝐴 = ∅ → ( 𝐸 ∖ ∪ 𝐴 ) = ( 𝐸 ∖ ∅ ) )
30 dif0 ⊢ ( 𝐸 ∖ ∅ ) = 𝐸
31 29 30 eqtrdi ⊢ ( 𝐴 = ∅ → ( 𝐸 ∖ ∪ 𝐴 ) = 𝐸 )
32 31 fveq2d ⊢ ( 𝐴 = ∅ → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) = ( 𝑀 ‘ 𝐸 ) )
33 28 32 oveq12d ⊢ ( 𝐴 = ∅ → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) = ( ( 𝑀 ‘ ∅ ) +𝑒 ( 𝑀 ‘ 𝐸 ) ) )
34 33 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) = ( ( 𝑀 ‘ ∅ ) +𝑒 ( 𝑀 ‘ 𝐸 ) ) )
35 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
36 35 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( ( 𝑀 ‘ ∅ ) +𝑒 ( 𝑀 ‘ 𝐸 ) ) = ( 0 +𝑒 ( 𝑀 ‘ 𝐸 ) ) )
37 2 8 ffvelrnd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐸 ) ∈ ( 0 [,] +∞ ) )
38 9 37 sselid ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐸 ) ∈ ℝ* )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( 𝑀 ‘ 𝐸 ) ∈ ℝ* )
40 xaddid2 ⊢ ( ( 𝑀 ‘ 𝐸 ) ∈ ℝ* → ( 0 +𝑒 ( 𝑀 ‘ 𝐸 ) ) = ( 𝑀 ‘ 𝐸 ) )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( 0 +𝑒 ( 𝑀 ‘ 𝐸 ) ) = ( 𝑀 ‘ 𝐸 ) )
42 34 36 41 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) )
43 42 39 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ∈ ℝ* )
44 xeqlelt ⊢ ( ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ∈ ℝ* ∧ ( 𝑀 ‘ 𝐸 ) ∈ ℝ* ) → ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) ↔ ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) ∧ ¬ ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) < ( 𝑀 ‘ 𝐸 ) ) ) )
45 43 39 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) = ( 𝑀 ‘ 𝐸 ) ↔ ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) ∧ ¬ ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) < ( 𝑀 ‘ 𝐸 ) ) ) )
46 42 45 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) ∧ ¬ ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) < ( 𝑀 ‘ 𝐸 ) ) )
47 46 simpld ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )
48 47 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 = ∅ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )
49 fvex ⊢ ( toCaraSiga ‘ 𝑀 ) ∈ V
50 49 ssex ⊢ ( 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) → 𝐴 ∈ V )
51 0sdomg ⊢ ( 𝐴 ∈ V → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
52 7 50 51 3syl ⊢ ( 𝜑 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
53 52 biimpar ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∅ ≺ 𝐴 )
54 53 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) → ∅ ≺ 𝐴 )
55 nnenom ⊢ ℕ ≈ ω
56 55 ensymi ⊢ ω ≈ ℕ
57 domentr ⊢ ( ( 𝐴 ≼ ω ∧ ω ≈ ℕ ) → 𝐴 ≼ ℕ )
58 6 56 57 sylancl ⊢ ( 𝜑 → 𝐴 ≼ ℕ )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ≼ ℕ )
60 fodomr ⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 )
61 54 59 60 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝐴 )
62 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑘 ) )
63 62 iundisj ⊢ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) )
64 fofn ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → 𝑓 Fn ℕ )
65 fniunfv ⊢ ( 𝑓 Fn ℕ → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ ran 𝑓 )
66 64 65 syl ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ ran 𝑓 )
67 forn ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ran 𝑓 = 𝐴 )
68 67 unieqd ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ∪ ran 𝑓 = ∪ 𝐴 )
69 66 68 eqtrd ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝐴 )
70 69 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝐴 )
71 63 70 eqtr3id ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) = ∪ 𝐴 )
72 71 ineq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( 𝐸 ∩ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ) = ( 𝐸 ∩ ∪ 𝐴 ) )
73 72 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ) ) = ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) )
74 71 difeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( 𝐸 ∖ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ) = ( 𝐸 ∖ ∪ 𝐴 ) )
75 74 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ) ) = ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) )
76 73 75 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ) ) ) = ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) )
77 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → 𝑂 ∈ 𝑉 )
78 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
79 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( 𝑀 ‘ ∅ ) = 0 )
80 4 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
81 80 3adant1r ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
82 81 3adant1r ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
83 5 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
84 83 3adant1r ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
85 84 3adant1r ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
86 62 iundisj2 ⊢ Disj 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) )
87 86 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → Disj 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) )
88 77 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → 𝑂 ∈ 𝑉 )
89 78 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
90 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
91 fof ⊢ ( 𝑓 : ℕ –onto→ 𝐴 → 𝑓 : ℕ ⟶ 𝐴 )
92 91 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → 𝑓 : ℕ ⟶ 𝐴 )
93 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
94 92 93 ffvelrnd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 )
95 90 94 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ‘ 𝑛 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
96 79 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ∅ ) = 0 )
97 82 3adant1r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
98 88 89 96 97 carsgsigalem ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑔 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ ( 𝑒 ∪ 𝑔 ) ) ≤ ( ( 𝑀 ‘ 𝑒 ) +𝑒 ( 𝑀 ‘ 𝑔 ) ) )
99 91 ad3antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑓 : ℕ ⟶ 𝐴 )
100 fzossnn ⊢ ( 1 ..^ 𝑛 ) ⊆ ℕ
101 100 a1i ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( 1 ..^ 𝑛 ) ⊆ ℕ )
102 101 sselda ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝑘 ∈ ℕ )
103 99 102 ffvelrnd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝐴 )
104 103 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ∈ 𝐴 )
105 dfiun2g ⊢ ( ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ∈ 𝐴 → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) = ∪ { 𝑧 ∣ ∃ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝑧 = ( 𝑓 ‘ 𝑘 ) } )
106 104 105 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) = ∪ { 𝑧 ∣ ∃ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝑧 = ( 𝑓 ‘ 𝑘 ) } )
107 eqid ⊢ ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) )
108 107 rnmpt ⊢ ran ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) = { 𝑧 ∣ ∃ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝑧 = ( 𝑓 ‘ 𝑘 ) }
109 fzofi ⊢ ( 1 ..^ 𝑛 ) ∈ Fin
110 mptfi ⊢ ( ( 1 ..^ 𝑛 ) ∈ Fin → ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ Fin )
111 rnfi ⊢ ( ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ Fin → ran ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ Fin )
112 109 110 111 mp2b ⊢ ran ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ Fin
113 108 112 eqeltrri ⊢ { 𝑧 ∣ ∃ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝑧 = ( 𝑓 ‘ 𝑘 ) } ∈ Fin
114 113 a1i ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → { 𝑧 ∣ ∃ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝑧 = ( 𝑓 ‘ 𝑘 ) } ∈ Fin )
115 90 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
116 115 103 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ..^ 𝑛 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
117 116 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
118 107 rnmptss ⊢ ( ∀ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ∈ ( toCaraSiga ‘ 𝑀 ) → ran ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( toCaraSiga ‘ 𝑀 ) )
119 117 118 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ran ( 𝑘 ∈ ( 1 ..^ 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( toCaraSiga ‘ 𝑀 ) )
120 108 119 eqsstrrid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → { 𝑧 ∣ ∃ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝑧 = ( 𝑓 ‘ 𝑘 ) } ⊆ ( toCaraSiga ‘ 𝑀 ) )
121 88 89 96 97 114 120 fiunelcarsg ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ∪ { 𝑧 ∣ ∃ 𝑘 ∈ ( 1 ..^ 𝑛 ) 𝑧 = ( 𝑓 ‘ 𝑘 ) } ∈ ( toCaraSiga ‘ 𝑀 ) )
122 106 121 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ∈ ( toCaraSiga ‘ 𝑀 ) )
123 88 89 95 98 122 difelcarsg2 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ∈ ( toCaraSiga ‘ 𝑀 ) )
124 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → 𝐸 ∈ 𝒫 𝑂 )
125 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( 𝑀 ‘ 𝐸 ) ≠ +∞ )
126 77 78 79 82 85 87 123 124 125 carsgclctunlem2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑘 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )
127 76 126 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝐴 ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )
128 61 127 exlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) ∧ 𝐴 ≠ ∅ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )
129 48 128 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝐸 ) ≠ +∞ ) → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )
130 21 129 pm2.61dane ⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝐸 ∩ ∪ 𝐴 ) ) +𝑒 ( 𝑀 ‘ ( 𝐸 ∖ ∪ 𝐴 ) ) ) ≤ ( 𝑀 ‘ 𝐸 ) )