Step | Hyp | Ref
| Expression |

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

2 | | vx |
. . 3
setvar *x* |

3 | | vy |
. . 3
setvar *y* |

4 | | cnpi 6256 |
. . . 4
class
**N** |

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

6 | 2 | cv 1241 |
. . . . . 6
class *x* |

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

8 | 6, 7 | cfv 4845 |
. . . . 5
class (1^{st}
‘*x*) |

9 | 3 | cv 1241 |
. . . . . 6
class *y* |

10 | 9, 7 | cfv 4845 |
. . . . 5
class (1^{st}
‘*y*) |

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

12 | 8, 10, 11 | co 5455 |
. . . 4
class ((1^{st}
‘*x*)
·_{N} (1^{st} ‘*y*)) |

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

14 | 6, 13 | cfv 4845 |
. . . . 5
class (2^{nd}
‘*x*) |

15 | 9, 13 | cfv 4845 |
. . . . 5
class (2^{nd}
‘*y*) |

16 | 14, 15, 11 | co 5455 |
. . . 4
class ((2^{nd}
‘*x*)
·_{N} (2^{nd} ‘*y*)) |

17 | 12, 16 | cop 3370 |
. . 3
class ⟨((1^{st}
‘*x*)
·_{N} (1^{st} ‘*y*)), ((2^{nd} ‘*x*) ·_{N}
(2^{nd} ‘*y*))⟩ |

18 | 2, 3, 5, 5, 17 | cmpt2 5457 |
. 2
class (*x* ∈
(**N** × **N**), *y* ∈
(**N** × **N**) ↦ ⟨((1^{st}
‘*x*)
·_{N} (1^{st} ‘*y*)), ((2^{nd} ‘*x*) ·_{N}
(2^{nd} ‘*y*))⟩) |

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