Step | Hyp | Ref
| Expression |
1 | | df-carsg 29691 |
. . 3
⊢
toCaraSiga = (𝑚
∈ V ↦ {𝑎 ∈
𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)}) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → toCaraSiga = (𝑚 ∈ V ↦ {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)})) |
3 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀) |
4 | 3 | dmeqd 5248 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑚 = dom 𝑀) |
5 | | carsgval.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
6 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝑀:𝒫 𝑂⟶(0[,]+∞) → dom 𝑀 = 𝒫 𝑂) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑀 = 𝒫 𝑂) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑀 = 𝒫 𝑂) |
9 | 4, 8 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → dom 𝑚 = 𝒫 𝑂) |
10 | 9 | unieqd 4382 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → ∪ dom
𝑚 = ∪ 𝒫 𝑂) |
11 | | unipw 4845 |
. . . . 5
⊢ ∪ 𝒫 𝑂 = 𝑂 |
12 | 10, 11 | syl6eq 2660 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → ∪ dom
𝑚 = 𝑂) |
13 | 12 | pweqd 4113 |
. . 3
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → 𝒫 ∪ dom 𝑚 = 𝒫 𝑂) |
14 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚‘(𝑒 ∩ 𝑎)) = (𝑀‘(𝑒 ∩ 𝑎))) |
15 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑚 = 𝑀 → (𝑚‘(𝑒 ∖ 𝑎)) = (𝑀‘(𝑒 ∖ 𝑎))) |
16 | 14, 15 | oveq12d 6567 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎)))) |
17 | | fveq1 6102 |
. . . . . 6
⊢ (𝑚 = 𝑀 → (𝑚‘𝑒) = (𝑀‘𝑒)) |
18 | 16, 17 | eqeq12d 2625 |
. . . . 5
⊢ (𝑚 = 𝑀 → (((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
19 | 18 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → (((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
20 | 13, 19 | raleqbidv 3129 |
. . 3
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → (∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒) ↔ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒))) |
21 | 13, 20 | rabeqbidv 3168 |
. 2
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → {𝑎 ∈ 𝒫 ∪ dom 𝑚 ∣ ∀𝑒 ∈ 𝒫 ∪ dom 𝑚((𝑚‘(𝑒 ∩ 𝑎)) +𝑒 (𝑚‘(𝑒 ∖ 𝑎))) = (𝑚‘𝑒)} = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)}) |
22 | | carsgval.1 |
. . . 4
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
23 | | pwexg 4776 |
. . . 4
⊢ (𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V) |
24 | 22, 23 | syl 17 |
. . 3
⊢ (𝜑 → 𝒫 𝑂 ∈ V) |
25 | | fex 6394 |
. . 3
⊢ ((𝑀:𝒫 𝑂⟶(0[,]+∞) ∧ 𝒫 𝑂 ∈ V) → 𝑀 ∈ V) |
26 | 5, 24, 25 | syl2anc 691 |
. 2
⊢ (𝜑 → 𝑀 ∈ V) |
27 | | rabexg 4739 |
. . 3
⊢
(𝒫 𝑂 ∈
V → {𝑎 ∈
𝒫 𝑂 ∣
∀𝑒 ∈ 𝒫
𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)} ∈ V) |
28 | 22, 23, 27 | 3syl 18 |
. 2
⊢ (𝜑 → {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)} ∈ V) |
29 | 2, 21, 26, 28 | fvmptd 6197 |
1
⊢ (𝜑 → (toCaraSiga‘𝑀) = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)}) |