| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fmpoco.1 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) | 
| 2 | 1 | ralrimivva 3202 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑅 ∈ 𝐶) | 
| 3 |  | eqid 2737 | . . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) | 
| 4 | 3 | fmpo 8093 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑅 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) | 
| 5 | 2, 4 | sylib 218 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) | 
| 6 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑢𝑅 | 
| 7 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑣𝑅 | 
| 8 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑥𝑣 | 
| 9 |  | nfcsb1v 3923 | . . . . . . . 8
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝑅 | 
| 10 | 8, 9 | nfcsbw 3925 | . . . . . . 7
⊢
Ⅎ𝑥⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 | 
| 11 |  | nfcsb1v 3923 | . . . . . . 7
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 | 
| 12 |  | csbeq1a 3913 | . . . . . . . 8
⊢ (𝑥 = 𝑢 → 𝑅 = ⦋𝑢 / 𝑥⦌𝑅) | 
| 13 |  | csbeq1a 3913 | . . . . . . . 8
⊢ (𝑦 = 𝑣 → ⦋𝑢 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 14 | 12, 13 | sylan9eq 2797 | . . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 15 | 6, 7, 10, 11, 14 | cbvmpo 7527 | . . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 16 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑢 ∈ V | 
| 17 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑣 ∈ V | 
| 18 | 16, 17 | op2ndd 8025 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (2nd ‘𝑤) = 𝑣) | 
| 19 | 18 | csbeq1d 3903 | . . . . . . . 8
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) | 
| 20 | 16, 17 | op1std 8024 | . . . . . . . . . 10
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (1st ‘𝑤) = 𝑢) | 
| 21 | 20 | csbeq1d 3903 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑢 / 𝑥⦌𝑅) | 
| 22 | 21 | csbeq2dv 3906 | . . . . . . . 8
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋𝑣 / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 23 | 19, 22 | eqtrd 2777 | . . . . . . 7
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 24 | 23 | mpompt 7547 | . . . . . 6
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 25 | 15, 24 | eqtr4i 2768 | . . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) | 
| 26 | 25 | fmpt 7130 | . . . 4
⊢
(∀𝑤 ∈
(𝐴 × 𝐵)⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) | 
| 27 | 5, 26 | sylibr 234 | . . 3
⊢ (𝜑 → ∀𝑤 ∈ (𝐴 × 𝐵)⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 ∈ 𝐶) | 
| 28 |  | fmpoco.2 | . . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) | 
| 29 | 28, 25 | eqtrdi 2793 | . . 3
⊢ (𝜑 → 𝐹 = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅)) | 
| 30 |  | fmpoco.3 | . . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) | 
| 31 | 27, 29, 30 | fmptcos 7151 | . 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆)) | 
| 32 | 23 | csbeq1d 3903 | . . . . 5
⊢ (𝑤 = 〈𝑢, 𝑣〉 →
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆 = ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) | 
| 33 | 32 | mpompt 7547 | . . . 4
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) | 
| 34 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑢⦋𝑅 / 𝑧⦌𝑆 | 
| 35 |  | nfcv 2905 | . . . . 5
⊢
Ⅎ𝑣⦋𝑅 / 𝑧⦌𝑆 | 
| 36 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑥𝑆 | 
| 37 | 10, 36 | nfcsbw 3925 | . . . . 5
⊢
Ⅎ𝑥⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆 | 
| 38 |  | nfcv 2905 | . . . . . 6
⊢
Ⅎ𝑦𝑆 | 
| 39 | 11, 38 | nfcsbw 3925 | . . . . 5
⊢
Ⅎ𝑦⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆 | 
| 40 | 14 | csbeq1d 3903 | . . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ⦋𝑅 / 𝑧⦌𝑆 = ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) | 
| 41 | 34, 35, 37, 39, 40 | cbvmpo 7527 | . . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) | 
| 42 | 33, 41 | eqtr4i 2768 | . . 3
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) | 
| 43 | 1 | 3impb 1115 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑅 ∈ 𝐶) | 
| 44 |  | nfcvd 2906 | . . . . . 6
⊢ (𝑅 ∈ 𝐶 → Ⅎ𝑧𝑇) | 
| 45 |  | fmpoco.4 | . . . . . 6
⊢ (𝑧 = 𝑅 → 𝑆 = 𝑇) | 
| 46 | 44, 45 | csbiegf 3932 | . . . . 5
⊢ (𝑅 ∈ 𝐶 → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) | 
| 47 | 43, 46 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) | 
| 48 | 47 | mpoeq3dva 7510 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | 
| 49 | 42, 48 | eqtrid 2789 | . 2
⊢ (𝜑 → (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | 
| 50 | 31, 49 | eqtrd 2777 | 1
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) |