Proof of Theorem ovmpt2s
Step | Hyp | Ref
| Expression |
1 | | elex 2560 |
. . 3
⊢
(⦋A / x⦌⦋B / y⦌𝑅 ∈ 𝑉 → ⦋A / x⦌⦋B / y⦌𝑅 ∈
V) |
2 | | nfcv 2175 |
. . . . 5
⊢
ℲxA |
3 | | nfcv 2175 |
. . . . 5
⊢
ℲyA |
4 | | nfcv 2175 |
. . . . 5
⊢
ℲyB |
5 | | nfcsb1v 2876 |
. . . . . . 7
⊢
Ⅎx⦋A / x⦌𝑅 |
6 | 5 | nfel1 2185 |
. . . . . 6
⊢
Ⅎx⦋A / x⦌𝑅 ∈
V |
7 | | ovmpt2s.3 |
. . . . . . . . 9
⊢ 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) |
8 | | nfmpt21 5513 |
. . . . . . . . 9
⊢
Ⅎx(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) |
9 | 7, 8 | nfcxfr 2172 |
. . . . . . . 8
⊢
Ⅎx𝐹 |
10 | | nfcv 2175 |
. . . . . . . 8
⊢
Ⅎxy |
11 | 2, 9, 10 | nfov 5478 |
. . . . . . 7
⊢
Ⅎx(A𝐹y) |
12 | 11, 5 | nfeq 2182 |
. . . . . 6
⊢
Ⅎx(A𝐹y) =
⦋A / x⦌𝑅 |
13 | 6, 12 | nfim 1461 |
. . . . 5
⊢
Ⅎx(⦋A / x⦌𝑅 ∈ V
→ (A𝐹y) =
⦋A / x⦌𝑅) |
14 | | nfcsb1v 2876 |
. . . . . . 7
⊢
Ⅎy⦋B / y⦌⦋A / x⦌𝑅 |
15 | 14 | nfel1 2185 |
. . . . . 6
⊢
Ⅎy⦋B / y⦌⦋A / x⦌𝑅 ∈
V |
16 | | nfmpt22 5514 |
. . . . . . . . 9
⊢
Ⅎy(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) |
17 | 7, 16 | nfcxfr 2172 |
. . . . . . . 8
⊢
Ⅎy𝐹 |
18 | 3, 17, 4 | nfov 5478 |
. . . . . . 7
⊢
Ⅎy(A𝐹B) |
19 | 18, 14 | nfeq 2182 |
. . . . . 6
⊢
Ⅎy(A𝐹B) =
⦋B / y⦌⦋A / x⦌𝑅 |
20 | 15, 19 | nfim 1461 |
. . . . 5
⊢
Ⅎy(⦋B / y⦌⦋A / x⦌𝑅 ∈ V
→ (A𝐹B) =
⦋B / y⦌⦋A / x⦌𝑅) |
21 | | csbeq1a 2854 |
. . . . . . 7
⊢ (x = A →
𝑅 = ⦋A / x⦌𝑅) |
22 | 21 | eleq1d 2103 |
. . . . . 6
⊢ (x = A →
(𝑅 ∈ V ↔ ⦋A / x⦌𝑅 ∈
V)) |
23 | | oveq1 5462 |
. . . . . . 7
⊢ (x = A →
(x𝐹y) =
(A𝐹y)) |
24 | 23, 21 | eqeq12d 2051 |
. . . . . 6
⊢ (x = A →
((x𝐹y) =
𝑅 ↔ (A𝐹y) =
⦋A / x⦌𝑅)) |
25 | 22, 24 | imbi12d 223 |
. . . . 5
⊢ (x = A →
((𝑅 ∈ V → (x𝐹y) =
𝑅) ↔
(⦋A / x⦌𝑅 ∈ V
→ (A𝐹y) =
⦋A / x⦌𝑅))) |
26 | | csbeq1a 2854 |
. . . . . . 7
⊢ (y = B →
⦋A / x⦌𝑅 = ⦋B / y⦌⦋A / x⦌𝑅) |
27 | 26 | eleq1d 2103 |
. . . . . 6
⊢ (y = B →
(⦋A / x⦌𝑅 ∈ V
↔ ⦋B / y⦌⦋A / x⦌𝑅 ∈
V)) |
28 | | oveq2 5463 |
. . . . . . 7
⊢ (y = B →
(A𝐹y) =
(A𝐹B)) |
29 | 28, 26 | eqeq12d 2051 |
. . . . . 6
⊢ (y = B →
((A𝐹y) =
⦋A / x⦌𝑅 ↔ (A𝐹B) =
⦋B / y⦌⦋A / x⦌𝑅)) |
30 | 27, 29 | imbi12d 223 |
. . . . 5
⊢ (y = B →
((⦋A / x⦌𝑅 ∈ V
→ (A𝐹y) =
⦋A / x⦌𝑅) ↔ (⦋B / y⦌⦋A / x⦌𝑅 ∈ V
→ (A𝐹B) =
⦋B / y⦌⦋A / x⦌𝑅))) |
31 | 7 | ovmpt4g 5565 |
. . . . . 6
⊢
((x ∈ 𝐶 ∧ y ∈ 𝐷 ∧ 𝑅 ∈ V)
→ (x𝐹y) =
𝑅) |
32 | 31 | 3expia 1105 |
. . . . 5
⊢
((x ∈ 𝐶 ∧ y ∈ 𝐷) → (𝑅 ∈ V
→ (x𝐹y) =
𝑅)) |
33 | 2, 3, 4, 13, 20, 25, 30, 32 | vtocl2gaf 2614 |
. . . 4
⊢
((A ∈ 𝐶 ∧ B ∈ 𝐷) →
(⦋B / y⦌⦋A / x⦌𝑅 ∈ V
→ (A𝐹B) =
⦋B / y⦌⦋A / x⦌𝑅)) |
34 | | csbcomg 2867 |
. . . . 5
⊢
((A ∈ 𝐶 ∧ B ∈ 𝐷) → ⦋A / x⦌⦋B / y⦌𝑅 = ⦋B / y⦌⦋A / x⦌𝑅) |
35 | 34 | eleq1d 2103 |
. . . 4
⊢
((A ∈ 𝐶 ∧ B ∈ 𝐷) →
(⦋A / x⦌⦋B / y⦌𝑅 ∈ V
↔ ⦋B / y⦌⦋A / x⦌𝑅 ∈
V)) |
36 | 34 | eqeq2d 2048 |
. . . 4
⊢
((A ∈ 𝐶 ∧ B ∈ 𝐷) → ((A𝐹B) =
⦋A / x⦌⦋B / y⦌𝑅 ↔ (A𝐹B) =
⦋B / y⦌⦋A / x⦌𝑅)) |
37 | 33, 35, 36 | 3imtr4d 192 |
. . 3
⊢
((A ∈ 𝐶 ∧ B ∈ 𝐷) →
(⦋A / x⦌⦋B / y⦌𝑅 ∈ V
→ (A𝐹B) =
⦋A / x⦌⦋B / y⦌𝑅)) |
38 | 1, 37 | syl5 28 |
. 2
⊢
((A ∈ 𝐶 ∧ B ∈ 𝐷) →
(⦋A / x⦌⦋B / y⦌𝑅 ∈ 𝑉 → (A𝐹B) =
⦋A / x⦌⦋B / y⦌𝑅)) |
39 | 38 | 3impia 1100 |
1
⊢
((A ∈ 𝐶 ∧ B ∈ 𝐷 ∧ ⦋A / x⦌⦋B / y⦌𝑅 ∈ 𝑉) → (A𝐹B) =
⦋A / x⦌⦋B / y⦌𝑅) |