Step | Hyp | Ref
| Expression |

1 | | cdenom 15850 |
. 2
class
denom |

2 | | vy |
. . 3
setvar 𝑦 |

3 | | cq 12099 |
. . 3
class
ℚ |

4 | | vx |
. . . . . . . . . 10
setvar 𝑥 |

5 | 4 | cv 1600 |
. . . . . . . . 9
class 𝑥 |

6 | | c1st 7445 |
. . . . . . . . 9
class
1^{st} |

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

8 | | c2nd 7446 |
. . . . . . . . 9
class
2^{nd} |

9 | 5, 8 | cfv 6137 |
. . . . . . . 8
class
(2^{nd} ‘𝑥) |

10 | | cgcd 15626 |
. . . . . . . 8
class
gcd |

11 | 7, 9, 10 | co 6924 |
. . . . . . 7
class
((1^{st} ‘𝑥) gcd (2^{nd} ‘𝑥)) |

12 | | c1 10275 |
. . . . . . 7
class
1 |

13 | 11, 12 | wceq 1601 |
. . . . . 6
wff
((1^{st} ‘𝑥) gcd (2^{nd} ‘𝑥)) = 1 |

14 | 2 | cv 1600 |
. . . . . . 7
class 𝑦 |

15 | | cdiv 11034 |
. . . . . . . 8
class
/ |

16 | 7, 9, 15 | co 6924 |
. . . . . . 7
class
((1^{st} ‘𝑥) / (2^{nd} ‘𝑥)) |

17 | 14, 16 | wceq 1601 |
. . . . . 6
wff 𝑦 = ((1^{st} ‘𝑥) / (2^{nd} ‘𝑥)) |

18 | 13, 17 | wa 386 |
. . . . 5
wff
(((1^{st} ‘𝑥) gcd (2^{nd} ‘𝑥)) = 1 ∧ 𝑦 = ((1^{st} ‘𝑥) / (2^{nd} ‘𝑥))) |

19 | | cz 11732 |
. . . . . 6
class
ℤ |

20 | | cn 11378 |
. . . . . 6
class
ℕ |

21 | 19, 20 | cxp 5355 |
. . . . 5
class (ℤ
× ℕ) |

22 | 18, 4, 21 | crio 6884 |
. . . 4
class
(__℩__𝑥
∈ (ℤ × ℕ)(((1^{st} ‘𝑥) gcd (2^{nd} ‘𝑥)) = 1 ∧ 𝑦 = ((1^{st} ‘𝑥) / (2^{nd} ‘𝑥)))) |

23 | 22, 8 | cfv 6137 |
. . 3
class
(2^{nd} ‘(__℩__𝑥 ∈ (ℤ ×
ℕ)(((1^{st} ‘𝑥) gcd (2^{nd} ‘𝑥)) = 1 ∧ 𝑦 = ((1^{st} ‘𝑥) / (2^{nd} ‘𝑥))))) |

24 | 2, 3, 23 | cmpt 4967 |
. 2
class (𝑦 ∈ ℚ ↦
(2^{nd} ‘(__℩__𝑥 ∈ (ℤ ×
ℕ)(((1^{st} ‘𝑥) gcd (2^{nd} ‘𝑥)) = 1 ∧ 𝑦 = ((1^{st} ‘𝑥) / (2^{nd} ‘𝑥)))))) |

25 | 1, 24 | wceq 1601 |
1
wff denom =
(𝑦 ∈ ℚ ↦
(2^{nd} ‘(__℩__𝑥 ∈ (ℤ ×
ℕ)(((1^{st} ‘𝑥) gcd (2^{nd} ‘𝑥)) = 1 ∧ 𝑦 = ((1^{st} ‘𝑥) / (2^{nd} ‘𝑥)))))) |