Proof of Theorem ovmpodf
Step | Hyp | Ref
| Expression |
1 | | nfv 1920 |
. 2
⊢
Ⅎ𝑥𝜑 |
2 | | ovmpodf.5 |
. . . 4
⊢
Ⅎ𝑥𝐹 |
3 | | nfmpo1 7242 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
4 | 2, 3 | nfeq 2912 |
. . 3
⊢
Ⅎ𝑥 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
5 | | ovmpodf.6 |
. . 3
⊢
Ⅎ𝑥𝜓 |
6 | 4, 5 | nfim 1902 |
. 2
⊢
Ⅎ𝑥(𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓) |
7 | | ovmpodf.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
8 | 7 | elexd 3417 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
9 | | isset 3410 |
. . 3
⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴) |
10 | 8, 9 | sylib 221 |
. 2
⊢ (𝜑 → ∃𝑥 𝑥 = 𝐴) |
11 | | nfv 1920 |
. . 3
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 = 𝐴) |
12 | | ovmpodf.7 |
. . . . 5
⊢
Ⅎ𝑦𝐹 |
13 | | nfmpo2 7243 |
. . . . 5
⊢
Ⅎ𝑦(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
14 | 12, 13 | nfeq 2912 |
. . . 4
⊢
Ⅎ𝑦 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
15 | | ovmpodf.8 |
. . . 4
⊢
Ⅎ𝑦𝜓 |
16 | 14, 15 | nfim 1902 |
. . 3
⊢
Ⅎ𝑦(𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓) |
17 | | ovmpodf.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐷) |
18 | 17 | elexd 3417 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ V) |
19 | | isset 3410 |
. . . 4
⊢ (𝐵 ∈ V ↔ ∃𝑦 𝑦 = 𝐵) |
20 | 18, 19 | sylib 221 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ∃𝑦 𝑦 = 𝐵) |
21 | | oveq 7170 |
. . . . 5
⊢ (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → (𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)) |
22 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑥 = 𝐴) |
23 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑦 = 𝐵) |
24 | 22, 23 | oveq12d 7182 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)) |
25 | 7 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐴 ∈ 𝐶) |
26 | 22, 25 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑥 ∈ 𝐶) |
27 | 17 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝐵 ∈ 𝐷) |
28 | 23, 27 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑦 ∈ 𝐷) |
29 | | ovmpodf.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 ∈ 𝑉) |
30 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
31 | 30 | ovmpt4g 7306 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ 𝑉) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) |
32 | 26, 28, 29, 31 | syl3anc 1372 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) |
33 | 24, 32 | eqtr3d 2775 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑅) |
34 | 33 | eqeq2d 2749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) ↔ (𝐴𝐹𝐵) = 𝑅)) |
35 | | ovmpodf.4 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = 𝑅 → 𝜓)) |
36 | 34, 35 | sylbid 243 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → ((𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) → 𝜓)) |
37 | 21, 36 | syl5 34 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
38 | 37 | expr 460 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝑦 = 𝐵 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓))) |
39 | 11, 16, 20, 38 | exlimimdd 2220 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |
40 | 1, 6, 10, 39 | exlimdd 2221 |
1
⊢ (𝜑 → (𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) → 𝜓)) |