| Step | Hyp | Ref
| Expression |
| 1 | | df-carsg 34304 |
. 2
⊢
toCaraSiga = (𝑚
∈ V ↦ {𝑎 ∈
𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)}) |
| 2 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀) |
| 3 | 2 | dmeqd 5916 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑚 = dom 𝑀) |
| 4 | | carsgval.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 5 | 4 | fdmd 6746 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑀 = 𝒫 𝑂) |
| 6 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑀 = 𝒫 𝑂) |
| 7 | 3, 6 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑚 = 𝒫 𝑂) |
| 8 | 7 | unieqd 4920 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → ∪ dom
𝑚 = ∪ 𝒫 𝑂) |
| 9 | | unipw 5455 |
. . . . 5
⊢ ∪ 𝒫 𝑂 = 𝑂 |
| 10 | 8, 9 | eqtrdi 2793 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → ∪ dom
𝑚 = 𝑂) |
| 11 | 10 | pweqd 4617 |
. . 3
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → 𝒫 ∪ dom 𝑚 = 𝒫 𝑂) |
| 12 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚‘(𝑒 ∩ 𝑎)) = (𝑀‘(𝑒 ∩ 𝑎))) |
| 13 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚‘(𝑒 ∖ 𝑎)) = (𝑀‘(𝑒 ∖ 𝑎))) |
| 14 | 12, 13 | oveq12d 7449 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎)))) |
| 15 | | fveq1 6905 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (𝑚‘𝑒) = (𝑀‘𝑒)) |
| 16 | 14, 15 | eqeq12d 2753 |
. . . . 5
⊢ (𝑚 = 𝑀 → (((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
| 17 | 16 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → (((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
| 18 | 11, 17 | raleqbidv 3346 |
. . 3
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → (∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
| 19 | 11, 18 | rabeqbidv 3455 |
. 2
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)} = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)}) |
| 20 | | carsgval.1 |
. . . 4
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
| 21 | 20 | pwexd 5379 |
. . 3
⊢ (𝜑 → 𝒫 𝑂 ∈ V) |
| 22 | 4, 21 | fexd 7247 |
. 2
⊢ (𝜑 → 𝑀 ∈ V) |
| 23 | | pwexg 5378 |
. . 3
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V) |
| 24 | | rabexg 5337 |
. . 3
⊢
(𝒫 𝑂 ∈
V → {𝑎 ∈
𝒫 𝑂 ∣
∀𝑒 ∈ 𝒫
𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)} ∈ V) |
| 25 | 20, 23, 24 | 3syl 18 |
. 2
⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)} ∈ V) |
| 26 | 1, 19, 22, 25 | fvmptd2 7024 |
1
⊢ (𝜑 → (toCaraSiga‘𝑀) = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)}) |