| Step | Hyp | Ref
| Expression |
| 1 | | carsgclctun.2 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
| 2 | 1 | unissd 4917 |
. . 3
⊢ (𝜑 → ∪ 𝐴
⊆ ∪ (toCaraSiga‘𝑀)) |
| 3 | | carsgval.1 |
. . . 4
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
| 4 | | carsgval.2 |
. . . 4
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 5 | | carsgsiga.1 |
. . . 4
⊢ (𝜑 → (𝑀‘∅) = 0) |
| 6 | 3, 4, 5 | carsguni 34310 |
. . 3
⊢ (𝜑 → ∪ (toCaraSiga‘𝑀) = 𝑂) |
| 7 | 2, 6 | sseqtrd 4020 |
. 2
⊢ (𝜑 → ∪ 𝐴
⊆ 𝑂) |
| 8 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑂 ∈ 𝑉) |
| 9 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 10 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘∅) = 0) |
| 11 | | carsgsiga.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
| 12 | 11 | 3adant1r 1178 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
| 13 | | carsgsiga.3 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
| 14 | 13 | 3adant1r 1178 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
| 15 | | carsgclctun.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≼ ω) |
| 16 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝐴 ≼ ω) |
| 17 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝐴 ⊆ (toCaraSiga‘𝑀)) |
| 18 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑒 ∈ 𝒫 𝑂) |
| 19 | 8, 9, 10, 12, 14, 16, 17, 18 | carsgclctunlem3 34322 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ≤ (𝑀‘𝑒)) |
| 20 | | inex1g 5319 |
. . . . . . . . 9
⊢ (𝑒 ∈ 𝒫 𝑂 → (𝑒 ∩ ∪ 𝐴) ∈ V) |
| 21 | 20 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∩ ∪ 𝐴) ∈ V) |
| 22 | | difexg 5329 |
. . . . . . . . 9
⊢ (𝑒 ∈ 𝒫 𝑂 → (𝑒 ∖ ∪ 𝐴) ∈ V) |
| 23 | 22 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∖ ∪ 𝐴) ∈ V) |
| 24 | | prct 32726 |
. . . . . . . 8
⊢ (((𝑒 ∩ ∪ 𝐴)
∈ V ∧ (𝑒 ∖
∪ 𝐴) ∈ V) → {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼
ω) |
| 25 | 21, 23, 24 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼
ω) |
| 26 | 18 | elpwincl1 32544 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∩ ∪ 𝐴) ∈ 𝒫 𝑂) |
| 27 | 18 | elpwdifcl 32545 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∖ ∪ 𝐴) ∈ 𝒫 𝑂) |
| 28 | | prssi 4821 |
. . . . . . . 8
⊢ (((𝑒 ∩ ∪ 𝐴)
∈ 𝒫 𝑂 ∧
(𝑒 ∖ ∪ 𝐴)
∈ 𝒫 𝑂) →
{(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
⊆ 𝒫 𝑂) |
| 29 | 26, 27, 28 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂) |
| 30 | | prex 5437 |
. . . . . . . . 9
⊢ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
∈ V |
| 31 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → (𝑥 ≼ ω ↔ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼
ω)) |
| 32 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → (𝑥 ⊆ 𝒫 𝑂 ↔ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂)) |
| 33 | 31, 32 | 3anbi23d 1441 |
. . . . . . . . . . 11
⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) ↔ (𝜑 ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
⊆ 𝒫 𝑂))) |
| 34 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → ∪ 𝑥 =
∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) |
| 35 | 34 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → (𝑀‘∪ 𝑥) = (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)})) |
| 36 | | esumeq1 34035 |
. . . . . . . . . . . 12
⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} →
Σ*𝑦 ∈
𝑥(𝑀‘𝑦) = Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦)) |
| 37 | 35, 36 | breq12d 5156 |
. . . . . . . . . . 11
⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → ((𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦) ↔ (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)})
≤ Σ*𝑦
∈ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
(𝑀‘𝑦))) |
| 38 | 33, 37 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → (((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) ↔ ((𝜑 ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
⊆ 𝒫 𝑂) →
(𝑀‘∪ {(𝑒
∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤
Σ*𝑦 ∈
{(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
(𝑀‘𝑦)))) |
| 39 | 38, 11 | vtoclg 3554 |
. . . . . . . . 9
⊢ ({(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
∈ V → ((𝜑 ∧
{(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
≼ ω ∧ {(𝑒
∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)})
≤ Σ*𝑦
∈ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
(𝑀‘𝑦))) |
| 40 | 30, 39 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝜑 ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
⊆ 𝒫 𝑂) →
(𝑀‘∪ {(𝑒
∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤
Σ*𝑦 ∈
{(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
(𝑀‘𝑦)) |
| 41 | 40 | 3adant1r 1178 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
⊆ 𝒫 𝑂) →
(𝑀‘∪ {(𝑒
∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤
Σ*𝑦 ∈
{(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
(𝑀‘𝑦)) |
| 42 | 25, 29, 41 | mpd3an23 1465 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)})
≤ Σ*𝑦
∈ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
(𝑀‘𝑦)) |
| 43 | | uniprg 4923 |
. . . . . . . . 9
⊢ (((𝑒 ∩ ∪ 𝐴)
∈ 𝒫 𝑂 ∧
(𝑒 ∖ ∪ 𝐴)
∈ 𝒫 𝑂) →
∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} = ((𝑒 ∩ ∪ 𝐴) ∪ (𝑒 ∖ ∪ 𝐴))) |
| 44 | 26, 27, 43 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ∪
{(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
= ((𝑒 ∩ ∪ 𝐴)
∪ (𝑒 ∖ ∪ 𝐴))) |
| 45 | | inundif 4479 |
. . . . . . . 8
⊢ ((𝑒 ∩ ∪ 𝐴)
∪ (𝑒 ∖ ∪ 𝐴))
= 𝑒 |
| 46 | 44, 45 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ∪
{(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)}
= 𝑒) |
| 47 | 46 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴),
(𝑒 ∖ ∪ 𝐴)})
= (𝑀‘𝑒)) |
| 48 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑦 = (𝑒 ∩ ∪ 𝐴)) → 𝑦 = (𝑒 ∩ ∪ 𝐴)) |
| 49 | 48 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑦 = (𝑒 ∩ ∪ 𝐴)) → (𝑀‘𝑦) = (𝑀‘(𝑒 ∩ ∪ 𝐴))) |
| 50 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑦 = (𝑒 ∖ ∪ 𝐴)) → 𝑦 = (𝑒 ∖ ∪ 𝐴)) |
| 51 | 50 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑦 = (𝑒 ∖ ∪ 𝐴)) → (𝑀‘𝑦) = (𝑀‘(𝑒 ∖ ∪ 𝐴))) |
| 52 | 9, 26 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∩ ∪ 𝐴)) ∈
(0[,]+∞)) |
| 53 | 9, 27 | ffvelcdmd 7105 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∖ ∪ 𝐴)) ∈
(0[,]+∞)) |
| 54 | | ineq2 4214 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∩ ∪ 𝐴) =
(𝑒 ∖ ∪ 𝐴)
→ ((𝑒 ∩ ∪ 𝐴)
∩ (𝑒 ∩ ∪ 𝐴))
= ((𝑒 ∩ ∪ 𝐴)
∩ (𝑒 ∖ ∪ 𝐴))) |
| 55 | | inidm 4227 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∩ ∪ 𝐴)
∩ (𝑒 ∩ ∪ 𝐴))
= (𝑒 ∩ ∪ 𝐴) |
| 56 | | inindif 4375 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∩ ∪ 𝐴)
∩ (𝑒 ∖ ∪ 𝐴))
= ∅ |
| 57 | 54, 55, 56 | 3eqtr3g 2800 |
. . . . . . . . . . . 12
⊢ ((𝑒 ∩ ∪ 𝐴) =
(𝑒 ∖ ∪ 𝐴)
→ (𝑒 ∩ ∪ 𝐴) =
∅) |
| 58 | 57 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → (𝑒 ∩ ∪ 𝐴) = ∅) |
| 59 | 58 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → (𝑀‘(𝑒 ∩ ∪ 𝐴)) = (𝑀‘∅)) |
| 60 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → (𝑀‘∅) = 0) |
| 61 | 59, 60 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → (𝑀‘(𝑒 ∩ ∪ 𝐴)) = 0) |
| 62 | 61 | orcd 874 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) = 0 ∨ (𝑀‘(𝑒 ∩ ∪ 𝐴)) = +∞)) |
| 63 | 62 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) = 0 ∨ (𝑀‘(𝑒 ∩ ∪ 𝐴)) =
+∞))) |
| 64 | 49, 51, 26, 27, 52, 53, 63 | esumpr2 34068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦) = ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴)))) |
| 65 | 42, 47, 64 | 3brtr3d 5174 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘𝑒) ≤ ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴)))) |
| 66 | 19, 65 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ≤ (𝑀‘𝑒) ∧ (𝑀‘𝑒) ≤ ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))))) |
| 67 | | iccssxr 13470 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
| 68 | 67, 52 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∩ ∪ 𝐴)) ∈
ℝ*) |
| 69 | 67, 53 | sselid 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∖ ∪ 𝐴)) ∈
ℝ*) |
| 70 | 68, 69 | xaddcld 13343 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ∈
ℝ*) |
| 71 | 4 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘𝑒) ∈ (0[,]+∞)) |
| 72 | 67, 71 | sselid 3981 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘𝑒) ∈
ℝ*) |
| 73 | | xrletri3 13196 |
. . . . 5
⊢ ((((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ∈ ℝ*
∧ (𝑀‘𝑒) ∈ ℝ*)
→ (((𝑀‘(𝑒 ∩ ∪ 𝐴))
+𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒) ↔ (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ≤ (𝑀‘𝑒) ∧ (𝑀‘𝑒) ≤ ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴)))))) |
| 74 | 70, 72, 73 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒) ↔ (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ≤ (𝑀‘𝑒) ∧ (𝑀‘𝑒) ≤ ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴)))))) |
| 75 | 66, 74 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒)) |
| 76 | 75 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒)) |
| 77 | 3, 4 | elcarsg 34307 |
. 2
⊢ (𝜑 → (∪ 𝐴
∈ (toCaraSiga‘𝑀)
↔ (∪ 𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒)))) |
| 78 | 7, 76, 77 | mpbir2and 713 |
1
⊢ (𝜑 → ∪ 𝐴
∈ (toCaraSiga‘𝑀)) |