Metamath Proof Explorer


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