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 = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
Assertion	efgmf	|- M : ( I X. 2o ) --> ( I X. 2o )

Proof

Step	Hyp	Ref	Expression
1		efgmval.m	|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
2		2oconcl	|- ( z e. 2o -> ( 1o \ z ) e. 2o )
3		opelxpi	|- ( ( y e. I /\ ( 1o \ z ) e. 2o ) -> <. y , ( 1o \ z ) >. e. ( I X. 2o ) )
4	2 3	sylan2	|- ( ( y e. I /\ z e. 2o ) -> <. y , ( 1o \ z ) >. e. ( I X. 2o ) )
5	4	rgen2	|- A. y e. I A. z e. 2o <. y , ( 1o \ z ) >. e. ( I X. 2o )
6	1	fmpo	|- ( A. y e. I A. z e. 2o <. y , ( 1o \ z ) >. e. ( I X. 2o ) <-> M : ( I X. 2o ) --> ( I X. 2o ) )
7	5 6	mpbi	|- M : ( I X. 2o ) --> ( I X. 2o )