Proof of Theorem ovmpodxf
Step | Hyp | Ref
| Expression |
1 | | ovmpodx.1 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)) |
2 | 1 | oveqd 7187 |
. 2
⊢ (𝜑 → (𝐴𝐹𝐵) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)) |
3 | | ovmpodx.4 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
4 | | ovmpodxf.px |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
5 | | ovmpodx.5 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐿) |
6 | | ovmpodxf.py |
. . . . . . 7
⊢
Ⅎ𝑦𝜑 |
7 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
8 | 7 | ovmpt4g 7312 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅)) |
10 | 6, 9 | alrimi 2215 |
. . . . . 6
⊢ (𝜑 → ∀𝑦((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅)) |
11 | 5, 10 | spsbcd 3694 |
. . . . 5
⊢ (𝜑 → [𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅)) |
12 | 4, 11 | alrimi 2215 |
. . . 4
⊢ (𝜑 → ∀𝑥[𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅)) |
13 | 3, 12 | spsbcd 3694 |
. . 3
⊢ (𝜑 → [𝐴 / 𝑥][𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅)) |
14 | 5 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 ∈ 𝐿) |
15 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 = 𝐴) |
16 | 3 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝐴 ∈ 𝐶) |
17 | 15, 16 | eqeltrd 2833 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 ∈ 𝐶) |
18 | 5 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝐵 ∈ 𝐿) |
19 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
20 | | ovmpodx.3 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐿) |
21 | 20 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝐷 = 𝐿) |
22 | 18, 19, 21 | 3eltr4d 2848 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 ∈ 𝐷) |
23 | | ovmpodx.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆) |
24 | 23 | anassrs 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑅 = 𝑆) |
25 | | ovmpodx.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ 𝑋) |
26 | 25 | elexd 3418 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ V) |
27 | 26 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑆 ∈ V) |
28 | 24, 27 | eqeltrd 2833 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → 𝑅 ∈ V) |
29 | | biimt 364 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → ((𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅 ↔ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅))) |
30 | 17, 22, 28, 29 | syl3anc 1372 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → ((𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅 ↔ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅))) |
31 | 15, 19 | oveq12d 7188 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵)) |
32 | 31, 24 | eqeq12d 2754 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → ((𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅 ↔ (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆)) |
33 | 30, 32 | bitr3d 284 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 = 𝐴) ∧ 𝑦 = 𝐵) → (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) ↔ (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆)) |
34 | | ovmpodxf.ay |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
35 | 34 | nfeq2 2916 |
. . . . . 6
⊢
Ⅎ𝑦 𝑥 = 𝐴 |
36 | 6, 35 | nfan 1906 |
. . . . 5
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 = 𝐴) |
37 | | nfmpo2 7249 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
38 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑦𝐵 |
39 | 34, 37, 38 | nfov 7200 |
. . . . . . 7
⊢
Ⅎ𝑦(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) |
40 | | ovmpodxf.sy |
. . . . . . 7
⊢
Ⅎ𝑦𝑆 |
41 | 39, 40 | nfeq 2912 |
. . . . . 6
⊢
Ⅎ𝑦(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆 |
42 | 41 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → Ⅎ𝑦(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆) |
43 | 14, 33, 36, 42 | sbciedf 3723 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝐴) → ([𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) ↔ (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆)) |
44 | | nfcv 2899 |
. . . . . . 7
⊢
Ⅎ𝑥𝐴 |
45 | | nfmpo1 7248 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) |
46 | | ovmpodxf.bx |
. . . . . . 7
⊢
Ⅎ𝑥𝐵 |
47 | 44, 45, 46 | nfov 7200 |
. . . . . 6
⊢
Ⅎ𝑥(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) |
48 | | ovmpodxf.sx |
. . . . . 6
⊢
Ⅎ𝑥𝑆 |
49 | 47, 48 | nfeq 2912 |
. . . . 5
⊢
Ⅎ𝑥(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆 |
50 | 49 | a1i 11 |
. . . 4
⊢ (𝜑 → Ⅎ𝑥(𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆) |
51 | 3, 43, 4, 50 | sbciedf 3723 |
. . 3
⊢ (𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ∧ 𝑅 ∈ V) → (𝑥(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝑦) = 𝑅) ↔ (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆)) |
52 | 13, 51 | mpbid 235 |
. 2
⊢ (𝜑 → (𝐴(𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅)𝐵) = 𝑆) |
53 | 2, 52 | eqtrd 2773 |
1
⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆) |