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 ⊢ 0 𝑔 Fn V

Proof

Step Hyp Ref Expression
1 iotaex ⊢ ι e | e ∈ Base g ∧ ∀ x ∈ Base g e + g x = x ∧ x + g e = x ∈ V
2 df-0g ⊢ 0 𝑔 = g ∈ V ⟼ ι e | e ∈ Base g ∧ ∀ x ∈ Base g e + g x = x ∧ x + g e = x
3 1 2 fnmpti ⊢ 0 𝑔 Fn V