Proof of Theorem ovmpodf
| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. 2
⊢
Ⅎ𝑥𝜑 |
| 2 | | ovmpodf.5 |
. . . 4
⊢
Ⅎ𝑥𝐹 |
| 3 | | nfmpo1 7513 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
| 4 | 2, 3 | nfeq 2919 |
. . 3
⊢
Ⅎ𝑥 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
| 5 | | ovmpodf.6 |
. . 3
⊢
Ⅎ𝑥𝜓 |
| 6 | 4, 5 | nfim 1896 |
. 2
⊢
Ⅎ𝑥(𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓) |
| 7 | | ovmpodf.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
| 8 | 7 | elexd 3504 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
| 9 | | isset 3494 |
. . 3
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
| 10 | 8, 9 | sylib 218 |
. 2
⊢ (𝜑 → ∃𝑥 𝑥 = 𝐴) |
| 11 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 = 𝐴) |
| 12 | | ovmpodf.7 |
. . . . 5
⊢
Ⅎ𝑦𝐹 |
| 13 | | nfmpo2 7514 |
. . . . 5
⊢
Ⅎ𝑦(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
| 14 | 12, 13 | nfeq 2919 |
. . . 4
⊢
Ⅎ𝑦 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
| 15 | | ovmpodf.8 |
. . . 4
⊢
Ⅎ𝑦𝜓 |
| 16 | 14, 15 | nfim 1896 |
. . 3
⊢
Ⅎ𝑦(𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓) |
| 17 | | ovmpodf.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) |
| 18 | 17 | elexd 3504 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ V) |
| 19 | | isset 3494 |
. . . 4
⊢ (𝐵 ∈ V ↔ ∃𝑦 𝑦 = 𝐵) |
| 20 | 18, 19 | sylib 218 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ∃𝑦 𝑦 = 𝐵) |
| 21 | | oveq 7437 |
. . . . 5
⊢ (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)) |
| 22 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑥 = 𝐴) |
| 23 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑦 = 𝐵) |
| 24 | 22, 23 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)) |
| 25 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐴 ∈ 𝐶) |
| 26 | 22, 25 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑥 ∈ 𝐶) |
| 27 | 17 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐵 ∈ 𝐷) |
| 28 | 23, 27 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑦 ∈ 𝐷) |
| 29 | | ovmpodf.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) |
| 30 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
| 31 | 30 | ovmpt4g 7580 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ 𝑉) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) |
| 32 | 26, 28, 29, 31 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) |
| 33 | 24, 32 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑅) |
| 34 | 33 | eqeq2d 2748 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) ↔ (𝐴𝐹𝐵) = 𝑅)) |
| 35 | | ovmpodf.4 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) |
| 36 | 34, 35 | sylbid 240 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) → 𝜓)) |
| 37 | 21, 36 | syl5 34 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
| 38 | 37 | expr 456 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑦 = 𝐵 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓))) |
| 39 | 11, 16, 20, 38 | exlimimdd 2219 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
| 40 | 1, 6, 10, 39 | exlimdd 2220 |
1
⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |