Proof of Theorem ovmpodf
Step | Hyp | Ref
| Expression |
1 | | nfv 1521 |
. 2
⊢
Ⅎ𝑥𝜑 |
2 | | ovmpodf.5 |
. . . 4
⊢
Ⅎ𝑥𝐹 |
3 | | nfmpo1 5920 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
4 | 2, 3 | nfeq 2320 |
. . 3
⊢
Ⅎ𝑥 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
5 | | ovmpodf.6 |
. . 3
⊢
Ⅎ𝑥𝜓 |
6 | 4, 5 | nfim 1565 |
. 2
⊢
Ⅎ𝑥(𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓) |
7 | | ovmpodf.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
8 | | elex 2741 |
. . . 4
⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V) |
9 | 7, 8 | syl 14 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
10 | | isset 2736 |
. . 3
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
11 | 9, 10 | sylib 121 |
. 2
⊢ (𝜑 → ∃𝑥 𝑥 = 𝐴) |
12 | | ovmpodf.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) |
13 | | elex 2741 |
. . . . 5
⊢ (𝐵 ∈ 𝐷 → 𝐵 ∈ V) |
14 | 12, 13 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ V) |
15 | | isset 2736 |
. . . 4
⊢ (𝐵 ∈ V ↔ ∃𝑦 𝑦 = 𝐵) |
16 | 14, 15 | sylib 121 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ∃𝑦 𝑦 = 𝐵) |
17 | | nfv 1521 |
. . . 4
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 = 𝐴) |
18 | | ovmpodf.7 |
. . . . . 6
⊢
Ⅎ𝑦𝐹 |
19 | | nfmpo2 5921 |
. . . . . 6
⊢
Ⅎ𝑦(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
20 | 18, 19 | nfeq 2320 |
. . . . 5
⊢
Ⅎ𝑦 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
21 | | ovmpodf.8 |
. . . . 5
⊢
Ⅎ𝑦𝜓 |
22 | 20, 21 | nfim 1565 |
. . . 4
⊢
Ⅎ𝑦(𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓) |
23 | | oveq 5859 |
. . . . . 6
⊢ (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)) |
24 | | simprl 526 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑥 = 𝐴) |
25 | | simprr 527 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑦 = 𝐵) |
26 | 24, 25 | oveq12d 5871 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)) |
27 | 7 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐴 ∈ 𝐶) |
28 | 24, 27 | eqeltrd 2247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑥 ∈ 𝐶) |
29 | 12 | adantrr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐵 ∈ 𝐷) |
30 | 25, 29 | eqeltrd 2247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑦 ∈ 𝐷) |
31 | | ovmpodf.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) |
32 | | eqid 2170 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
33 | 32 | ovmpt4g 5975 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ 𝑉) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) |
34 | 28, 30, 31, 33 | syl3anc 1233 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) |
35 | 26, 34 | eqtr3d 2205 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑅) |
36 | 35 | eqeq2d 2182 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) ↔ (𝐴𝐹𝐵) = 𝑅)) |
37 | | ovmpodf.4 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) |
38 | 36, 37 | sylbid 149 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) → 𝜓)) |
39 | 23, 38 | syl5 32 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
40 | 39 | expr 373 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑦 = 𝐵 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓))) |
41 | 17, 22, 40 | exlimd 1590 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (∃𝑦 𝑦 = 𝐵 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓))) |
42 | 16, 41 | mpd 13 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
43 | 1, 6, 11, 42 | exlimdd 1865 |
1
⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |