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 ⊢ X = Base G
odcl.2 ⊢ O = od ⁡ G
Assertion odf ⊢ O : X ⟶ ℕ 0

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ X = Base G
2 odcl.2 ⊢ O = od ⁡ G
3 c0ex ⊢ 0 ∈ V
4 ltso ⊢ < Or ℝ
5 4 infex ⊢ inf w ℝ < ∈ V
6 3 5 ifex ⊢ if w = ∅ 0 inf w ℝ < ∈ V
7 6 csbex ⊢ ⦋ z ∈ ℕ | z ⋅ G y = 0 G / w⦌ if w = ∅ 0 inf w ℝ < ∈ V
8 eqid ⊢ ⋅ G = ⋅ G
9 eqid ⊢ 0 G = 0 G
10 1 8 9 2 odfval ⊢ O = y ∈ X ⟼ ⦋ z ∈ ℕ | z ⋅ G y = 0 G / w⦌ if w = ∅ 0 inf w ℝ <
11 7 10 fnmpti ⊢ O Fn X
12 1 2 odcl ⊢ x ∈ X → O ⁡ x ∈ ℕ 0
13 12 rgen ⊢ ∀ x ∈ X O ⁡ x ∈ ℕ 0
14 ffnfv ⊢ O : X ⟶ ℕ 0 ↔ O Fn X ∧ ∀ x ∈ X O ⁡ x ∈ ℕ 0
15 11 13 14 mpbir2an ⊢ O : X ⟶ ℕ 0