Proof of Theorem ovmpt2df
Step | Hyp | Ref
| Expression |
1 | | nfv 1418 |
. 2
⊢
Ⅎxφ |
2 | | ovmpt2df.5 |
. . . 4
⊢
Ⅎx𝐹 |
3 | | nfmpt21 5513 |
. . . 4
⊢
Ⅎx(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) |
4 | 2, 3 | nfeq 2182 |
. . 3
⊢
Ⅎx 𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) |
5 | | ovmpt2df.6 |
. . 3
⊢
Ⅎxψ |
6 | 4, 5 | nfim 1461 |
. 2
⊢
Ⅎx(𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) → ψ) |
7 | | ovmpt2df.1 |
. . . 4
⊢ (φ → A ∈ 𝐶) |
8 | | elex 2560 |
. . . 4
⊢ (A ∈ 𝐶 → A ∈
V) |
9 | 7, 8 | syl 14 |
. . 3
⊢ (φ → A ∈
V) |
10 | | isset 2555 |
. . 3
⊢ (A ∈ V ↔ ∃x x = A) |
11 | 9, 10 | sylib 127 |
. 2
⊢ (φ → ∃x x = A) |
12 | | ovmpt2df.2 |
. . . . 5
⊢ ((φ ∧ x = A) →
B ∈ 𝐷) |
13 | | elex 2560 |
. . . . 5
⊢ (B ∈ 𝐷 → B ∈
V) |
14 | 12, 13 | syl 14 |
. . . 4
⊢ ((φ ∧ x = A) →
B ∈
V) |
15 | | isset 2555 |
. . . 4
⊢ (B ∈ V ↔ ∃y y = B) |
16 | 14, 15 | sylib 127 |
. . 3
⊢ ((φ ∧ x = A) →
∃y
y = B) |
17 | | nfv 1418 |
. . . 4
⊢
Ⅎy(φ ∧ x = A) |
18 | | ovmpt2df.7 |
. . . . . 6
⊢
Ⅎy𝐹 |
19 | | nfmpt22 5514 |
. . . . . 6
⊢
Ⅎy(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) |
20 | 18, 19 | nfeq 2182 |
. . . . 5
⊢
Ⅎy 𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) |
21 | | ovmpt2df.8 |
. . . . 5
⊢
Ⅎyψ |
22 | 20, 21 | nfim 1461 |
. . . 4
⊢
Ⅎy(𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) → ψ) |
23 | | oveq 5461 |
. . . . . 6
⊢ (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → (A𝐹B) =
(A(x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)B)) |
24 | | simprl 483 |
. . . . . . . . . 10
⊢ ((φ ∧
(x = A
∧ y =
B)) → x = A) |
25 | | simprr 484 |
. . . . . . . . . 10
⊢ ((φ ∧
(x = A
∧ y =
B)) → y = B) |
26 | 24, 25 | oveq12d 5473 |
. . . . . . . . 9
⊢ ((φ ∧
(x = A
∧ y =
B)) → (x(x ∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)y) =
(A(x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)B)) |
27 | 7 | adantr 261 |
. . . . . . . . . . 11
⊢ ((φ ∧
(x = A
∧ y =
B)) → A ∈ 𝐶) |
28 | 24, 27 | eqeltrd 2111 |
. . . . . . . . . 10
⊢ ((φ ∧
(x = A
∧ y =
B)) → x ∈ 𝐶) |
29 | 12 | adantrr 448 |
. . . . . . . . . . 11
⊢ ((φ ∧
(x = A
∧ y =
B)) → B ∈ 𝐷) |
30 | 25, 29 | eqeltrd 2111 |
. . . . . . . . . 10
⊢ ((φ ∧
(x = A
∧ y =
B)) → y ∈ 𝐷) |
31 | | ovmpt2df.3 |
. . . . . . . . . 10
⊢ ((φ ∧
(x = A
∧ y =
B)) → 𝑅 ∈ 𝑉) |
32 | | eqid 2037 |
. . . . . . . . . . 11
⊢ (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) |
33 | 32 | ovmpt4g 5565 |
. . . . . . . . . 10
⊢
((x ∈ 𝐶 ∧ y ∈ 𝐷 ∧ 𝑅 ∈ 𝑉) → (x(x ∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)y) =
𝑅) |
34 | 28, 30, 31, 33 | syl3anc 1134 |
. . . . . . . . 9
⊢ ((φ ∧
(x = A
∧ y =
B)) → (x(x ∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)y) =
𝑅) |
35 | 26, 34 | eqtr3d 2071 |
. . . . . . . 8
⊢ ((φ ∧
(x = A
∧ y =
B)) → (A(x ∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)B) =
𝑅) |
36 | 35 | eqeq2d 2048 |
. . . . . . 7
⊢ ((φ ∧
(x = A
∧ y =
B)) → ((A𝐹B) =
(A(x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)B)
↔ (A𝐹B) =
𝑅)) |
37 | | ovmpt2df.4 |
. . . . . . 7
⊢ ((φ ∧
(x = A
∧ y =
B)) → ((A𝐹B) =
𝑅 → ψ)) |
38 | 36, 37 | sylbid 139 |
. . . . . 6
⊢ ((φ ∧
(x = A
∧ y =
B)) → ((A𝐹B) =
(A(x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅)B)
→ ψ)) |
39 | 23, 38 | syl5 28 |
. . . . 5
⊢ ((φ ∧
(x = A
∧ y =
B)) → (𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) → ψ)) |
40 | 39 | expr 357 |
. . . 4
⊢ ((φ ∧ x = A) →
(y = B
→ (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))) |
41 | 17, 22, 40 | exlimd 1485 |
. . 3
⊢ ((φ ∧ x = A) →
(∃y
y = B
→ (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))) |
42 | 16, 41 | mpd 13 |
. 2
⊢ ((φ ∧ x = A) →
(𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)) |
43 | 1, 6, 11, 42 | exlimdd 1749 |
1
⊢ (φ → (𝐹 = (x
∈ 𝐶, y
∈ 𝐷 ↦ 𝑅) → ψ)) |