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 ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝑔 ) 𝑒 ) = 𝑥 ) ) ) ∈ V
2 df-0g 0g = ( 𝑔 ∈ V ↦ ( ℩ 𝑒 ( 𝑒 ∈ ( Base ‘ 𝑔 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑔 ) ( ( 𝑒 ( +g𝑔 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g𝑔 ) 𝑒 ) = 𝑥 ) ) ) )
3 1 2 fnmpti 0g Fn V