Step | Hyp | Ref
| Expression |
1 | | iccssxr 13048 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
2 | | carsgval.2 |
. . . . . . . 8
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
3 | | carsgclctunlem3.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂) |
4 | 3 | elpwincl1 30625 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 ∩ ∪ 𝐴) ∈ 𝒫 𝑂) |
5 | 2, 4 | ffvelrnd 6927 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ 𝐴)) ∈
(0[,]+∞)) |
6 | 1, 5 | sselid 3915 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪ 𝐴)) ∈
ℝ*) |
7 | 3 | elpwdifcl 30626 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 ∖ ∪ 𝐴) ∈ 𝒫 𝑂) |
8 | 2, 7 | ffvelrnd 6927 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘(𝐸 ∖ ∪ 𝐴)) ∈
(0[,]+∞)) |
9 | 1, 8 | sselid 3915 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝐸 ∖ ∪ 𝐴)) ∈
ℝ*) |
10 | 6, 9 | xaddcld 12921 |
. . . . 5
⊢ (𝜑 → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ∈
ℝ*) |
11 | 10 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑀‘𝐸) = +∞) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ∈
ℝ*) |
12 | | pnfge 12752 |
. . . 4
⊢ (((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ∈ ℝ*
→ ((𝑀‘(𝐸 ∩ ∪ 𝐴))
+𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤
+∞) |
13 | 11, 12 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑀‘𝐸) = +∞) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤
+∞) |
14 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ (𝑀‘𝐸) = +∞) → (𝑀‘𝐸) = +∞) |
15 | 13, 14 | breqtrrd 5098 |
. 2
⊢ ((𝜑 ∧ (𝑀‘𝐸) = +∞) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸)) |
16 | | unieq 4847 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
17 | | uni0 4866 |
. . . . . . . . . . . . 13
⊢ ∪ ∅ = ∅ |
18 | 16, 17 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
19 | 18 | ineq2d 4144 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → (𝐸 ∩ ∪ 𝐴) =
(𝐸 ∩
∅)) |
20 | | in0 4323 |
. . . . . . . . . . 11
⊢ (𝐸 ∩ ∅) =
∅ |
21 | 19, 20 | eqtrdi 2796 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐸 ∩ ∪ 𝐴) =
∅) |
22 | 21 | fveq2d 6743 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → (𝑀‘(𝐸 ∩ ∪ 𝐴)) = (𝑀‘∅)) |
23 | 18 | difeq2d 4054 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → (𝐸 ∖ ∪ 𝐴) =
(𝐸 ∖
∅)) |
24 | | dif0 4304 |
. . . . . . . . . . 11
⊢ (𝐸 ∖ ∅) = 𝐸 |
25 | 23, 24 | eqtrdi 2796 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → (𝐸 ∖ ∪ 𝐴) =
𝐸) |
26 | 25 | fveq2d 6743 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → (𝑀‘(𝐸 ∖ ∪ 𝐴)) = (𝑀‘𝐸)) |
27 | 22, 26 | oveq12d 7253 |
. . . . . . . 8
⊢ (𝐴 = ∅ → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) = ((𝑀‘∅) +𝑒 (𝑀‘𝐸))) |
28 | 27 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = ∅) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) = ((𝑀‘∅) +𝑒 (𝑀‘𝐸))) |
29 | | carsgsiga.1 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀‘∅) = 0) |
30 | 29 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = ∅) → (𝑀‘∅) = 0) |
31 | 30 | oveq1d 7250 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = ∅) → ((𝑀‘∅) +𝑒 (𝑀‘𝐸)) = (0 +𝑒 (𝑀‘𝐸))) |
32 | 2, 3 | ffvelrnd 6927 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀‘𝐸) ∈ (0[,]+∞)) |
33 | 1, 32 | sselid 3915 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀‘𝐸) ∈
ℝ*) |
34 | 33 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 = ∅) → (𝑀‘𝐸) ∈
ℝ*) |
35 | | xaddid2 12862 |
. . . . . . . 8
⊢ ((𝑀‘𝐸) ∈ ℝ* → (0
+𝑒 (𝑀‘𝐸)) = (𝑀‘𝐸)) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = ∅) → (0 +𝑒
(𝑀‘𝐸)) = (𝑀‘𝐸)) |
37 | 28, 31, 36 | 3eqtrd 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = ∅) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) = (𝑀‘𝐸)) |
38 | 37, 34 | eqeltrd 2840 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 = ∅) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ∈
ℝ*) |
39 | | xeqlelt 30849 |
. . . . . . 7
⊢ ((((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ∈ ℝ*
∧ (𝑀‘𝐸) ∈ ℝ*)
→ (((𝑀‘(𝐸 ∩ ∪ 𝐴))
+𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) = (𝑀‘𝐸) ↔ (((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸) ∧ ¬ ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) < (𝑀‘𝐸)))) |
40 | 38, 34, 39 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 = ∅) → (((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) = (𝑀‘𝐸) ↔ (((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸) ∧ ¬ ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) < (𝑀‘𝐸)))) |
41 | 37, 40 | mpbid 235 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = ∅) → (((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸) ∧ ¬ ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) < (𝑀‘𝐸))) |
42 | 41 | simpld 498 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = ∅) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸)) |
43 | 42 | adantlr 715 |
. . 3
⊢ (((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 = ∅) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸)) |
44 | | carsgclctun.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
45 | | fvex 6752 |
. . . . . . . . 9
⊢
(toCaraSiga‘𝑀)
∈ V |
46 | 45 | ssex 5231 |
. . . . . . . 8
⊢ (𝐴 ⊆ (toCaraSiga‘𝑀) → 𝐴 ∈ V) |
47 | | 0sdomg 8801 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
48 | 44, 46, 47 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
49 | 48 | biimpar 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → ∅ ≺ 𝐴) |
50 | 49 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) → ∅ ≺ 𝐴) |
51 | | carsgclctun.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≼ ω) |
52 | | nnenom 13585 |
. . . . . . . 8
⊢ ℕ
≈ ω |
53 | 52 | ensymi 8704 |
. . . . . . 7
⊢ ω
≈ ℕ |
54 | | domentr 8713 |
. . . . . . 7
⊢ ((𝐴 ≼ ω ∧ ω
≈ ℕ) → 𝐴
≼ ℕ) |
55 | 51, 53, 54 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≼ ℕ) |
56 | 55 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) → 𝐴 ≼ ℕ) |
57 | | fodomr 8823 |
. . . . 5
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ℕ) →
∃𝑓 𝑓:ℕ–onto→𝐴) |
58 | 50, 56, 57 | syl2anc 587 |
. . . 4
⊢ (((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto→𝐴) |
59 | | fveq2 6739 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘)) |
60 | 59 | iundisj 24477 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘)) |
61 | | fofn 6657 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → 𝑓 Fn ℕ) |
62 | | fniunfv 7082 |
. . . . . . . . . . . 12
⊢ (𝑓 Fn ℕ → ∪ 𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ ran 𝑓) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ ran 𝑓) |
64 | | forn 6658 |
. . . . . . . . . . . 12
⊢ (𝑓:ℕ–onto→𝐴 → ran 𝑓 = 𝐴) |
65 | 64 | unieqd 4850 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → ∪ ran
𝑓 = ∪ 𝐴) |
66 | 63, 65 | eqtrd 2779 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–onto→𝐴 → ∪
𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝐴) |
67 | 66 | adantl 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → ∪
𝑛 ∈ ℕ (𝑓‘𝑛) = ∪ 𝐴) |
68 | 60, 67 | eqtr3id 2794 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘)) = ∪ 𝐴) |
69 | 68 | ineq2d 4144 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → (𝐸 ∩ ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘))) = (𝐸 ∩ ∪ 𝐴)) |
70 | 69 | fveq2d 6743 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → (𝑀‘(𝐸 ∩ ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘)))) = (𝑀‘(𝐸 ∩ ∪ 𝐴))) |
71 | 68 | difeq2d 4054 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → (𝐸 ∖ ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘))) = (𝐸 ∖ ∪ 𝐴)) |
72 | 71 | fveq2d 6743 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → (𝑀‘(𝐸 ∖ ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘)))) = (𝑀‘(𝐸 ∖ ∪ 𝐴))) |
73 | 70, 72 | oveq12d 7253 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → ((𝑀‘(𝐸 ∩ ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘)))) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘))))) = ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴)))) |
74 | | carsgval.1 |
. . . . . . 7
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
75 | 74 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → 𝑂 ∈ 𝑉) |
76 | 2 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
77 | 29 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → (𝑀‘∅) = 0) |
78 | | carsgsiga.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
79 | 78 | 3adant1r 1179 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
80 | 79 | 3adant1r 1179 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
81 | 80 | 3adant1r 1179 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
82 | | carsgsiga.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
83 | 82 | 3adant1r 1179 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
84 | 83 | 3adant1r 1179 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
85 | 84 | 3adant1r 1179 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
86 | 59 | iundisj2 24478 |
. . . . . . 7
⊢
Disj 𝑛 ∈
ℕ ((𝑓‘𝑛) ∖ ∪ 𝑘 ∈ (1..^𝑛)(𝑓‘𝑘)) |
87 | 86 | a1i 11 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → Disj 𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘))) |
88 | 75 | adantr 484 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝑂 ∈ 𝑉) |
89 | 76 | adantr 484 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
90 | 44 | ad4antr 732 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
91 | | fof 6655 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–onto→𝐴 → 𝑓:ℕ⟶𝐴) |
92 | 91 | ad2antlr 727 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝑓:ℕ⟶𝐴) |
93 | | simpr 488 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
94 | 92, 93 | ffvelrnd 6927 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ 𝐴) |
95 | 90, 94 | sseldd 3919 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → (𝑓‘𝑛) ∈ (toCaraSiga‘𝑀)) |
96 | 77 | adantr 484 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → (𝑀‘∅) = 0) |
97 | 81 | 3adant1r 1179 |
. . . . . . . 8
⊢
((((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
98 | 88, 89, 96, 97 | carsgsigalem 32026 |
. . . . . . 7
⊢
((((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑒 ∈ 𝒫 𝑂 ∧ 𝑔 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∪ 𝑔)) ≤ ((𝑀‘𝑒) +𝑒 (𝑀‘𝑔))) |
99 | 91 | ad3antlr 731 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → 𝑓:ℕ⟶𝐴) |
100 | | fzossnn 13321 |
. . . . . . . . . . . . 13
⊢
(1..^𝑛) ⊆
ℕ |
101 | 100 | a1i 11 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → (1..^𝑛) ⊆
ℕ) |
102 | 101 | sselda 3918 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → 𝑘 ∈ ℕ) |
103 | 99, 102 | ffvelrnd 6927 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → (𝑓‘𝑘) ∈ 𝐴) |
104 | 103 | ralrimiva 3108 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1..^𝑛)(𝑓‘𝑘) ∈ 𝐴) |
105 | | dfiun2g 4957 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(1..^𝑛)(𝑓‘𝑘) ∈ 𝐴 → ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘) = ∪ {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓‘𝑘)}) |
106 | 104, 105 | syl 17 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → ∪ 𝑘 ∈ (1..^𝑛)(𝑓‘𝑘) = ∪ {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓‘𝑘)}) |
107 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) = (𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) |
108 | 107 | rnmpt 5842 |
. . . . . . . . . . 11
⊢ ran
(𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) = {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓‘𝑘)} |
109 | | fzofi 13579 |
. . . . . . . . . . . 12
⊢
(1..^𝑛) ∈
Fin |
110 | | mptfi 9005 |
. . . . . . . . . . . 12
⊢
((1..^𝑛) ∈ Fin
→ (𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) ∈ Fin) |
111 | | rnfi 8989 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) ∈ Fin → ran (𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) ∈ Fin) |
112 | 109, 110,
111 | mp2b 10 |
. . . . . . . . . . 11
⊢ ran
(𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) ∈ Fin |
113 | 108, 112 | eqeltrri 2837 |
. . . . . . . . . 10
⊢ {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓‘𝑘)} ∈ Fin |
114 | 113 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓‘𝑘)} ∈ Fin) |
115 | 90 | adantr 484 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
116 | 115, 103 | sseldd 3919 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1..^𝑛)) → (𝑓‘𝑘) ∈ (toCaraSiga‘𝑀)) |
117 | 116 | ralrimiva 3108 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1..^𝑛)(𝑓‘𝑘) ∈ (toCaraSiga‘𝑀)) |
118 | 107 | rnmptss 6961 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(1..^𝑛)(𝑓‘𝑘) ∈ (toCaraSiga‘𝑀) → ran (𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) ⊆ (toCaraSiga‘𝑀)) |
119 | 117, 118 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → ran (𝑘 ∈ (1..^𝑛) ↦ (𝑓‘𝑘)) ⊆ (toCaraSiga‘𝑀)) |
120 | 108, 119 | eqsstrrid 3967 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → {𝑧 ∣ ∃𝑘 ∈ (1..^𝑛)𝑧 = (𝑓‘𝑘)} ⊆ (toCaraSiga‘𝑀)) |
121 | 88, 89, 96, 97, 114, 120 | fiunelcarsg 32027 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → ∪ {𝑧
∣ ∃𝑘 ∈
(1..^𝑛)𝑧 = (𝑓‘𝑘)} ∈ (toCaraSiga‘𝑀)) |
122 | 106, 121 | eqeltrd 2840 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → ∪ 𝑘 ∈ (1..^𝑛)(𝑓‘𝑘) ∈ (toCaraSiga‘𝑀)) |
123 | 88, 89, 95, 98, 122 | difelcarsg2 32024 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) ∧ 𝑛 ∈ ℕ) → ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘)) ∈ (toCaraSiga‘𝑀)) |
124 | 3 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → 𝐸 ∈ 𝒫 𝑂) |
125 | | simpllr 776 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → (𝑀‘𝐸) ≠ +∞) |
126 | 75, 76, 77, 81, 85, 87, 123, 124, 125 | carsgclctunlem2 32030 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → ((𝑀‘(𝐸 ∩ ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘)))) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑛 ∈ ℕ ((𝑓‘𝑛) ∖ ∪
𝑘 ∈ (1..^𝑛)(𝑓‘𝑘))))) ≤ (𝑀‘𝐸)) |
127 | 73, 126 | eqbrtrrd 5094 |
. . . 4
⊢ ((((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) ∧ 𝑓:ℕ–onto→𝐴) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸)) |
128 | 58, 127 | exlimddv 1943 |
. . 3
⊢ (((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) ∧ 𝐴 ≠ ∅) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸)) |
129 | 43, 128 | pm2.61dane 3032 |
. 2
⊢ ((𝜑 ∧ (𝑀‘𝐸) ≠ +∞) → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸)) |
130 | 15, 129 | pm2.61dane 3032 |
1
⊢ (𝜑 → ((𝑀‘(𝐸 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪ 𝐴))) ≤ (𝑀‘𝐸)) |