Metamath Proof Explorer

Theorem carsggect

Description: The outer measure is countably superadditive on Caratheodory measurable sets. (Contributed by Thierry Arnoux, 31-May-2020)

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

Proof

Step Hyp Ref Expression
1 carsgval.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 carsgval.2 ⊢ ( 𝜑 → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
3 carsgsiga.1 ⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
4 carsgsiga.2 ⊢ ( ( 𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
5 carsggect.0 ⊢ ( 𝜑 → ¬ ∅ ∈ 𝐴 )
6 carsggect.1 ⊢ ( 𝜑 → 𝐴 ≼ ω )
7 carsggect.2 ⊢ ( 𝜑 → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
8 carsggect.3 ⊢ ( 𝜑 → Disj 𝑦 ∈ 𝐴 𝑦 )
9 carsggect.4 ⊢ ( ( 𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
10 0ex ⊢ ∅ ∈ V
11 10 a1i ⊢ ( 𝜑 → ∅ ∈ V )
12 padct ⊢ ( ( 𝐴 ≼ ω ∧ ∅ ∈ V ∧ ¬ ∅ ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
13 6 11 5 12 syl3anc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
14 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) )
15 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) )
16 15 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝑓 = ( 𝑘 ∈ ℕ ↦ ( 𝑓 ‘ 𝑘 ) ) )
17 16 rneqd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran 𝑓 = ran ( 𝑘 ∈ ℕ ↦ ( 𝑓 ‘ 𝑘 ) ) )
18 14 17 esumeq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) = Σ* 𝑧 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝑓 ‘ 𝑘 ) ) ( 𝑀 ‘ 𝑧 ) )
19 fvex ⊢ ( toCaraSiga ‘ 𝑀 ) ∈ V
20 19 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( toCaraSiga ‘ 𝑀 ) ∈ V )
21 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝐴 ⊆ ( toCaraSiga ‘ 𝑀 ) )
22 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝑂 ∈ 𝑉 )
23 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
24 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝑀 ‘ ∅ ) = 0 )
25 22 23 24 0elcarsg ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ∅ ∈ ( toCaraSiga ‘ 𝑀 ) )
26 25 snssd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → { ∅ } ⊆ ( toCaraSiga ‘ 𝑀 ) )
27 21 26 unssd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝐴 ∪ { ∅ } ) ⊆ ( toCaraSiga ‘ 𝑀 ) )
28 20 27 ssexd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝐴 ∪ { ∅ } ) ∈ V )
29 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
30 1 2 carsgcl ⊢ ( 𝜑 → ( toCaraSiga ‘ 𝑀 ) ⊆ 𝒫 𝑂 )
31 7 30 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ 𝒫 𝑂 )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝐴 ⊆ 𝒫 𝑂 )
33 0elpw ⊢ ∅ ∈ 𝒫 𝑂
34 33 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ∅ ∈ 𝒫 𝑂 )
35 34 snssd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → { ∅ } ⊆ 𝒫 𝑂 )
36 32 35 unssd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝐴 ∪ { ∅ } ) ⊆ 𝒫 𝑂 )
37 36 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) ) → 𝑧 ∈ 𝒫 𝑂 )
38 29 37 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) ) → ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
39 15 frnd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran 𝑓 ⊆ ( 𝐴 ∪ { ∅ } ) )
40 14 28 38 39 esummono ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) ( 𝑀 ‘ 𝑧 ) )
41 ctex ⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
42 6 41 syl ⊢ ( 𝜑 → 𝐴 ∈ V )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝐴 ∈ V )
44 20 26 ssexd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → { ∅ } ∈ V )
45 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
46 32 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝒫 𝑂 )
47 45 46 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
48 elsni ⊢ ( 𝑧 ∈ { ∅ } → 𝑧 = ∅ )
49 48 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ { ∅ } ) → 𝑧 = ∅ )
50 49 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ ∅ ) )
51 24 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ { ∅ } ) → ( 𝑀 ‘ ∅ ) = 0 )
52 50 51 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ { ∅ } ) → ( 𝑀 ‘ 𝑧 ) = 0 )
53 43 44 47 52 esumpad ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) ( 𝑀 ‘ 𝑧 ) = Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) )
54 40 53 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) )
55 39 27 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran 𝑓 ⊆ ( toCaraSiga ‘ 𝑀 ) )
56 ssexg ⊢ ( ( ran 𝑓 ⊆ ( toCaraSiga ‘ 𝑀 ) ∧ ( toCaraSiga ‘ 𝑀 ) ∈ V ) → ran 𝑓 ∈ V )
57 55 19 56 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran 𝑓 ∈ V )
58 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
59 39 36 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran 𝑓 ⊆ 𝒫 𝑂 )
60 59 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑧 ∈ 𝒫 𝑂 )
61 58 60 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
62 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝐴 ⊆ ran 𝑓 )
63 14 57 61 62 esummono ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) )
64 54 63 jca ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∧ Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ) )
65 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
66 61 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ∀ 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
67 nfcv ⊢ Ⅎ 𝑧 ran 𝑓
68 67 esumcl ⊢ ( ( ran 𝑓 ∈ V ∧ ∀ 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
69 57 66 68 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
70 65 69 sselid ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ∈ ℝ* )
71 47 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ∀ 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
72 nfcv ⊢ Ⅎ 𝑧 𝐴
73 72 esumcl ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) ) → Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
74 43 71 73 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∈ ( 0 [,] +∞ ) )
75 65 74 sselid ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∈ ℝ* )
76 xrletri3 ⊢ ( ( Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ∈ ℝ* ∧ Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∈ ℝ* ) → ( Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) = Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ↔ ( Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∧ Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ) ) )
77 70 75 76 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) = Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ↔ ( Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ∧ Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ≤ Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) ) ) )
78 64 77 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ( 𝑀 ‘ 𝑧 ) = Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) )
79 fveq2 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑘 ) → ( 𝑀 ‘ 𝑧 ) = ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) )
80 nnex ⊢ ℕ ∈ V
81 80 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ℕ ∈ V )
82 23 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
83 36 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ∪ { ∅ } ) ⊆ 𝒫 𝑂 )
84 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) → 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) )
85 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
86 84 85 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ ( 𝐴 ∪ { ∅ } ) )
87 83 86 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝒫 𝑂 )
88 82 87 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) ∈ ( 0 [,] +∞ ) )
89 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( 𝑓 ‘ 𝑘 ) = ∅ )
90 89 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝑀 ‘ ∅ ) )
91 24 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
92 90 91 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) = 0 )
93 cnvimass ⊢ ( ◡ 𝑓 “ 𝐴 ) ⊆ dom 𝑓
94 93 15 fssdm ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( ◡ 𝑓 “ 𝐴 ) ⊆ ℕ )
95 ffun ⊢ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) → Fun 𝑓 )
96 15 95 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Fun 𝑓 )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → Fun 𝑓 )
98 difpreima ⊢ ( Fun 𝑓 → ( ◡ 𝑓 “ ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) ) = ( ( ◡ 𝑓 “ ( 𝐴 ∪ { ∅ } ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) )
99 15 95 98 3syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( ◡ 𝑓 “ ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) ) = ( ( ◡ 𝑓 “ ( 𝐴 ∪ { ∅ } ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) )
100 fimacnv ⊢ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) → ( ◡ 𝑓 “ ( 𝐴 ∪ { ∅ } ) ) = ℕ )
101 15 100 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( ◡ 𝑓 “ ( 𝐴 ∪ { ∅ } ) ) = ℕ )
102 101 difeq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( ( ◡ 𝑓 “ ( 𝐴 ∪ { ∅ } ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) = ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) )
103 99 102 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( ◡ 𝑓 “ ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) ) = ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) )
104 uncom ⊢ ( { ∅ } ∪ 𝐴 ) = ( 𝐴 ∪ { ∅ } )
105 104 difeq1i ⊢ ( ( { ∅ } ∪ 𝐴 ) ∖ 𝐴 ) = ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 )
106 difun2 ⊢ ( ( { ∅ } ∪ 𝐴 ) ∖ 𝐴 ) = ( { ∅ } ∖ 𝐴 )
107 105 106 eqtr3i ⊢ ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) = ( { ∅ } ∖ 𝐴 )
108 difss ⊢ ( { ∅ } ∖ 𝐴 ) ⊆ { ∅ }
109 107 108 eqsstri ⊢ ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) ⊆ { ∅ }
110 109 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) ⊆ { ∅ } )
111 sspreima ⊢ ( ( Fun 𝑓 ∧ ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) ⊆ { ∅ } ) → ( ◡ 𝑓 “ ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) ) ⊆ ( ◡ 𝑓 “ { ∅ } ) )
112 96 110 111 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( ◡ 𝑓 “ ( ( 𝐴 ∪ { ∅ } ) ∖ 𝐴 ) ) ⊆ ( ◡ 𝑓 “ { ∅ } ) )
113 103 112 eqsstrrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) ⊆ ( ◡ 𝑓 “ { ∅ } ) )
114 113 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → 𝑘 ∈ ( ◡ 𝑓 “ { ∅ } ) )
115 fvimacnvi ⊢ ( ( Fun 𝑓 ∧ 𝑘 ∈ ( ◡ 𝑓 “ { ∅ } ) ) → ( 𝑓 ‘ 𝑘 ) ∈ { ∅ } )
116 97 114 115 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑘 ) ∈ { ∅ } )
117 elsni ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ { ∅ } → ( 𝑓 ‘ 𝑘 ) = ∅ )
118 116 117 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑘 ) = ∅ )
119 118 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ∀ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) ( 𝑓 ‘ 𝑘 ) = ∅ )
120 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Disj 𝑦 ∈ 𝐴 𝑦 )
121 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Fun ( ◡ 𝑓 ↾ 𝐴 ) )
122 fresf1o ⊢ ( ( Fun 𝑓 ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) → ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) : ( ◡ 𝑓 “ 𝐴 ) –1-1-onto→ 𝐴 )
123 96 62 121 122 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) : ( ◡ 𝑓 “ 𝐴 ) –1-1-onto→ 𝐴 )
124 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑦 = ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) ‘ 𝑘 ) ) → 𝑦 = ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) ‘ 𝑘 ) )
125 123 124 disjrdx ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( Disj 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) ‘ 𝑘 ) ↔ Disj 𝑦 ∈ 𝐴 𝑦 ) )
126 fvres ⊢ ( 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) → ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
127 126 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) ) → ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
128 127 disjeq2dv ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( Disj 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) ‘ 𝑘 ) ↔ Disj 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) ( 𝑓 ‘ 𝑘 ) ) )
129 125 128 bitr3d ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( Disj 𝑦 ∈ 𝐴 𝑦 ↔ Disj 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) ( 𝑓 ‘ 𝑘 ) ) )
130 120 129 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Disj 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) ( 𝑓 ‘ 𝑘 ) )
131 disjss3 ⊢ ( ( ( ◡ 𝑓 “ 𝐴 ) ⊆ ℕ ∧ ∀ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( Disj 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) ( 𝑓 ‘ 𝑘 ) ↔ Disj 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) ) )
132 131 biimpa ⊢ ( ( ( ( ◡ 𝑓 “ 𝐴 ) ⊆ ℕ ∧ ∀ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝑓 “ 𝐴 ) ) ( 𝑓 ‘ 𝑘 ) = ∅ ) ∧ Disj 𝑘 ∈ ( ◡ 𝑓 “ 𝐴 ) ( 𝑓 ‘ 𝑘 ) ) → Disj 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) )
133 94 119 130 132 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Disj 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) )
134 79 81 88 87 92 133 esumrnmpt2 ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ ran ( 𝑘 ∈ ℕ ↦ ( 𝑓 ‘ 𝑘 ) ) ( 𝑀 ‘ 𝑧 ) = Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) )
135 18 78 134 3eqtr3rd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) = Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) )
136 uniiun ⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
137 31 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝒫 𝑂 )
138 42 137 elpwiuncl ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝑂 )
139 136 138 eqeltrid ⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝒫 𝑂 )
140 139 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ∪ 𝐴 ∈ 𝒫 𝑂 )
141 23 140 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝑀 ‘ ∪ 𝐴 ) ∈ ( 0 [,] +∞ ) )
142 4 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
143 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑀 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑧 ) )
144 nfcv ⊢ Ⅎ 𝑧 𝑥
145 nfcv ⊢ Ⅎ 𝑦 𝑥
146 nfcv ⊢ Ⅎ 𝑧 ( 𝑀 ‘ 𝑦 )
147 nfcv ⊢ Ⅎ 𝑦 ( 𝑀 ‘ 𝑧 )
148 143 144 145 146 147 cbvesum ⊢ Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) = Σ* 𝑧 ∈ 𝑥 ( 𝑀 ‘ 𝑧 )
149 142 148 breqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂 ) → ( 𝑀 ‘ ∪ 𝑥 ) ≤ Σ* 𝑧 ∈ 𝑥 ( 𝑀 ‘ 𝑧 ) )
150 ffn ⊢ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) → 𝑓 Fn ℕ )
151 fz1ssnn ⊢ ( 1 ... 𝑛 ) ⊆ ℕ
152 fnssres ⊢ ( ( 𝑓 Fn ℕ ∧ ( 1 ... 𝑛 ) ⊆ ℕ ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) Fn ( 1 ... 𝑛 ) )
153 151 152 mpan2 ⊢ ( 𝑓 Fn ℕ → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) Fn ( 1 ... 𝑛 ) )
154 15 150 153 3syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) Fn ( 1 ... 𝑛 ) )
155 fzfi ⊢ ( 1 ... 𝑛 ) ∈ Fin
156 fnfi ⊢ ( ( ( 𝑓 ↾ ( 1 ... 𝑛 ) ) Fn ( 1 ... 𝑛 ) ∧ ( 1 ... 𝑛 ) ∈ Fin ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ∈ Fin )
157 155 156 mpan2 ⊢ ( ( 𝑓 ↾ ( 1 ... 𝑛 ) ) Fn ( 1 ... 𝑛 ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ∈ Fin )
158 rnfi ⊢ ( ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ∈ Fin → ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ∈ Fin )
159 154 157 158 3syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ∈ Fin )
160 resss ⊢ ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ 𝑓
161 rnss ⊢ ( ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ 𝑓 → ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ran 𝑓 )
162 160 161 ax-mp ⊢ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ran 𝑓
163 162 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ran 𝑓 )
164 163 55 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ( toCaraSiga ‘ 𝑀 ) )
165 163 39 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ( 𝐴 ∪ { ∅ } ) )
166 nfcv ⊢ Ⅎ 𝑧 𝑦
167 nfcv ⊢ Ⅎ 𝑦 𝑧
168 id ⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
169 166 167 168 cbvdisj ⊢ ( Disj 𝑦 ∈ 𝐴 𝑦 ↔ Disj 𝑧 ∈ 𝐴 𝑧 )
170 disjun0 ⊢ ( Disj 𝑧 ∈ 𝐴 𝑧 → Disj 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) 𝑧 )
171 169 170 sylbi ⊢ ( Disj 𝑦 ∈ 𝐴 𝑦 → Disj 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) 𝑧 )
172 8 171 syl ⊢ ( 𝜑 → Disj 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) 𝑧 )
173 172 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Disj 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) 𝑧 )
174 disjss1 ⊢ ( ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ( 𝐴 ∪ { ∅ } ) → ( Disj 𝑧 ∈ ( 𝐴 ∪ { ∅ } ) 𝑧 → Disj 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) 𝑧 ) )
175 165 173 174 sylc ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Disj 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) 𝑧 )
176 pwidg ⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂 )
177 22 176 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → 𝑂 ∈ 𝒫 𝑂 )
178 22 23 24 149 159 164 175 177 carsgclctunlem1 ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝑀 ‘ ( 𝑂 ∩ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ) = Σ* 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ( 𝑀 ‘ ( 𝑂 ∩ 𝑧 ) ) )
179 178 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝑂 ∩ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ) = Σ* 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ( 𝑀 ‘ ( 𝑂 ∩ 𝑧 ) ) )
180 165 unissd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ∪ ( 𝐴 ∪ { ∅ } ) )
181 uniun ⊢ ∪ ( 𝐴 ∪ { ∅ } ) = ( ∪ 𝐴 ∪ ∪ { ∅ } )
182 10 unisn ⊢ ∪ { ∅ } = ∅
183 182 uneq2i ⊢ ( ∪ 𝐴 ∪ ∪ { ∅ } ) = ( ∪ 𝐴 ∪ ∅ )
184 un0 ⊢ ( ∪ 𝐴 ∪ ∅ ) = ∪ 𝐴
185 181 183 184 3eqtri ⊢ ∪ ( 𝐴 ∪ { ∅ } ) = ∪ 𝐴
186 180 185 sseqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ∪ 𝐴 )
187 186 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ∪ 𝐴 )
188 uniss ⊢ ( 𝐴 ⊆ 𝒫 𝑂 → ∪ 𝐴 ⊆ ∪ 𝒫 𝑂 )
189 unipw ⊢ ∪ 𝒫 𝑂 = 𝑂
190 188 189 sseqtrdi ⊢ ( 𝐴 ⊆ 𝒫 𝑂 → ∪ 𝐴 ⊆ 𝑂 )
191 31 190 syl ⊢ ( 𝜑 → ∪ 𝐴 ⊆ 𝑂 )
192 191 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∪ 𝐴 ⊆ 𝑂 )
193 187 192 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ 𝑂 )
194 sseqin2 ⊢ ( ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ 𝑂 ↔ ( 𝑂 ∩ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) = ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
195 193 194 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑂 ∩ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) = ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
196 195 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ( 𝑂 ∩ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ) = ( 𝑀 ‘ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) )
197 nfv ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ )
198 165 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ ( 𝐴 ∪ { ∅ } ) )
199 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ 𝒫 𝑂 )
200 33 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∅ ∈ 𝒫 𝑂 )
201 200 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → { ∅ } ⊆ 𝒫 𝑂 )
202 199 201 unssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ∪ { ∅ } ) ⊆ 𝒫 𝑂 )
203 198 202 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ⊆ 𝒫 𝑂 )
204 203 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) → 𝑧 ∈ 𝒫 𝑂 )
205 204 elpwid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) → 𝑧 ⊆ 𝑂 )
206 sseqin2 ⊢ ( 𝑧 ⊆ 𝑂 ↔ ( 𝑂 ∩ 𝑧 ) = 𝑧 )
207 205 206 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) → ( 𝑂 ∩ 𝑧 ) = 𝑧 )
208 207 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) → ( 𝑀 ‘ ( 𝑂 ∩ 𝑧 ) ) = ( 𝑀 ‘ 𝑧 ) )
209 208 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ( 𝑀 ‘ ( 𝑂 ∩ 𝑧 ) ) = ( 𝑀 ‘ 𝑧 ) )
210 197 209 esumeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ( 𝑀 ‘ ( 𝑂 ∩ 𝑧 ) ) = Σ* 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ( 𝑀 ‘ 𝑧 ) )
211 16 reseq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) = ( ( 𝑘 ∈ ℕ ↦ ( 𝑓 ‘ 𝑘 ) ) ↾ ( 1 ... 𝑛 ) ) )
212 211 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) = ( ( 𝑘 ∈ ℕ ↦ ( 𝑓 ‘ 𝑘 ) ) ↾ ( 1 ... 𝑛 ) ) )
213 resmpt ⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( 𝑓 ‘ 𝑘 ) ) ↾ ( 1 ... 𝑛 ) ) = ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) )
214 151 213 ax-mp ⊢ ( ( 𝑘 ∈ ℕ ↦ ( 𝑓 ‘ 𝑘 ) ) ↾ ( 1 ... 𝑛 ) ) = ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) )
215 212 214 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑓 ↾ ( 1 ... 𝑛 ) ) = ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) )
216 215 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) = ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
217 216 rneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) = ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) )
218 197 217 esumeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑧 ∈ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ( 𝑀 ‘ 𝑧 ) = Σ* 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ( 𝑀 ‘ 𝑧 ) )
219 155 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ∈ Fin )
220 23 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑀 : 𝒫 𝑂 ⟶ ( 0 [,] +∞ ) )
221 151 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ )
222 221 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
223 87 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ℕ ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝒫 𝑂 )
224 222 223 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝒫 𝑂 )
225 220 224 ffvelrnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) ∈ ( 0 [,] +∞ ) )
226 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( 𝑓 ‘ 𝑘 ) = ∅ )
227 226 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝑀 ‘ ∅ ) )
228 24 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( 𝑀 ‘ ∅ ) = 0 )
229 227 228 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) ∧ ( 𝑓 ‘ 𝑘 ) = ∅ ) → ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) = 0 )
230 disjss1 ⊢ ( ( 1 ... 𝑛 ) ⊆ ℕ → ( Disj 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) → Disj 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑓 ‘ 𝑘 ) ) )
231 151 230 ax-mp ⊢ ( Disj 𝑘 ∈ ℕ ( 𝑓 ‘ 𝑘 ) → Disj 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑓 ‘ 𝑘 ) )
232 133 231 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Disj 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑓 ‘ 𝑘 ) )
233 232 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → Disj 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑓 ‘ 𝑘 ) )
234 79 219 225 224 229 233 esumrnmpt2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑧 ∈ ran ( 𝑘 ∈ ( 1 ... 𝑛 ) ↦ ( 𝑓 ‘ 𝑘 ) ) ( 𝑀 ‘ 𝑧 ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) )
235 210 218 234 3eqtr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑧 ∈ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ( 𝑀 ‘ ( 𝑂 ∩ 𝑧 ) ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) )
236 179 196 235 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) )
237 9 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂 ) → ( 𝑀 ‘ 𝑥 ) ≤ ( 𝑀 ‘ 𝑦 ) )
238 22 23 186 140 237 carsgmon ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → ( 𝑀 ‘ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ≤ ( 𝑀 ‘ ∪ 𝐴 ) )
239 238 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑀 ‘ ∪ ran ( 𝑓 ↾ ( 1 ... 𝑛 ) ) ) ≤ ( 𝑀 ‘ ∪ 𝐴 ) )
240 236 239 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 𝑀 ‘ ∪ 𝐴 ) )
241 141 88 240 esumgect ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑘 ∈ ℕ ( 𝑀 ‘ ( 𝑓 ‘ 𝑘 ) ) ≤ ( 𝑀 ‘ ∪ 𝐴 ) )
242 135 241 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : ℕ ⟶ ( 𝐴 ∪ { ∅ } ) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun ( ◡ 𝑓 ↾ 𝐴 ) ) ) → Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ≤ ( 𝑀 ‘ ∪ 𝐴 ) )
243 13 242 exlimddv ⊢ ( 𝜑 → Σ* 𝑧 ∈ 𝐴 ( 𝑀 ‘ 𝑧 ) ≤ ( 𝑀 ‘ ∪ 𝐴 ) )