Proof of Theorem fvmptopabOLD
| Step | Hyp | Ref
| Expression |
| 1 | | fvmptopabOLD.3 |
. . . 4
⊢ 𝑀 = (𝑧 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)}) |
| 2 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑧 = 𝑍 → (𝐹‘𝑧) = (𝐹‘𝑍)) |
| 3 | 2 | breqd 5154 |
. . . . . . 7
⊢ (𝑧 = 𝑍 → (𝑥(𝐹‘𝑧)𝑦 ↔ 𝑥(𝐹‘𝑍)𝑦)) |
| 4 | 3 | adantl 481 |
. . . . . 6
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → (𝑥(𝐹‘𝑧)𝑦 ↔ 𝑥(𝐹‘𝑍)𝑦)) |
| 5 | | fvmptopabOLD.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓)) |
| 6 | 5 | adantll 714 |
. . . . . 6
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → (𝜒 ↔ 𝜓)) |
| 7 | 4, 6 | anbi12d 632 |
. . . . 5
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → ((𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒) ↔ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓))) |
| 8 | 7 | opabbidv 5209 |
. . . 4
⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑧 = 𝑍) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑧)𝑦 ∧ 𝜒)} = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
| 9 | | simpl 482 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝑍 ∈ V) |
| 10 | | id 22 |
. . . . . 6
⊢ (𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) |
| 11 | 10 | gen2 1796 |
. . . . 5
⊢
∀𝑥∀𝑦(𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) |
| 12 | | fvmptopabOLD.2 |
. . . . . 6
⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) |
| 13 | 12 | adantl 481 |
. . . . 5
⊢ ((𝑍 ∈ V ∧ 𝜑) → {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) |
| 14 | | opabbrex 7484 |
. . . . 5
⊢
((∀𝑥∀𝑦(𝑥(𝐹‘𝑍)𝑦 → 𝑥(𝐹‘𝑍)𝑦) ∧ {〈𝑥, 𝑦〉 ∣ 𝑥(𝐹‘𝑍)𝑦} ∈ V) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} ∈ V) |
| 15 | 11, 13, 14 | sylancr 587 |
. . . 4
⊢ ((𝑍 ∈ V ∧ 𝜑) → {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} ∈ V) |
| 16 | 1, 8, 9, 15 | fvmptd2 7024 |
. . 3
⊢ ((𝑍 ∈ V ∧ 𝜑) → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
| 17 | 16 | ex 412 |
. 2
⊢ (𝑍 ∈ V → (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)})) |
| 18 | | fvprc 6898 |
. . . 4
⊢ (¬
𝑍 ∈ V → (𝑀‘𝑍) = ∅) |
| 19 | | br0 5192 |
. . . . . . . 8
⊢ ¬
𝑥∅𝑦 |
| 20 | | fvprc 6898 |
. . . . . . . . 9
⊢ (¬
𝑍 ∈ V → (𝐹‘𝑍) = ∅) |
| 21 | 20 | breqd 5154 |
. . . . . . . 8
⊢ (¬
𝑍 ∈ V → (𝑥(𝐹‘𝑍)𝑦 ↔ 𝑥∅𝑦)) |
| 22 | 19, 21 | mtbiri 327 |
. . . . . . 7
⊢ (¬
𝑍 ∈ V → ¬
𝑥(𝐹‘𝑍)𝑦) |
| 23 | 22 | intnanrd 489 |
. . . . . 6
⊢ (¬
𝑍 ∈ V → ¬
(𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
| 24 | 23 | alrimivv 1928 |
. . . . 5
⊢ (¬
𝑍 ∈ V →
∀𝑥∀𝑦 ¬ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
| 25 | | opab0 5559 |
. . . . 5
⊢
({〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} = ∅ ↔ ∀𝑥∀𝑦 ¬ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)) |
| 26 | 24, 25 | sylibr 234 |
. . . 4
⊢ (¬
𝑍 ∈ V →
{〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)} = ∅) |
| 27 | 18, 26 | eqtr4d 2780 |
. . 3
⊢ (¬
𝑍 ∈ V → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |
| 28 | 27 | a1d 25 |
. 2
⊢ (¬
𝑍 ∈ V → (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)})) |
| 29 | 17, 28 | pm2.61i 182 |
1
⊢ (𝜑 → (𝑀‘𝑍) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝐹‘𝑍)𝑦 ∧ 𝜓)}) |