Metamath Proof Explorer

Theorem fn0g

Description: The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015)

Ref Expression
Assertion fn0g 
|- 0g Fn _V

Proof

Step Hyp Ref Expression
1 iotaex 
 |-  ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) e. _V
2 df-0g 
 |-  0g = ( g e. _V |-> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) )
3 1 2 fnmpti 
 |-  0g Fn _V