Step | Hyp | Ref
| Expression |
1 | | carsgval.1 |
. . . 4
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
2 | | carsgval.2 |
. . . 4
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
3 | 1, 2 | carsgval 29692 |
. . 3
⊢ (𝜑 → (toCaraSiga‘𝑀) = {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)}) |
4 | 3 | eleq2d 2673 |
. 2
⊢ (𝜑 → (𝐴 ∈ (toCaraSiga‘𝑀) ↔ 𝐴 ∈ {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)})) |
5 | | ineq2 3770 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑒 ∩ 𝑎) = (𝑒 ∩ 𝐴)) |
6 | 5 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑀‘(𝑒 ∩ 𝑎)) = (𝑀‘(𝑒 ∩ 𝐴))) |
7 | | difeq2 3684 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑒 ∖ 𝑎) = (𝑒 ∖ 𝐴)) |
8 | 7 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑀‘(𝑒 ∖ 𝑎)) = (𝑀‘(𝑒 ∖ 𝐴))) |
9 | 6, 8 | oveq12d 6567 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = ((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴)))) |
10 | 9 | eqeq1d 2612 |
. . . . 5
⊢ (𝑎 = 𝐴 → (((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒) ↔ ((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒))) |
11 | 10 | ralbidv 2969 |
. . . 4
⊢ (𝑎 = 𝐴 → (∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒) ↔ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒))) |
12 | 11 | elrab 3331 |
. . 3
⊢ (𝐴 ∈ {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)} ↔ (𝐴 ∈ 𝒫 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒))) |
13 | | elex 3185 |
. . . . . 6
⊢ (𝐴 ∈ 𝒫 𝑂 → 𝐴 ∈ V) |
14 | 13 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ 𝒫 𝑂 → 𝐴 ∈ V)) |
15 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝑂) → 𝐴 ⊆ 𝑂) |
16 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝑂) → 𝑂 ∈ 𝑉) |
17 | | ssexg 4732 |
. . . . . . 7
⊢ ((𝐴 ⊆ 𝑂 ∧ 𝑂 ∈ 𝑉) → 𝐴 ∈ V) |
18 | 15, 16, 17 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ⊆ 𝑂) → 𝐴 ∈ V) |
19 | 18 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝐴 ⊆ 𝑂 → 𝐴 ∈ V)) |
20 | | elpwg 4116 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝑂 ↔ 𝐴 ⊆ 𝑂)) |
21 | 20 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝑂 ↔ 𝐴 ⊆ 𝑂))) |
22 | 14, 19, 21 | pm5.21ndd 368 |
. . . 4
⊢ (𝜑 → (𝐴 ∈ 𝒫 𝑂 ↔ 𝐴 ⊆ 𝑂)) |
23 | 22 | anbi1d 737 |
. . 3
⊢ (𝜑 → ((𝐴 ∈ 𝒫 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒)) ↔ (𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒)))) |
24 | 12, 23 | syl5bb 271 |
. 2
⊢ (𝜑 → (𝐴 ∈ {𝑎 ∈ 𝒫 𝑂 ∣ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝑎)) +𝑒 (𝑀‘(𝑒 ∖ 𝑎))) = (𝑀‘𝑒)} ↔ (𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒)))) |
25 | 4, 24 | bitrd 267 |
1
⊢ (𝜑 → (𝐴 ∈ (toCaraSiga‘𝑀) ↔ (𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ 𝐴))) = (𝑀‘𝑒)))) |