Step | Hyp | Ref
| Expression |

1 | | cltpq 9529 |
. 2
class
<_{pQ} |

2 | | vx |
. . . . . . 7
setvar 𝑥 |

3 | 2 | cv 1474 |
. . . . . 6
class 𝑥 |

4 | | cnpi 9523 |
. . . . . . 7
class
**N** |

5 | 4, 4 | cxp 5026 |
. . . . . 6
class
(**N** × **N**) |

6 | 3, 5 | wcel 1977 |
. . . . 5
wff 𝑥 ∈ (**N** ×
**N**) |

7 | | vy |
. . . . . . 7
setvar 𝑦 |

8 | 7 | cv 1474 |
. . . . . 6
class 𝑦 |

9 | 8, 5 | wcel 1977 |
. . . . 5
wff 𝑦 ∈ (**N** ×
**N**) |

10 | 6, 9 | wa 383 |
. . . 4
wff (𝑥 ∈ (**N** ×
**N**) ∧ 𝑦
∈ (**N** × **N**)) |

11 | | c1st 7035 |
. . . . . . 7
class
1^{st} |

12 | 3, 11 | cfv 5790 |
. . . . . 6
class
(1^{st} ‘𝑥) |

13 | | c2nd 7036 |
. . . . . . 7
class
2^{nd} |

14 | 8, 13 | cfv 5790 |
. . . . . 6
class
(2^{nd} ‘𝑦) |

15 | | cmi 9525 |
. . . . . 6
class
·_{N} |

16 | 12, 14, 15 | co 6527 |
. . . . 5
class
((1^{st} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦)) |

17 | 8, 11 | cfv 5790 |
. . . . . 6
class
(1^{st} ‘𝑦) |

18 | 3, 13 | cfv 5790 |
. . . . . 6
class
(2^{nd} ‘𝑥) |

19 | 17, 18, 15 | co 6527 |
. . . . 5
class
((1^{st} ‘𝑦) ·_{N}
(2^{nd} ‘𝑥)) |

20 | | clti 9526 |
. . . . 5
class
<_{N} |

21 | 16, 19, 20 | wbr 4578 |
. . . 4
wff
((1^{st} ‘𝑥) ·_{N}
(2^{nd} ‘𝑦))
<_{N} ((1^{st} ‘𝑦) ·_{N}
(2^{nd} ‘𝑥)) |

22 | 10, 21 | wa 383 |
. . 3
wff ((𝑥 ∈ (**N** ×
**N**) ∧ 𝑦
∈ (**N** × **N**)) ∧ ((1^{st}
‘𝑥)
·_{N} (2^{nd} ‘𝑦)) <_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥))) |

23 | 22, 2, 7 | copab 4637 |
. 2
class
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (**N** ×
**N**) ∧ 𝑦
∈ (**N** × **N**)) ∧ ((1^{st}
‘𝑥)
·_{N} (2^{nd} ‘𝑦)) <_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥)))} |

24 | 1, 23 | wceq 1475 |
1
wff
<_{pQ} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (**N** ×
**N**) ∧ 𝑦
∈ (**N** × **N**)) ∧ ((1^{st}
‘𝑥)
·_{N} (2^{nd} ‘𝑦)) <_{N}
((1^{st} ‘𝑦)
·_{N} (2^{nd} ‘𝑥)))} |