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

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