Theorem dgraaf

Description: Degree function on algebraic numbers is a function. (Contributed by Stefan O'Rear, 25-Nov-2014) (Proof shortened by AV, 29-Sep-2020)

	Ref	Expression
Assertion	dgraaf	|- degAA : AA --> NN

Proof

Step	Hyp	Ref	Expression
1		ltso	|- < Or RR
2	1	infex	|- inf ( { b e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = b /\ ( p ` a ) = 0 ) } , RR , < ) e. _V
3		df-dgraa	|- degAA = ( a e. AA |-> inf ( { b e. NN | E. p e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` p ) = b /\ ( p ` a ) = 0 ) } , RR , < ) )
4	2 3	fnmpti	|- degAA Fn AA
5		dgraacl	|- ( a e. AA -> ( degAA ` a ) e. NN )
6	5	rgen	|- A. a e. AA ( degAA ` a ) e. NN
7		ffnfv	|- ( degAA : AA --> NN <-> ( degAA Fn AA /\ A. a e. AA ( degAA ` a ) e. NN ) )
8	4 6 7	mpbir2an	|- degAA : AA --> NN