Proof of Theorem fvmptopab
Step | Hyp | Ref
| Expression |
1 | | fvmptopab.3 |
. . . 4
⊢ 𝑀 = (𝑧 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)}) |
2 | | fveq2 6766 |
. . . . . . . 8
⊢ (𝑧 = 𝑍 → (𝐹‘𝑧) = (𝐹‘𝑍)) |
3 | 2 | breqd 5084 |
. . . . . . 7
⊢ (𝑧 = 𝑍 → (𝑥(𝐹‘𝑧)𝑦 ↔ 𝑥(𝐹‘𝑍)𝑦)) |
4 | 3 | adantl 482 |
. . . . . 6
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → (𝑥(𝐹‘𝑧)𝑦 ↔ 𝑥(𝐹‘𝑍)𝑦)) |
5 | | fvmptopab.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓)) |
6 | 5 | adantll 711 |
. . . . . 6
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓)) |
7 | 4, 6 | anbi12d 631 |
. . . . 5
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → ((𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒) ↔ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓))) |
8 | 7 | opabbidv 5139 |
. . . 4
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)} = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
9 | | simpl 483 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝑍 ∈ V) |
10 | | id 22 |
. . . . . 6
⊢ (𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) |
11 | 10 | gen2 1799 |
. . . . 5
⊢
∀𝑥∀𝑦(𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) |
12 | | fvmptopab.2 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) |
13 | 12 | adantl 482 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ 𝜑) → {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) |
14 | | opabbrex 7318 |
. . . . 5
⊢
((∀𝑥∀𝑦(𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) ∧ {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} ∈ V) |
15 | 11, 13, 14 | sylancr 587 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} ∈ V) |
16 | 1, 8, 9, 15 | fvmptd2 6875 |
. . 3
⊢ ((𝑍 ∈ V ∧ 𝜑) → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
17 | 16 | ex 413 |
. 2
⊢ (𝑍 ∈ V → (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)})) |
18 | | fvprc 6758 |
. . . 4
⊢ (¬
𝑍 ∈ V → (𝑀‘𝑍) = ∅) |
19 | | br0 5122 |
. . . . . . . 8
⊢ ¬
𝑥∅𝑦 |
20 | | fvprc 6758 |
. . . . . . . . 9
⊢ (¬
𝑍 ∈ V → (𝐹‘𝑍) = ∅) |
21 | 20 | breqd 5084 |
. . . . . . . 8
⊢ (¬
𝑍 ∈ V → (𝑥(𝐹‘𝑍)𝑦 ↔ 𝑥∅𝑦)) |
22 | 19, 21 | mtbiri 327 |
. . . . . . 7
⊢ (¬
𝑍 ∈ V → ¬
𝑥(𝐹‘𝑍)𝑦) |
23 | 22 | intnanrd 490 |
. . . . . 6
⊢ (¬
𝑍 ∈ V → ¬
(𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
24 | 23 | alrimivv 1931 |
. . . . 5
⊢ (¬
𝑍 ∈ V →
∀𝑥∀𝑦 ¬ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
25 | | opab0 5464 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} = ∅ ↔ ∀𝑥∀𝑦 ¬ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
26 | 24, 25 | sylibr 233 |
. . . 4
⊢ (¬
𝑍 ∈ V →
{〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} = ∅) |
27 | 18, 26 | eqtr4d 2781 |
. . 3
⊢ (¬
𝑍 ∈ V → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
28 | 27 | a1d 25 |
. 2
⊢ (¬
𝑍 ∈ V → (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)})) |
29 | 17, 28 | pm2.61i 182 |
1
⊢ (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |