Theorem efgmf

Description: The formal inverse operation is an endofunction on the generating set. (Contributed by Mario Carneiro, 27-Sep-2015)

	Ref	Expression
Hypothesis	efgmval.m	$$⊢M=\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)$$
Assertion	efgmf	$$⊢M:I\times 2_{𝑜}⟶I\times 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		efgmval.m	$$⊢M=\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)$$
2		2oconcl	$$⊢z\in 2_{𝑜}\to 1_{𝑜}\setminus z\in 2_{𝑜}$$
3		opelxpi	$$⊢\left(y\in I\wedge 1_{𝑜}\setminus z\in 2_{𝑜}\right)\to ⟨y,1_{𝑜}\setminus z⟩\in \left(I\times 2_{𝑜}\right)$$
4	2 3	sylan2	$$⊢\left(y\in I\wedge z\in 2_{𝑜}\right)\to ⟨y,1_{𝑜}\setminus z⟩\in \left(I\times 2_{𝑜}\right)$$
5	4	rgen2	$$⊢\forall y\in I\forall z\in 2_{𝑜}⟨y,1_{𝑜}\setminus z⟩\in \left(I\times 2_{𝑜}\right)$$
6	1	fmpo	$$⊢\forall y\in I\forall z\in 2_{𝑜}⟨y,1_{𝑜}\setminus z⟩\in \left(I\times 2_{𝑜}\right)\leftrightarrow M:I\times 2_{𝑜}⟶I\times 2_{𝑜}$$
7	5 6	mpbi	$$⊢M:I\times 2_{𝑜}⟶I\times 2_{𝑜}$$