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 --> NN0

Proof

Step Hyp Ref Expression
1 odcl.1 
 |-  X = ( Base ` G )
2 odcl.2 
 |-  O = ( od ` G )
3 c0ex 
 |-  0 e. _V
4 ltso 
 |-  < Or RR
5 4 infex 
 |-  inf ( w , RR , < ) e. _V
6 3 5 ifex 
 |-  if ( w = (/) , 0 , inf ( w , RR , < ) ) e. _V
7 6 csbex 
 |-  [_ { z e. NN | ( z ( .g ` G ) y ) = ( 0g ` G ) } / w ]_ if ( w = (/) , 0 , inf ( w , RR , < ) ) e. _V
8 eqid 
 |-  ( .g ` G ) = ( .g ` G )
9 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
10 1 8 9 2 odfval 
 |-  O = ( y e. X |-> [_ { z e. NN | ( z ( .g ` G ) y ) = ( 0g ` G ) } / w ]_ if ( w = (/) , 0 , inf ( w , RR , < ) ) )
11 7 10 fnmpti 
 |-  O Fn X
12 1 2 odcl 
 |-  ( x e. X -> ( O ` x ) e. NN0 )
13 12 rgen 
 |-  A. x e. X ( O ` x ) e. NN0
14 ffnfv 
 |-  ( O : X --> NN0 <-> ( O Fn X /\ A. x e. X ( O ` x ) e. NN0 ) )
15 11 13 14 mpbir2an 
 |-  O : X --> NN0