Step | Hyp | Ref
| Expression |
1 | | df-carsg 30905 |
. . 3
⊢
toCaraSiga = (𝑚
∈ V ↦ {𝑎 ∈
𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)}) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})) |
3 | | simpr 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀) |
4 | 3 | dmeqd 5562 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑚 = dom 𝑀) |
5 | | carsgval.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
6 | 5 | fdmd 6291 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑀 = 𝒫 𝑂) |
7 | 6 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑀 = 𝒫 𝑂) |
8 | 4, 7 | eqtrd 2861 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑚 = 𝒫 𝑂) |
9 | 8 | unieqd 4670 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → ∪ dom
𝑚 = ∪ 𝒫 𝑂) |
10 | | unipw 5141 |
. . . . 5
⊢ ∪ 𝒫 𝑂 = 𝑂 |
11 | 9, 10 | syl6eq 2877 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → ∪ dom
𝑚 = 𝑂) |
12 | 11 | pweqd 4385 |
. . 3
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → 𝒫 ∪ dom 𝑚 = 𝒫 𝑂) |
13 | | fveq1 6436 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚‘(𝑒 ∩ 𝑎)) = (𝑀‘(𝑒 ∩ 𝑎))) |
14 | | fveq1 6436 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚‘(𝑒 ∖ 𝑎)) = (𝑀‘(𝑒 ∖ 𝑎))) |
15 | 13, 14 | oveq12d 6928 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎)))) |
16 | | fveq1 6436 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (𝑚‘𝑒) = (𝑀‘𝑒)) |
17 | 15, 16 | eqeq12d 2840 |
. . . . 5
⊢ (𝑚 = 𝑀 → (((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
18 | 17 | adantl 475 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → (((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
19 | 12, 18 | raleqbidv 3364 |
. . 3
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → (∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
20 | 12, 19 | rabeqbidv 3408 |
. 2
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)} = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)}) |
21 | | carsgval.1 |
. . . 4
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
22 | 21 | pwexd 5081 |
. . 3
⊢ (𝜑 → 𝒫 𝑂 ∈ V) |
23 | | fex 6750 |
. . 3
⊢ ((𝑀:𝒫 𝑂⟶(0[,]+∞) ∧ 𝒫 𝑂 ∈ V) → 𝑀 ∈ V) |
24 | 5, 22, 23 | syl2anc 579 |
. 2
⊢ (𝜑 → 𝑀 ∈ V) |
25 | | pwexg 5080 |
. . 3
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V) |
26 | | rabexg 5038 |
. . 3
⊢
(𝒫 𝑂 ∈
V → {𝑎 ∈
𝒫 𝑂 ∣
∀𝑒 ∈ 𝒫
𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)} ∈ V) |
27 | 21, 25, 26 | 3syl 18 |
. 2
⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)} ∈ V) |
28 | 2, 20, 24, 27 | fvmptd 6539 |
1
⊢ (𝜑 → (toCaraSiga‘𝑀) = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)}) |