Theorem odf

Description: Functionality of the group element order. (Contributed by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 5-Oct-2020)

	Ref	Expression
Hypotheses	odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion	odf	⊢ 𝑂 : 𝑋 ⟶ ℕ0

Proof

Step	Hyp	Ref	Expression
1		odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		c0ex	⊢ 0 ∈ V
4		ltso	⊢ < Or ℝ
5	4	infex	⊢ inf ( 𝑤 , ℝ , < ) ∈ V
6	3 5	ifex	⊢ if ( 𝑤 = ∅ , 0 , inf ( 𝑤 , ℝ , < ) ) ∈ V
7	6	csbex	⊢ ⦋ { 𝑧 ∈ ℕ ∣ ( 𝑧 ( .g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) } / 𝑤 ⦌ if ( 𝑤 = ∅ , 0 , inf ( 𝑤 , ℝ , < ) ) ∈ V
8		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
9		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
10	1 8 9 2	odfval	⊢ 𝑂 = ( 𝑦 ∈ 𝑋 ↦ ⦋ { 𝑧 ∈ ℕ ∣ ( 𝑧 ( .g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) } / 𝑤 ⦌ if ( 𝑤 = ∅ , 0 , inf ( 𝑤 , ℝ , < ) ) )
11	7 10	fnmpti	⊢ 𝑂 Fn 𝑋
12	1 2	odcl	⊢ ( 𝑥 ∈ 𝑋 → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
13	12	rgen	⊢ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ℕ0
14		ffnfv	⊢ ( 𝑂 : 𝑋 ⟶ ℕ0 ↔ ( 𝑂 Fn 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 ) )
15	11 13 14	mpbir2an	⊢ 𝑂 : 𝑋 ⟶ ℕ0