Theorem fden

Description: Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014)

	Ref	Expression
Assertion	fden	|- denom : QQ --> NN

Proof

Step	Hyp	Ref	Expression
1		df-denom	|- denom = ( a e. QQ |-> ( 2nd ` ( iota_ b e. ( ZZ X. NN ) ( ( ( 1st ` b ) gcd ( 2nd ` b ) ) = 1 /\ a = ( ( 1st ` b ) / ( 2nd ` b ) ) ) ) ) )
2		qdenval	|- ( a e. QQ -> ( denom ` a ) = ( 2nd ` ( iota_ b e. ( ZZ X. NN ) ( ( ( 1st ` b ) gcd ( 2nd ` b ) ) = 1 /\ a = ( ( 1st ` b ) / ( 2nd ` b ) ) ) ) ) )
3		qdencl	|- ( a e. QQ -> ( denom ` a ) e. NN )
4	2 3	eqeltrrd	|- ( a e. QQ -> ( 2nd ` ( iota_ b e. ( ZZ X. NN ) ( ( ( 1st ` b ) gcd ( 2nd ` b ) ) = 1 /\ a = ( ( 1st ` b ) / ( 2nd ` b ) ) ) ) ) e. NN )
5	1 4	fmpti	|- denom : QQ --> NN