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

Metamath Proof Explorer

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 )