Theorem fn0g

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

	Ref	Expression
Assertion	fn0g	$$⊢0_{𝑔}Fn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		iotaex	$$⊢\left(\iota e|\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\right)\in \mathrm{V}$$
2		df-0g	$$⊢0_{𝑔}=\left(g\in \mathrm{V}⟼\left(\iota e|\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\right)\right)$$
3	1 2	fnmpti	$$⊢0_{𝑔}Fn\mathrm{V}$$