Proof of Theorem fvmptopab
Step | Hyp | Ref
| Expression |
1 | | fvmptopab.3 |
. . . . 5
⊢ 𝑀 = (𝑧 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)}) |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝑀 = (𝑧 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)})) |
3 | | fveq2 6411 |
. . . . . . . 8
⊢ (𝑧 = 𝑍 → (𝐹‘𝑧) = (𝐹‘𝑍)) |
4 | 3 | breqd 4854 |
. . . . . . 7
⊢ (𝑧 = 𝑍 → (𝑥(𝐹‘𝑧)𝑦 ↔ 𝑥(𝐹‘𝑍)𝑦)) |
5 | 4 | adantl 474 |
. . . . . 6
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → (𝑥(𝐹‘𝑧)𝑦 ↔ 𝑥(𝐹‘𝑍)𝑦)) |
6 | | fvmptopab.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓)) |
7 | 6 | adantll 706 |
. . . . . 6
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓)) |
8 | 5, 7 | anbi12d 625 |
. . . . 5
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → ((𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒) ↔ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓))) |
9 | 8 | opabbidv 4909 |
. . . 4
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)} = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
10 | | simpl 475 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝑍 ∈ V) |
11 | | id 22 |
. . . . . 6
⊢ (𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) |
12 | 11 | gen2 1892 |
. . . . 5
⊢
∀𝑥∀𝑦(𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) |
13 | | fvmptopab.2 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) |
14 | 13 | adantl 474 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ 𝜑) → {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) |
15 | | opabbrex 6929 |
. . . . 5
⊢
((∀𝑥∀𝑦(𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) ∧ {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} ∈ V) |
16 | 12, 14, 15 | sylancr 582 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} ∈ V) |
17 | 2, 9, 10, 16 | fvmptd 6513 |
. . 3
⊢ ((𝑍 ∈ V ∧ 𝜑) → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
18 | 17 | ex 402 |
. 2
⊢ (𝑍 ∈ V → (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)})) |
19 | | fvprc 6404 |
. . . 4
⊢ (¬
𝑍 ∈ V → (𝑀‘𝑍) = ∅) |
20 | | br0 4892 |
. . . . . . . 8
⊢ ¬
𝑥∅𝑦 |
21 | | fvprc 6404 |
. . . . . . . . 9
⊢ (¬
𝑍 ∈ V → (𝐹‘𝑍) = ∅) |
22 | 21 | breqd 4854 |
. . . . . . . 8
⊢ (¬
𝑍 ∈ V → (𝑥(𝐹‘𝑍)𝑦 ↔ 𝑥∅𝑦)) |
23 | 20, 22 | mtbiri 319 |
. . . . . . 7
⊢ (¬
𝑍 ∈ V → ¬
𝑥(𝐹‘𝑍)𝑦) |
24 | 23 | intnanrd 484 |
. . . . . 6
⊢ (¬
𝑍 ∈ V → ¬
(𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
25 | 24 | alrimivv 2024 |
. . . . 5
⊢ (¬
𝑍 ∈ V →
∀𝑥∀𝑦 ¬ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
26 | | opab0 5203 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} = ∅ ↔ ∀𝑥∀𝑦 ¬ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
27 | 25, 26 | sylibr 226 |
. . . 4
⊢ (¬
𝑍 ∈ V →
{〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} = ∅) |
28 | 19, 27 | eqtr4d 2836 |
. . 3
⊢ (¬
𝑍 ∈ V → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
29 | 28 | a1d 25 |
. 2
⊢ (¬
𝑍 ∈ V → (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)})) |
30 | 18, 29 | pm2.61i 177 |
1
⊢ (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |