Step | Hyp | Ref
| Expression |
1 | | fmpoco.1 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) |
2 | 1 | ralrimivva 3194 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑅 ∈ 𝐶) |
3 | | eqid 2726 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) |
4 | 3 | fmpo 8050 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑅 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) |
5 | 2, 4 | sylib 217 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) |
6 | | nfcv 2897 |
. . . . . . 7
⊢
Ⅎ𝑢𝑅 |
7 | | nfcv 2897 |
. . . . . . 7
⊢
Ⅎ𝑣𝑅 |
8 | | nfcv 2897 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑣 |
9 | | nfcsb1v 3913 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝑅 |
10 | 8, 9 | nfcsbw 3915 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 |
11 | | nfcsb1v 3913 |
. . . . . . 7
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 |
12 | | csbeq1a 3902 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → 𝑅 = ⦋𝑢 / 𝑥⦌𝑅) |
13 | | csbeq1a 3902 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → ⦋𝑢 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
14 | 12, 13 | sylan9eq 2786 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
15 | 6, 7, 10, 11, 14 | cbvmpo 7498 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
16 | | vex 3472 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
17 | | vex 3472 |
. . . . . . . . . 10
⊢ 𝑣 ∈ V |
18 | 16, 17 | op2ndd 7982 |
. . . . . . . . 9
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → (2nd ‘𝑤) = 𝑣) |
19 | 18 | csbeq1d 3892 |
. . . . . . . 8
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) |
20 | 16, 17 | op1std 7981 |
. . . . . . . . . 10
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → (1st ‘𝑤) = 𝑢) |
21 | 20 | csbeq1d 3892 |
. . . . . . . . 9
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → ⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑢 / 𝑥⦌𝑅) |
22 | 21 | csbeq2dv 3895 |
. . . . . . . 8
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → ⦋𝑣 / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
23 | 19, 22 | eqtrd 2766 |
. . . . . . 7
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
24 | 23 | mpompt 7517 |
. . . . . 6
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
25 | 15, 24 | eqtr4i 2757 |
. . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) |
26 | 25 | fmpt 7104 |
. . . 4
⊢
(∀𝑤 ∈
(𝐴 × 𝐵)⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) |
27 | 5, 26 | sylibr 233 |
. . 3
⊢ (𝜑 → ∀𝑤 ∈ (𝐴 × 𝐵)⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 ∈ 𝐶) |
28 | | fmpoco.2 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) |
29 | 28, 25 | eqtrdi 2782 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅)) |
30 | | fmpoco.3 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) |
31 | 27, 29, 30 | fmptcos 7124 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆)) |
32 | 23 | csbeq1d 3892 |
. . . . 5
⊢ (𝑤 = ⟨𝑢, 𝑣⟩ →
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆 = ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) |
33 | 32 | mpompt 7517 |
. . . 4
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) |
34 | | nfcv 2897 |
. . . . 5
⊢
Ⅎ𝑢⦋𝑅 / 𝑧⦌𝑆 |
35 | | nfcv 2897 |
. . . . 5
⊢
Ⅎ𝑣⦋𝑅 / 𝑧⦌𝑆 |
36 | | nfcv 2897 |
. . . . . 6
⊢
Ⅎ𝑥𝑆 |
37 | 10, 36 | nfcsbw 3915 |
. . . . 5
⊢
Ⅎ𝑥⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆 |
38 | | nfcv 2897 |
. . . . . 6
⊢
Ⅎ𝑦𝑆 |
39 | 11, 38 | nfcsbw 3915 |
. . . . 5
⊢
Ⅎ𝑦⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆 |
40 | 14 | csbeq1d 3892 |
. . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ⦋𝑅 / 𝑧⦌𝑆 = ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) |
41 | 34, 35, 37, 39, 40 | cbvmpo 7498 |
. . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) |
42 | 33, 41 | eqtr4i 2757 |
. . 3
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) |
43 | 1 | 3impb 1112 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑅 ∈ 𝐶) |
44 | | nfcvd 2898 |
. . . . . 6
⊢ (𝑅 ∈ 𝐶 → Ⅎ𝑧𝑇) |
45 | | fmpoco.4 |
. . . . . 6
⊢ (𝑧 = 𝑅 → 𝑆 = 𝑇) |
46 | 44, 45 | csbiegf 3922 |
. . . . 5
⊢ (𝑅 ∈ 𝐶 → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) |
47 | 43, 46 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) |
48 | 47 | mpoeq3dva 7481 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) |
49 | 42, 48 | eqtrid 2778 |
. 2
⊢ (𝜑 → (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) |
50 | 31, 49 | eqtrd 2766 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) |