Step | Hyp | Ref
| Expression |
1 | | carsggect.1 |
. . 3
⊢ (𝜑 → 𝐴 ≼ ω) |
2 | | 0ex 4718 |
. . . 4
⊢ ∅
∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → ∅ ∈
V) |
4 | | carsggect.0 |
. . 3
⊢ (𝜑 → ¬ ∅ ∈ 𝐴) |
5 | | padct 28885 |
. . 3
⊢ ((𝐴 ≼ ω ∧ ∅
∈ V ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
6 | 1, 3, 4, 5 | syl3anc 1318 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
7 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑧(𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
8 | | simpr1 1060 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝑓:ℕ⟶(𝐴 ∪ {∅})) |
9 | 8 | feqmptd 6159 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝑓 = (𝑘 ∈ ℕ ↦ (𝑓‘𝑘))) |
10 | 9 | rneqd 5274 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran 𝑓 = ran (𝑘 ∈ ℕ ↦ (𝑓‘𝑘))) |
11 | 7, 10 | esumeq1d 29424 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) = Σ*𝑧 ∈ ran (𝑘 ∈ ℕ ↦ (𝑓‘𝑘))(𝑀‘𝑧)) |
12 | | fvex 6113 |
. . . . . . . . . 10
⊢
(toCaraSiga‘𝑀)
∈ V |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (toCaraSiga‘𝑀) ∈ V) |
14 | | carsggect.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
15 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
16 | | carsgval.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝑂 ∈ 𝑉) |
18 | | carsgval.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
19 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
20 | | carsgsiga.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀‘∅) = 0) |
21 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝑀‘∅) = 0) |
22 | 17, 19, 21 | 0elcarsg 29696 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ∅ ∈
(toCaraSiga‘𝑀)) |
23 | 22 | snssd 4281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → {∅} ⊆
(toCaraSiga‘𝑀)) |
24 | 15, 23 | unssd 3751 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝐴 ∪ {∅}) ⊆
(toCaraSiga‘𝑀)) |
25 | 13, 24 | ssexd 4733 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝐴 ∪ {∅}) ∈ V) |
26 | 19 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ (𝐴 ∪ {∅})) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
27 | 16, 18 | carsgcl 29693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (toCaraSiga‘𝑀) ⊆ 𝒫 𝑂) |
28 | 14, 27 | sstrd 3578 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑂) |
29 | 28 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝐴 ⊆ 𝒫 𝑂) |
30 | | 0elpw 4760 |
. . . . . . . . . . . . 13
⊢ ∅
∈ 𝒫 𝑂 |
31 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ∅ ∈ 𝒫 𝑂) |
32 | 31 | snssd 4281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → {∅} ⊆ 𝒫 𝑂) |
33 | 29, 32 | unssd 3751 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝐴 ∪ {∅}) ⊆ 𝒫 𝑂) |
34 | 33 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ (𝐴 ∪ {∅})) → 𝑧 ∈ 𝒫 𝑂) |
35 | 26, 34 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ (𝐴 ∪ {∅})) → (𝑀‘𝑧) ∈ (0[,]+∞)) |
36 | | frn 5966 |
. . . . . . . . 9
⊢ (𝑓:ℕ⟶(𝐴 ∪ {∅}) → ran
𝑓 ⊆ (𝐴 ∪
{∅})) |
37 | 8, 36 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran 𝑓 ⊆ (𝐴 ∪ {∅})) |
38 | 7, 25, 35, 37 | esummono 29443 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) ≤ Σ*𝑧 ∈ (𝐴 ∪ {∅})(𝑀‘𝑧)) |
39 | | ctex 7856 |
. . . . . . . . . 10
⊢ (𝐴 ≼ ω → 𝐴 ∈ V) |
40 | 1, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ V) |
41 | 40 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝐴 ∈ V) |
42 | 13, 23 | ssexd 4733 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → {∅} ∈
V) |
43 | 19 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ 𝐴) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
44 | 29 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝒫 𝑂) |
45 | 43, 44 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ 𝐴) → (𝑀‘𝑧) ∈ (0[,]+∞)) |
46 | | elsni 4142 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ {∅} → 𝑧 = ∅) |
47 | 46 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ {∅}) → 𝑧 = ∅) |
48 | 47 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ {∅}) → (𝑀‘𝑧) = (𝑀‘∅)) |
49 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ {∅}) → (𝑀‘∅) = 0) |
50 | 48, 49 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ {∅}) → (𝑀‘𝑧) = 0) |
51 | 41, 42, 45, 50 | esumpad 29444 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ (𝐴 ∪ {∅})(𝑀‘𝑧) = Σ*𝑧 ∈ 𝐴(𝑀‘𝑧)) |
52 | 38, 51 | breqtrd 4609 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) ≤ Σ*𝑧 ∈ 𝐴(𝑀‘𝑧)) |
53 | 37, 24 | sstrd 3578 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran 𝑓 ⊆ (toCaraSiga‘𝑀)) |
54 | | ssexg 4732 |
. . . . . . . 8
⊢ ((ran
𝑓 ⊆
(toCaraSiga‘𝑀) ∧
(toCaraSiga‘𝑀) ∈
V) → ran 𝑓 ∈
V) |
55 | 53, 12, 54 | sylancl 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran 𝑓 ∈ V) |
56 | 19 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
57 | 37, 33 | sstrd 3578 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran 𝑓 ⊆ 𝒫 𝑂) |
58 | 57 | sselda 3568 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ 𝒫 𝑂) |
59 | 56, 58 | ffvelrnd 6268 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑧 ∈ ran 𝑓) → (𝑀‘𝑧) ∈ (0[,]+∞)) |
60 | | simpr2 1061 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝐴 ⊆ ran 𝑓) |
61 | 7, 55, 59, 60 | esummono 29443 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ≤ Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧)) |
62 | 52, 61 | jca 553 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) ≤ Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ∧ Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ≤ Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧))) |
63 | | iccssxr 12127 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
64 | 59 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ∀𝑧 ∈ ran 𝑓(𝑀‘𝑧) ∈ (0[,]+∞)) |
65 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑧ran
𝑓 |
66 | 65 | esumcl 29419 |
. . . . . . . 8
⊢ ((ran
𝑓 ∈ V ∧
∀𝑧 ∈ ran 𝑓(𝑀‘𝑧) ∈ (0[,]+∞)) →
Σ*𝑧 ∈
ran 𝑓(𝑀‘𝑧) ∈ (0[,]+∞)) |
67 | 55, 64, 66 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) ∈ (0[,]+∞)) |
68 | 63, 67 | sseldi 3566 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) ∈
ℝ*) |
69 | 45 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ∀𝑧 ∈ 𝐴 (𝑀‘𝑧) ∈ (0[,]+∞)) |
70 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑧𝐴 |
71 | 70 | esumcl 29419 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ ∀𝑧 ∈ 𝐴 (𝑀‘𝑧) ∈ (0[,]+∞)) →
Σ*𝑧 ∈
𝐴(𝑀‘𝑧) ∈ (0[,]+∞)) |
72 | 41, 69, 71 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ∈ (0[,]+∞)) |
73 | 63, 72 | sseldi 3566 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ∈
ℝ*) |
74 | | xrletri3 11861 |
. . . . . 6
⊢
((Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) ∈ ℝ* ∧
Σ*𝑧 ∈
𝐴(𝑀‘𝑧) ∈ ℝ*) →
(Σ*𝑧
∈ ran 𝑓(𝑀‘𝑧) = Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ↔ (Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) ≤ Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ∧ Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ≤ Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧)))) |
75 | 68, 73, 74 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) = Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ↔ (Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) ≤ Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ∧ Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ≤ Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧)))) |
76 | 62, 75 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ ran 𝑓(𝑀‘𝑧) = Σ*𝑧 ∈ 𝐴(𝑀‘𝑧)) |
77 | | fveq2 6103 |
. . . . 5
⊢ (𝑧 = (𝑓‘𝑘) → (𝑀‘𝑧) = (𝑀‘(𝑓‘𝑘))) |
78 | | nnex 10903 |
. . . . . 6
⊢ ℕ
∈ V |
79 | 78 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ℕ ∈
V) |
80 | 19 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
81 | 33 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) → (𝐴 ∪ {∅}) ⊆ 𝒫 𝑂) |
82 | 8 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) → 𝑓:ℕ⟶(𝐴 ∪ {∅})) |
83 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
84 | 82, 83 | ffvelrnd 6268 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ (𝐴 ∪ {∅})) |
85 | 81, 84 | sseldd 3569 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝒫 𝑂) |
86 | 80, 85 | ffvelrnd 6268 |
. . . . 5
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) → (𝑀‘(𝑓‘𝑘)) ∈ (0[,]+∞)) |
87 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) ∧ (𝑓‘𝑘) = ∅) → (𝑓‘𝑘) = ∅) |
88 | 87 | fveq2d 6107 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) ∧ (𝑓‘𝑘) = ∅) → (𝑀‘(𝑓‘𝑘)) = (𝑀‘∅)) |
89 | 21 | ad2antrr 758 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) ∧ (𝑓‘𝑘) = ∅) → (𝑀‘∅) = 0) |
90 | 88, 89 | eqtrd 2644 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ ℕ) ∧ (𝑓‘𝑘) = ∅) → (𝑀‘(𝑓‘𝑘)) = 0) |
91 | | cnvimass 5404 |
. . . . . . . 8
⊢ (◡𝑓 “ 𝐴) ⊆ dom 𝑓 |
92 | 91 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (◡𝑓 “ 𝐴) ⊆ dom 𝑓) |
93 | | fdm 5964 |
. . . . . . . 8
⊢ (𝑓:ℕ⟶(𝐴 ∪ {∅}) → dom
𝑓 =
ℕ) |
94 | 8, 93 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → dom 𝑓 = ℕ) |
95 | 92, 94 | sseqtrd 3604 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (◡𝑓 “ 𝐴) ⊆ ℕ) |
96 | | ffun 5961 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ⟶(𝐴 ∪ {∅}) → Fun
𝑓) |
97 | 8, 96 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Fun 𝑓) |
98 | 97 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ (ℕ ∖ (◡𝑓 “ 𝐴))) → Fun 𝑓) |
99 | | difpreima 6251 |
. . . . . . . . . . . . 13
⊢ (Fun
𝑓 → (◡𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) = ((◡𝑓 “ (𝐴 ∪ {∅})) ∖ (◡𝑓 “ 𝐴))) |
100 | 8, 96, 99 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (◡𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) = ((◡𝑓 “ (𝐴 ∪ {∅})) ∖ (◡𝑓 “ 𝐴))) |
101 | | fimacnv 6255 |
. . . . . . . . . . . . . 14
⊢ (𝑓:ℕ⟶(𝐴 ∪ {∅}) → (◡𝑓 “ (𝐴 ∪ {∅})) =
ℕ) |
102 | 8, 101 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (◡𝑓 “ (𝐴 ∪ {∅})) =
ℕ) |
103 | 102 | difeq1d 3689 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ((◡𝑓 “ (𝐴 ∪ {∅})) ∖ (◡𝑓 “ 𝐴)) = (ℕ ∖ (◡𝑓 “ 𝐴))) |
104 | 100, 103 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (◡𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) = (ℕ ∖ (◡𝑓 “ 𝐴))) |
105 | | uncom 3719 |
. . . . . . . . . . . . . . . 16
⊢
({∅} ∪ 𝐴)
= (𝐴 ∪
{∅}) |
106 | 105 | difeq1i 3686 |
. . . . . . . . . . . . . . 15
⊢
(({∅} ∪ 𝐴)
∖ 𝐴) = ((𝐴 ∪ {∅}) ∖ 𝐴) |
107 | | difun2 4000 |
. . . . . . . . . . . . . . 15
⊢
(({∅} ∪ 𝐴)
∖ 𝐴) = ({∅}
∖ 𝐴) |
108 | 106, 107 | eqtr3i 2634 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∪ {∅}) ∖ 𝐴) = ({∅} ∖ 𝐴) |
109 | | difss 3699 |
. . . . . . . . . . . . . 14
⊢
({∅} ∖ 𝐴) ⊆ {∅} |
110 | 108, 109 | eqsstri 3598 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∪ {∅}) ∖ 𝐴) ⊆
{∅} |
111 | 110 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ((𝐴 ∪ {∅}) ∖ 𝐴) ⊆ {∅}) |
112 | | sspreima 28827 |
. . . . . . . . . . . 12
⊢ ((Fun
𝑓 ∧ ((𝐴 ∪ {∅}) ∖ 𝐴) ⊆ {∅}) → (◡𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) ⊆ (◡𝑓 “ {∅})) |
113 | 97, 111, 112 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (◡𝑓 “ ((𝐴 ∪ {∅}) ∖ 𝐴)) ⊆ (◡𝑓 “ {∅})) |
114 | 104, 113 | eqsstr3d 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (ℕ ∖ (◡𝑓 “ 𝐴)) ⊆ (◡𝑓 “ {∅})) |
115 | 114 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ (ℕ ∖ (◡𝑓 “ 𝐴))) → 𝑘 ∈ (◡𝑓 “ {∅})) |
116 | | fvimacnvi 6239 |
. . . . . . . . 9
⊢ ((Fun
𝑓 ∧ 𝑘 ∈ (◡𝑓 “ {∅})) → (𝑓‘𝑘) ∈ {∅}) |
117 | 98, 115, 116 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ (ℕ ∖ (◡𝑓 “ 𝐴))) → (𝑓‘𝑘) ∈ {∅}) |
118 | | elsni 4142 |
. . . . . . . 8
⊢ ((𝑓‘𝑘) ∈ {∅} → (𝑓‘𝑘) = ∅) |
119 | 117, 118 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ (ℕ ∖ (◡𝑓 “ 𝐴))) → (𝑓‘𝑘) = ∅) |
120 | 119 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ∀𝑘 ∈ (ℕ ∖ (◡𝑓 “ 𝐴))(𝑓‘𝑘) = ∅) |
121 | | carsggect.3 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 𝑦) |
122 | 121 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Disj 𝑦 ∈ 𝐴 𝑦) |
123 | | simpr3 1062 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Fun (◡𝑓 ↾ 𝐴)) |
124 | | fresf1o 28815 |
. . . . . . . . . 10
⊢ ((Fun
𝑓 ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)) → (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→𝐴) |
125 | 97, 60, 123, 124 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝑓 ↾ (◡𝑓 “ 𝐴)):(◡𝑓 “ 𝐴)–1-1-onto→𝐴) |
126 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑦 = ((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑘)) → 𝑦 = ((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑘)) |
127 | 125, 126 | disjrdx 28786 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (Disj 𝑘 ∈ (◡𝑓 “ 𝐴)((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑘) ↔ Disj 𝑦 ∈ 𝐴 𝑦)) |
128 | | fvres 6117 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (◡𝑓 “ 𝐴) → ((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑘) = (𝑓‘𝑘)) |
129 | 128 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑘 ∈ (◡𝑓 “ 𝐴)) → ((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑘) = (𝑓‘𝑘)) |
130 | 129 | disjeq2dv 4558 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (Disj 𝑘 ∈ (◡𝑓 “ 𝐴)((𝑓 ↾ (◡𝑓 “ 𝐴))‘𝑘) ↔ Disj 𝑘 ∈ (◡𝑓 “ 𝐴)(𝑓‘𝑘))) |
131 | 127, 130 | bitr3d 269 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (Disj 𝑦 ∈ 𝐴 𝑦 ↔ Disj 𝑘 ∈ (◡𝑓 “ 𝐴)(𝑓‘𝑘))) |
132 | 122, 131 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Disj 𝑘 ∈ (◡𝑓 “ 𝐴)(𝑓‘𝑘)) |
133 | | disjss3 4582 |
. . . . . . 7
⊢ (((◡𝑓 “ 𝐴) ⊆ ℕ ∧ ∀𝑘 ∈ (ℕ ∖ (◡𝑓 “ 𝐴))(𝑓‘𝑘) = ∅) → (Disj 𝑘 ∈ (◡𝑓 “ 𝐴)(𝑓‘𝑘) ↔ Disj 𝑘 ∈ ℕ (𝑓‘𝑘))) |
134 | 133 | biimpa 500 |
. . . . . 6
⊢ ((((◡𝑓 “ 𝐴) ⊆ ℕ ∧ ∀𝑘 ∈ (ℕ ∖ (◡𝑓 “ 𝐴))(𝑓‘𝑘) = ∅) ∧ Disj 𝑘 ∈ (◡𝑓 “ 𝐴)(𝑓‘𝑘)) → Disj 𝑘 ∈ ℕ (𝑓‘𝑘)) |
135 | 95, 120, 132, 134 | syl21anc 1317 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Disj 𝑘 ∈ ℕ (𝑓‘𝑘)) |
136 | 77, 79, 86, 85, 90, 135 | esumrnmpt2 29457 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ ran (𝑘 ∈ ℕ ↦ (𝑓‘𝑘))(𝑀‘𝑧) = Σ*𝑘 ∈ ℕ(𝑀‘(𝑓‘𝑘))) |
137 | 11, 76, 136 | 3eqtr3rd 2653 |
. . 3
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑘 ∈ ℕ(𝑀‘(𝑓‘𝑘)) = Σ*𝑧 ∈ 𝐴(𝑀‘𝑧)) |
138 | | uniiun 4509 |
. . . . . . 7
⊢ ∪ 𝐴 =
∪ 𝑥 ∈ 𝐴 𝑥 |
139 | 28 | sselda 3568 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑂) |
140 | 40, 139 | elpwiuncl 28743 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝑂) |
141 | 138, 140 | syl5eqel 2692 |
. . . . . 6
⊢ (𝜑 → ∪ 𝐴
∈ 𝒫 𝑂) |
142 | 141 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ∪
𝐴 ∈ 𝒫 𝑂) |
143 | 19, 142 | ffvelrnd 6268 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝑀‘∪ 𝐴) ∈
(0[,]+∞)) |
144 | | carsgsiga.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
145 | 144 | 3adant1r 1311 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
146 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑀‘𝑦) = (𝑀‘𝑧)) |
147 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑧𝑥 |
148 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝑥 |
149 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑀‘𝑦) |
150 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑀‘𝑧) |
151 | 146, 147,
148, 149, 150 | cbvesum 29431 |
. . . . . . . . 9
⊢
Σ*𝑦
∈ 𝑥(𝑀‘𝑦) = Σ*𝑧 ∈ 𝑥(𝑀‘𝑧) |
152 | 145, 151 | syl6breq 4624 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑧 ∈ 𝑥(𝑀‘𝑧)) |
153 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝑓:ℕ⟶(𝐴 ∪ {∅}) → 𝑓 Fn ℕ) |
154 | | fz1ssnn 12243 |
. . . . . . . . . . 11
⊢
(1...𝑛) ⊆
ℕ |
155 | | fnssres 5918 |
. . . . . . . . . . 11
⊢ ((𝑓 Fn ℕ ∧ (1...𝑛) ⊆ ℕ) → (𝑓 ↾ (1...𝑛)) Fn (1...𝑛)) |
156 | 154, 155 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝑓 Fn ℕ → (𝑓 ↾ (1...𝑛)) Fn (1...𝑛)) |
157 | 8, 153, 156 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝑓 ↾ (1...𝑛)) Fn (1...𝑛)) |
158 | | fzfi 12633 |
. . . . . . . . . 10
⊢
(1...𝑛) ∈
Fin |
159 | | fnfi 8123 |
. . . . . . . . . 10
⊢ (((𝑓 ↾ (1...𝑛)) Fn (1...𝑛) ∧ (1...𝑛) ∈ Fin) → (𝑓 ↾ (1...𝑛)) ∈ Fin) |
160 | 158, 159 | mpan2 703 |
. . . . . . . . 9
⊢ ((𝑓 ↾ (1...𝑛)) Fn (1...𝑛) → (𝑓 ↾ (1...𝑛)) ∈ Fin) |
161 | | rnfi 8132 |
. . . . . . . . 9
⊢ ((𝑓 ↾ (1...𝑛)) ∈ Fin → ran (𝑓 ↾ (1...𝑛)) ∈ Fin) |
162 | 157, 160,
161 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran (𝑓 ↾ (1...𝑛)) ∈ Fin) |
163 | | resss 5342 |
. . . . . . . . . . 11
⊢ (𝑓 ↾ (1...𝑛)) ⊆ 𝑓 |
164 | | rnss 5275 |
. . . . . . . . . . 11
⊢ ((𝑓 ↾ (1...𝑛)) ⊆ 𝑓 → ran (𝑓 ↾ (1...𝑛)) ⊆ ran 𝑓) |
165 | 163, 164 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran
(𝑓 ↾ (1...𝑛)) ⊆ ran 𝑓 |
166 | 165 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran (𝑓 ↾ (1...𝑛)) ⊆ ran 𝑓) |
167 | 166, 53 | sstrd 3578 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran (𝑓 ↾ (1...𝑛)) ⊆ (toCaraSiga‘𝑀)) |
168 | 166, 37 | sstrd 3578 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ran (𝑓 ↾ (1...𝑛)) ⊆ (𝐴 ∪ {∅})) |
169 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧𝑦 |
170 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝑧 |
171 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
172 | 169, 170,
171 | cbvdisj 4563 |
. . . . . . . . . . . 12
⊢
(Disj 𝑦
∈ 𝐴 𝑦 ↔ Disj 𝑧 ∈ 𝐴 𝑧) |
173 | | disjun0 28790 |
. . . . . . . . . . . 12
⊢
(Disj 𝑧
∈ 𝐴 𝑧 → Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧) |
174 | 172, 173 | sylbi 206 |
. . . . . . . . . . 11
⊢
(Disj 𝑦
∈ 𝐴 𝑦 → Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧) |
175 | 121, 174 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧) |
176 | 175 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧) |
177 | | disjss1 4559 |
. . . . . . . . 9
⊢ (ran
(𝑓 ↾ (1...𝑛)) ⊆ (𝐴 ∪ {∅}) → (Disj 𝑧 ∈ (𝐴 ∪ {∅})𝑧 → Disj 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))𝑧)) |
178 | 168, 176,
177 | sylc 63 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Disj 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))𝑧) |
179 | | pwidg 4121 |
. . . . . . . . 9
⊢ (𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂) |
180 | 17, 179 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → 𝑂 ∈ 𝒫 𝑂) |
181 | 17, 19, 21, 152, 162, 167, 178, 180 | carsgclctunlem1 29706 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝑀‘(𝑂 ∩ ∪ ran
(𝑓 ↾ (1...𝑛)))) = Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂 ∩ 𝑧))) |
182 | 181 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝑂 ∩ ∪ ran
(𝑓 ↾ (1...𝑛)))) = Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂 ∩ 𝑧))) |
183 | 168 | unissd 4398 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ∪ ran
(𝑓 ↾ (1...𝑛)) ⊆ ∪ (𝐴
∪ {∅})) |
184 | | uniun 4392 |
. . . . . . . . . . . 12
⊢ ∪ (𝐴
∪ {∅}) = (∪ 𝐴 ∪ ∪
{∅}) |
185 | 2 | unisn 4387 |
. . . . . . . . . . . . 13
⊢ ∪ {∅} = ∅ |
186 | 185 | uneq2i 3726 |
. . . . . . . . . . . 12
⊢ (∪ 𝐴
∪ ∪ {∅}) = (∪
𝐴 ∪
∅) |
187 | | un0 3919 |
. . . . . . . . . . . 12
⊢ (∪ 𝐴
∪ ∅) = ∪ 𝐴 |
188 | 184, 186,
187 | 3eqtri 2636 |
. . . . . . . . . . 11
⊢ ∪ (𝐴
∪ {∅}) = ∪ 𝐴 |
189 | 183, 188 | syl6sseq 3614 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → ∪ ran
(𝑓 ↾ (1...𝑛)) ⊆ ∪ 𝐴) |
190 | 189 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → ∪ ran (𝑓 ↾ (1...𝑛)) ⊆ ∪ 𝐴) |
191 | | uniss 4394 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝒫 𝑂 → ∪ 𝐴
⊆ ∪ 𝒫 𝑂) |
192 | | unipw 4845 |
. . . . . . . . . . . 12
⊢ ∪ 𝒫 𝑂 = 𝑂 |
193 | 191, 192 | syl6sseq 3614 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝒫 𝑂 → ∪ 𝐴
⊆ 𝑂) |
194 | 28, 193 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝐴
⊆ 𝑂) |
195 | 194 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → ∪ 𝐴
⊆ 𝑂) |
196 | 190, 195 | sstrd 3578 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → ∪ ran (𝑓 ↾ (1...𝑛)) ⊆ 𝑂) |
197 | | sseqin2 3779 |
. . . . . . . 8
⊢ (∪ ran (𝑓 ↾ (1...𝑛)) ⊆ 𝑂 ↔ (𝑂 ∩ ∪ ran
(𝑓 ↾ (1...𝑛))) = ∪ ran (𝑓 ↾ (1...𝑛))) |
198 | 196, 197 | sylib 207 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑂 ∩ ∪ ran
(𝑓 ↾ (1...𝑛))) = ∪ ran (𝑓 ↾ (1...𝑛))) |
199 | 198 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝑂 ∩ ∪ ran
(𝑓 ↾ (1...𝑛)))) = (𝑀‘∪ ran
(𝑓 ↾ (1...𝑛)))) |
200 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑧((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) |
201 | 168 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → ran (𝑓 ↾ (1...𝑛)) ⊆ (𝐴 ∪ {∅})) |
202 | 28 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ 𝒫 𝑂) |
203 | 30 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → ∅ ∈
𝒫 𝑂) |
204 | 203 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → {∅} ⊆
𝒫 𝑂) |
205 | 202, 204 | unssd 3751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝐴 ∪ {∅}) ⊆ 𝒫 𝑂) |
206 | 201, 205 | sstrd 3578 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → ran (𝑓 ↾ (1...𝑛)) ⊆ 𝒫 𝑂) |
207 | 206 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))) → 𝑧 ∈ 𝒫 𝑂) |
208 | 207 | elpwid 4118 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))) → 𝑧 ⊆ 𝑂) |
209 | | sseqin2 3779 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ 𝑂 ↔ (𝑂 ∩ 𝑧) = 𝑧) |
210 | 208, 209 | sylib 207 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))) → (𝑂 ∩ 𝑧) = 𝑧) |
211 | 210 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 ∈ ran (𝑓 ↾ (1...𝑛))) → (𝑀‘(𝑂 ∩ 𝑧)) = (𝑀‘𝑧)) |
212 | 211 | ralrimiva 2949 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → ∀𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂 ∩ 𝑧)) = (𝑀‘𝑧)) |
213 | 200, 212 | esumeq2d 29426 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) →
Σ*𝑧 ∈
ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂 ∩ 𝑧)) = Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘𝑧)) |
214 | 9 | reseq1d 5316 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝑓 ↾ (1...𝑛)) = ((𝑘 ∈ ℕ ↦ (𝑓‘𝑘)) ↾ (1...𝑛))) |
215 | 214 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑓 ↾ (1...𝑛)) = ((𝑘 ∈ ℕ ↦ (𝑓‘𝑘)) ↾ (1...𝑛))) |
216 | | resmpt 5369 |
. . . . . . . . . . . 12
⊢
((1...𝑛) ⊆
ℕ → ((𝑘 ∈
ℕ ↦ (𝑓‘𝑘)) ↾ (1...𝑛)) = (𝑘 ∈ (1...𝑛) ↦ (𝑓‘𝑘))) |
217 | 154, 216 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℕ ↦ (𝑓‘𝑘)) ↾ (1...𝑛)) = (𝑘 ∈ (1...𝑛) ↦ (𝑓‘𝑘)) |
218 | 215, 217 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑓 ↾ (1...𝑛)) = (𝑘 ∈ (1...𝑛) ↦ (𝑓‘𝑘))) |
219 | 218 | eqcomd 2616 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ (1...𝑛) ↦ (𝑓‘𝑘)) = (𝑓 ↾ (1...𝑛))) |
220 | 219 | rneqd 5274 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ (𝑓‘𝑘)) = ran (𝑓 ↾ (1...𝑛))) |
221 | 200, 220 | esumeq1d 29424 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) →
Σ*𝑧 ∈
ran (𝑘 ∈ (1...𝑛) ↦ (𝑓‘𝑘))(𝑀‘𝑧) = Σ*𝑧 ∈ ran (𝑓 ↾ (1...𝑛))(𝑀‘𝑧)) |
222 | 158 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ Fin) |
223 | 19 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
224 | 154 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆
ℕ) |
225 | 224 | sselda 3568 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
226 | 85 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ℕ) → (𝑓‘𝑘) ∈ 𝒫 𝑂) |
227 | 225, 226 | syldan 486 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑓‘𝑘) ∈ 𝒫 𝑂) |
228 | 223, 227 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑀‘(𝑓‘𝑘)) ∈ (0[,]+∞)) |
229 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ (𝑓‘𝑘) = ∅) → (𝑓‘𝑘) = ∅) |
230 | 229 | fveq2d 6107 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ (𝑓‘𝑘) = ∅) → (𝑀‘(𝑓‘𝑘)) = (𝑀‘∅)) |
231 | 21 | ad3antrrr 762 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ (𝑓‘𝑘) = ∅) → (𝑀‘∅) = 0) |
232 | 230, 231 | eqtrd 2644 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ (𝑓‘𝑘) = ∅) → (𝑀‘(𝑓‘𝑘)) = 0) |
233 | | disjss1 4559 |
. . . . . . . . . . 11
⊢
((1...𝑛) ⊆
ℕ → (Disj 𝑘 ∈ ℕ (𝑓‘𝑘) → Disj 𝑘 ∈ (1...𝑛)(𝑓‘𝑘))) |
234 | 154, 233 | ax-mp 5 |
. . . . . . . . . 10
⊢
(Disj 𝑘
∈ ℕ (𝑓‘𝑘) → Disj 𝑘 ∈ (1...𝑛)(𝑓‘𝑘)) |
235 | 135, 234 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Disj 𝑘 ∈ (1...𝑛)(𝑓‘𝑘)) |
236 | 235 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → Disj 𝑘 ∈ (1...𝑛)(𝑓‘𝑘)) |
237 | 77, 222, 228, 227, 232, 236 | esumrnmpt2 29457 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) →
Σ*𝑧 ∈
ran (𝑘 ∈ (1...𝑛) ↦ (𝑓‘𝑘))(𝑀‘𝑧) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝑓‘𝑘))) |
238 | 213, 221,
237 | 3eqtr2d 2650 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) →
Σ*𝑧 ∈
ran (𝑓 ↾ (1...𝑛))(𝑀‘(𝑂 ∩ 𝑧)) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝑓‘𝑘))) |
239 | 182, 199,
238 | 3eqtr3d 2652 |
. . . . 5
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑀‘∪ ran
(𝑓 ↾ (1...𝑛))) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝑓‘𝑘))) |
240 | | carsggect.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
241 | 240 | 3adant1r 1311 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
242 | 17, 19, 189, 142, 241 | carsgmon 29703 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → (𝑀‘∪ ran
(𝑓 ↾ (1...𝑛))) ≤ (𝑀‘∪ 𝐴)) |
243 | 242 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) → (𝑀‘∪ ran
(𝑓 ↾ (1...𝑛))) ≤ (𝑀‘∪ 𝐴)) |
244 | 239, 243 | eqbrtrrd 4607 |
. . . 4
⊢ (((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)(𝑀‘(𝑓‘𝑘)) ≤ (𝑀‘∪ 𝐴)) |
245 | 143, 86, 244 | esumgect 29479 |
. . 3
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑘 ∈ ℕ(𝑀‘(𝑓‘𝑘)) ≤ (𝑀‘∪ 𝐴)) |
246 | 137, 245 | eqbrtrrd 4607 |
. 2
⊢ ((𝜑 ∧ (𝑓:ℕ⟶(𝐴 ∪ {∅}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) → Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ≤ (𝑀‘∪ 𝐴)) |
247 | 6, 246 | exlimddv 1850 |
1
⊢ (𝜑 → Σ*𝑧 ∈ 𝐴(𝑀‘𝑧) ≤ (𝑀‘∪ 𝐴)) |