This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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