Step | Hyp | Ref
| Expression |
1 | | opelxp 5146 |
. . 3
⊢
(〈〈𝐷,
𝐻〉, 𝐴〉 ∈ (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) ↔ (〈𝐷, 𝐻〉 ∈ ({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ∧ 𝐴 ∈ 𝐸)) |
2 | | opelxp 5146 |
. . . . 5
⊢
(〈𝐷, 𝐻〉 ∈ ({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ↔ (𝐷 ∈ {𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} ∧ 𝐻 ∈ (𝒫 𝐸 ∩ Fin))) |
3 | | cnveq 5296 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → ◡𝑑 = ◡𝐷) |
4 | | id 22 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → 𝑑 = 𝐷) |
5 | 3, 4 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (◡𝑑 = 𝑑 ↔ ◡𝐷 = 𝐷)) |
6 | 5 | elrab 3363 |
. . . . . . 7
⊢ (𝐷 ∈ {𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} ↔ (𝐷 ∈ 𝒫 𝑉 ∧ ◡𝐷 = 𝐷)) |
7 | | mpstval.v |
. . . . . . . . . 10
⊢ 𝑉 = (mDV‘𝑇) |
8 | | fvex 6201 |
. . . . . . . . . 10
⊢
(mDV‘𝑇) ∈
V |
9 | 7, 8 | eqeltri 2697 |
. . . . . . . . 9
⊢ 𝑉 ∈ V |
10 | 9 | elpw2 4828 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝒫 𝑉 ↔ 𝐷 ⊆ 𝑉) |
11 | 10 | anbi1i 731 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝒫 𝑉 ∧ ◡𝐷 = 𝐷) ↔ (𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷)) |
12 | 6, 11 | bitri 264 |
. . . . . 6
⊢ (𝐷 ∈ {𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} ↔ (𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷)) |
13 | | elfpw 8268 |
. . . . . 6
⊢ (𝐻 ∈ (𝒫 𝐸 ∩ Fin) ↔ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin)) |
14 | 12, 13 | anbi12i 733 |
. . . . 5
⊢ ((𝐷 ∈ {𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} ∧ 𝐻 ∈ (𝒫 𝐸 ∩ Fin)) ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin))) |
15 | 2, 14 | bitri 264 |
. . . 4
⊢
(〈𝐷, 𝐻〉 ∈ ({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin))) |
16 | 15 | anbi1i 731 |
. . 3
⊢
((〈𝐷, 𝐻〉 ∈ ({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) ∧ 𝐴 ∈ 𝐸) ↔ (((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin)) ∧ 𝐴 ∈ 𝐸)) |
17 | 1, 16 | bitri 264 |
. 2
⊢
(〈〈𝐷,
𝐻〉, 𝐴〉 ∈ (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) ↔ (((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin)) ∧ 𝐴 ∈ 𝐸)) |
18 | | df-ot 4186 |
. . 3
⊢
〈𝐷, 𝐻, 𝐴〉 = 〈〈𝐷, 𝐻〉, 𝐴〉 |
19 | | mpstval.e |
. . . 4
⊢ 𝐸 = (mEx‘𝑇) |
20 | | mpstval.p |
. . . 4
⊢ 𝑃 = (mPreSt‘𝑇) |
21 | 7, 19, 20 | mpstval 31432 |
. . 3
⊢ 𝑃 = (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸) |
22 | 18, 21 | eleq12i 2694 |
. 2
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ↔ 〈〈𝐷, 𝐻〉, 𝐴〉 ∈ (({𝑑 ∈ 𝒫 𝑉 ∣ ◡𝑑 = 𝑑} × (𝒫 𝐸 ∩ Fin)) × 𝐸)) |
23 | | df-3an 1039 |
. 2
⊢ (((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸) ↔ (((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin)) ∧ 𝐴 ∈ 𝐸)) |
24 | 17, 22, 23 | 3bitr4i 292 |
1
⊢
(〈𝐷, 𝐻, 𝐴〉 ∈ 𝑃 ↔ ((𝐷 ⊆ 𝑉 ∧ ◡𝐷 = 𝐷) ∧ (𝐻 ⊆ 𝐸 ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ 𝐸)) |