Step | Hyp | Ref
| Expression |

1 | | cmpq 6986 |
. 2
class
·_{pQ} |

2 | | vx |
. . 3
setvar 𝑥 |

3 | | vy |
. . 3
setvar 𝑦 |

4 | | cnpi 6981 |
. . . 4
class
**N** |

5 | 4, 4 | cxp 4475 |
. . 3
class
(**N** × **N**) |

6 | 2 | cv 1298 |
. . . . . 6
class 𝑥 |

7 | | c1st 5967 |
. . . . . 6
class
1^{st} |

8 | 6, 7 | cfv 5059 |
. . . . 5
class
(1^{st} ‘𝑥) |

9 | 3 | cv 1298 |
. . . . . 6
class 𝑦 |

10 | 9, 7 | cfv 5059 |
. . . . 5
class
(1^{st} ‘𝑦) |

11 | | cmi 6983 |
. . . . 5
class
·_{N} |

12 | 8, 10, 11 | co 5706 |
. . . 4
class
((1^{st} ‘𝑥) ·_{N}
(1^{st} ‘𝑦)) |

13 | | c2nd 5968 |
. . . . . 6
class
2^{nd} |

14 | 6, 13 | cfv 5059 |
. . . . 5
class
(2^{nd} ‘𝑥) |

15 | 9, 13 | cfv 5059 |
. . . . 5
class
(2^{nd} ‘𝑦) |

16 | 14, 15, 11 | co 5706 |
. . . 4
class
((2^{nd} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦)) |

17 | 12, 16 | cop 3477 |
. . 3
class
⟨((1^{st} ‘𝑥) ·_{N}
(1^{st} ‘𝑦)),
((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩ |

18 | 2, 3, 5, 5, 17 | cmpo 5708 |
. 2
class (𝑥 ∈ (**N** ×
**N**), 𝑦 ∈
(**N** × **N**) ↦ ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |

19 | 1, 18 | wceq 1299 |
1
wff
·_{pQ} = (𝑥 ∈ (**N** ×
**N**), 𝑦 ∈
(**N** × **N**) ↦ ⟨((1^{st}
‘𝑥)
·_{N} (1^{st} ‘𝑦)), ((2^{nd} ‘𝑥)
·_{N} (2^{nd} ‘𝑦))⟩) |