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 : 𝔸 ⟶ ℕ

Proof

Step	Hyp	Ref	Expression
1		ltso	⊢ < Or ℝ
2	1	infex	⊢ inf ( { 𝑏 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑏 ∧ ( 𝑝 ‘ 𝑎 ) = 0 ) } , ℝ , < ) ∈ V
3		df-dgraa	⊢ degAA = ( 𝑎 ∈ 𝔸 ↦ inf ( { 𝑏 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑏 ∧ ( 𝑝 ‘ 𝑎 ) = 0 ) } , ℝ , < ) )
4	2 3	fnmpti	⊢ degAA Fn 𝔸
5		dgraacl	⊢ ( 𝑎 ∈ 𝔸 → ( degAA ‘ 𝑎 ) ∈ ℕ )
6	5	rgen	⊢ ∀ 𝑎 ∈ 𝔸 ( degAA ‘ 𝑎 ) ∈ ℕ
7		ffnfv	⊢ ( degAA : 𝔸 ⟶ ℕ ↔ ( degAA Fn 𝔸 ∧ ∀ 𝑎 ∈ 𝔸 ( degAA ‘ 𝑎 ) ∈ ℕ ) )
8	4 6 7	mpbir2an	⊢ degAA : 𝔸 ⟶ ℕ