Step | Hyp | Ref
| Expression |
1 | | fmpoco.1 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) |
2 | 1 | ralrimivva 3123 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑅 ∈ 𝐶) |
3 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) |
4 | 3 | fmpo 7908 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑅 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) |
5 | 2, 4 | sylib 217 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) |
6 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑢𝑅 |
7 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑣𝑅 |
8 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑣 |
9 | | nfcsb1v 3857 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝑅 |
10 | 8, 9 | nfcsbw 3859 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 |
11 | | nfcsb1v 3857 |
. . . . . . 7
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 |
12 | | csbeq1a 3846 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → 𝑅 = ⦋𝑢 / 𝑥⦌𝑅) |
13 | | csbeq1a 3846 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → ⦋𝑢 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
14 | 12, 13 | sylan9eq 2798 |
. . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
15 | 6, 7, 10, 11, 14 | cbvmpo 7369 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
16 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
17 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑣 ∈ V |
18 | 16, 17 | op2ndd 7842 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (2nd ‘𝑤) = 𝑣) |
19 | 18 | csbeq1d 3836 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) |
20 | 16, 17 | op1std 7841 |
. . . . . . . . . 10
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (1st ‘𝑤) = 𝑢) |
21 | 20 | csbeq1d 3836 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑢 / 𝑥⦌𝑅) |
22 | 21 | csbeq2dv 3839 |
. . . . . . . 8
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋𝑣 / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
23 | 19, 22 | eqtrd 2778 |
. . . . . . 7
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
24 | 23 | mpompt 7388 |
. . . . . 6
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) |
25 | 15, 24 | eqtr4i 2769 |
. . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) |
26 | 25 | fmpt 6984 |
. . . 4
⊢
(∀𝑤 ∈
(𝐴 × 𝐵)⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) |
27 | 5, 26 | sylibr 233 |
. . 3
⊢ (𝜑 → ∀𝑤 ∈ (𝐴 × 𝐵)⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 ∈ 𝐶) |
28 | | fmpoco.2 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) |
29 | 28, 25 | eqtrdi 2794 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅)) |
30 | | fmpoco.3 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) |
31 | 27, 29, 30 | fmptcos 7003 |
. 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆)) |
32 | 23 | csbeq1d 3836 |
. . . . 5
⊢ (𝑤 = 〈𝑢, 𝑣〉 →
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆 = ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) |
33 | 32 | mpompt 7388 |
. . . 4
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) |
34 | | nfcv 2907 |
. . . . 5
⊢
Ⅎ𝑢⦋𝑅 / 𝑧⦌𝑆 |
35 | | nfcv 2907 |
. . . . 5
⊢
Ⅎ𝑣⦋𝑅 / 𝑧⦌𝑆 |
36 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑥𝑆 |
37 | 10, 36 | nfcsbw 3859 |
. . . . 5
⊢
Ⅎ𝑥⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆 |
38 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑦𝑆 |
39 | 11, 38 | nfcsbw 3859 |
. . . . 5
⊢
Ⅎ𝑦⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆 |
40 | 14 | csbeq1d 3836 |
. . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ⦋𝑅 / 𝑧⦌𝑆 = ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) |
41 | 34, 35, 37, 39, 40 | cbvmpo 7369 |
. . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) |
42 | 33, 41 | eqtr4i 2769 |
. . 3
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) |
43 | 1 | 3impb 1114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑅 ∈ 𝐶) |
44 | | nfcvd 2908 |
. . . . . 6
⊢ (𝑅 ∈ 𝐶 → Ⅎ𝑧𝑇) |
45 | | fmpoco.4 |
. . . . . 6
⊢ (𝑧 = 𝑅 → 𝑆 = 𝑇) |
46 | 44, 45 | csbiegf 3866 |
. . . . 5
⊢ (𝑅 ∈ 𝐶 → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) |
47 | 43, 46 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) |
48 | 47 | mpoeq3dva 7352 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) |
49 | 42, 48 | eqtrid 2790 |
. 2
⊢ (𝜑 → (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) |
50 | 31, 49 | eqtrd 2778 |
1
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) |