| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fmpocos.1 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ 𝐶) | 
| 2 | 1 | ralrimivva 3201 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑅 ∈ 𝐶) | 
| 3 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) | 
| 4 | 3 | fmpo 8094 | . . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝑅 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) | 
| 5 | 2, 4 | sylib 218 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) | 
| 6 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑢𝑅 | 
| 7 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑣𝑅 | 
| 8 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑥𝑣 | 
| 9 |  | nfcsb1v 3922 | . . . . . . . 8
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝑅 | 
| 10 | 8, 9 | nfcsbw 3924 | . . . . . . 7
⊢
Ⅎ𝑥⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 | 
| 11 |  | nfcsb1v 3922 | . . . . . . 7
⊢
Ⅎ𝑦⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 | 
| 12 |  | csbeq1a 3912 | . . . . . . . 8
⊢ (𝑥 = 𝑢 → 𝑅 = ⦋𝑢 / 𝑥⦌𝑅) | 
| 13 |  | csbeq1a 3912 | . . . . . . . 8
⊢ (𝑦 = 𝑣 → ⦋𝑢 / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 14 | 12, 13 | sylan9eq 2796 | . . . . . . 7
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 15 | 6, 7, 10, 11, 14 | cbvmpo 7528 | . . . . . 6
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 16 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑢 ∈ V | 
| 17 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑣 ∈ V | 
| 18 | 16, 17 | op2ndd 8026 | . . . . . . . 8
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (2nd ‘𝑤) = 𝑣) | 
| 19 | 16, 17 | op1std 8025 | . . . . . . . . 9
⊢ (𝑤 = 〈𝑢, 𝑣〉 → (1st ‘𝑤) = 𝑢) | 
| 20 | 19 | csbeq1d 3902 | . . . . . . . 8
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑢 / 𝑥⦌𝑅) | 
| 21 | 18, 20 | csbeq12dv 3907 | . . . . . . 7
⊢ (𝑤 = 〈𝑢, 𝑣〉 → ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 = ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 22 | 21 | mpompt 7548 | . . . . . 6
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅) | 
| 23 | 15, 22 | eqtr4i 2767 | . . . . 5
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅) = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅) | 
| 24 | 23 | fmpt 7129 | . . . 4
⊢
(∀𝑤 ∈
(𝐴 × 𝐵)⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅):(𝐴 × 𝐵)⟶𝐶) | 
| 25 | 5, 24 | sylibr 234 | . . 3
⊢ (𝜑 → ∀𝑤 ∈ (𝐴 × 𝐵)⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 ∈ 𝐶) | 
| 26 |  | fmpocos.2 | . . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑅)) | 
| 27 | 26, 23 | eqtrdi 2792 | . . 3
⊢ (𝜑 → 𝐹 = (𝑤 ∈ (𝐴 × 𝐵) ↦ ⦋(2nd
‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅)) | 
| 28 |  | fmpocos.3 | . . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ 𝐶 ↦ 𝑆)) | 
| 29 | 25, 27, 28 | fmptcos 7150 | . 2
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆)) | 
| 30 | 21 | csbeq1d 3902 | . . . . 5
⊢ (𝑤 = 〈𝑢, 𝑣〉 →
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆 = ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) | 
| 31 | 30 | mpompt 7548 | . . . 4
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) | 
| 32 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑢⦋𝑅 / 𝑧⦌𝑆 | 
| 33 |  | nfcv 2904 | . . . . 5
⊢
Ⅎ𝑣⦋𝑅 / 𝑧⦌𝑆 | 
| 34 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑥𝑆 | 
| 35 | 10, 34 | nfcsbw 3924 | . . . . 5
⊢
Ⅎ𝑥⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆 | 
| 36 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑦𝑆 | 
| 37 | 11, 36 | nfcsbw 3924 | . . . . 5
⊢
Ⅎ𝑦⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆 | 
| 38 | 14 | csbeq1d 3902 | . . . . 5
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ⦋𝑅 / 𝑧⦌𝑆 = ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) | 
| 39 | 32, 33, 35, 37, 38 | cbvmpo 7528 | . . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) = (𝑢 ∈ 𝐴, 𝑣 ∈ 𝐵 ↦ ⦋⦋𝑣 / 𝑦⦌⦋𝑢 / 𝑥⦌𝑅 / 𝑧⦌𝑆) | 
| 40 | 31, 39 | eqtr4i 2767 | . . 3
⊢ (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) | 
| 41 |  | fmpocos.4 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) | 
| 42 | 41 | 3impb 1114 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⦋𝑅 / 𝑧⦌𝑆 = 𝑇) | 
| 43 | 42 | mpoeq3dva 7511 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ⦋𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | 
| 44 | 40, 43 | eqtrid 2788 | . 2
⊢ (𝜑 → (𝑤 ∈ (𝐴 × 𝐵) ↦
⦋⦋(2nd ‘𝑤) / 𝑦⦌⦋(1st
‘𝑤) / 𝑥⦌𝑅 / 𝑧⦌𝑆) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) | 
| 45 | 29, 44 | eqtrd 2776 | 1
⊢ (𝜑 → (𝐺 ∘ 𝐹) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝑇)) |