Metamath Proof Explorer

Theorem efgmnvl

Description: The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Hypothesis efgmval.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
Assertion efgmnvl 
|- ( A e. ( I X. 2o ) -> ( M ` ( M ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 efgmval.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
2 elxp2 
 |-  ( A e. ( I X. 2o ) <-> E. a e. I E. b e. 2o A = <. a , b >. )
3 1 efgmval 
 |-  ( ( a e. I /\ b e. 2o ) -> ( a M b ) = <. a , ( 1o \ b ) >. )
4 3 fveq2d 
 |-  ( ( a e. I /\ b e. 2o ) -> ( M ` ( a M b ) ) = ( M ` <. a , ( 1o \ b ) >. ) )
5 df-ov 
 |-  ( a M ( 1o \ b ) ) = ( M ` <. a , ( 1o \ b ) >. )
6 4 5 eqtr4di 
 |-  ( ( a e. I /\ b e. 2o ) -> ( M ` ( a M b ) ) = ( a M ( 1o \ b ) ) )
7 2oconcl 
 |-  ( b e. 2o -> ( 1o \ b ) e. 2o )
8 1 efgmval 
 |-  ( ( a e. I /\ ( 1o \ b ) e. 2o ) -> ( a M ( 1o \ b ) ) = <. a , ( 1o \ ( 1o \ b ) ) >. )
9 7 8 sylan2 
 |-  ( ( a e. I /\ b e. 2o ) -> ( a M ( 1o \ b ) ) = <. a , ( 1o \ ( 1o \ b ) ) >. )
10 1on 
 |-  1o e. On
11 10 onordi 
 |-  Ord 1o
12 ordtr 
 |-  ( Ord 1o -> Tr 1o )
13 trsucss 
 |-  ( Tr 1o -> ( b e. suc 1o -> b C_ 1o ) )
14 11 12 13 mp2b 
 |-  ( b e. suc 1o -> b C_ 1o )
15 df-2o 
 |-  2o = suc 1o
16 14 15 eleq2s 
 |-  ( b e. 2o -> b C_ 1o )
17 16 adantl 
 |-  ( ( a e. I /\ b e. 2o ) -> b C_ 1o )
18 dfss4 
 |-  ( b C_ 1o <-> ( 1o \ ( 1o \ b ) ) = b )
19 17 18 sylib 
 |-  ( ( a e. I /\ b e. 2o ) -> ( 1o \ ( 1o \ b ) ) = b )
20 19 opeq2d 
 |-  ( ( a e. I /\ b e. 2o ) -> <. a , ( 1o \ ( 1o \ b ) ) >. = <. a , b >. )
21 6 9 20 3eqtrd 
 |-  ( ( a e. I /\ b e. 2o ) -> ( M ` ( a M b ) ) = <. a , b >. )
22 fveq2 
 |-  ( A = <. a , b >. -> ( M ` A ) = ( M ` <. a , b >. ) )
23 df-ov 
 |-  ( a M b ) = ( M ` <. a , b >. )
24 22 23 eqtr4di 
 |-  ( A = <. a , b >. -> ( M ` A ) = ( a M b ) )
25 24 fveq2d 
 |-  ( A = <. a , b >. -> ( M ` ( M ` A ) ) = ( M ` ( a M b ) ) )
26 id 
 |-  ( A = <. a , b >. -> A = <. a , b >. )
27 25 26 eqeq12d 
 |-  ( A = <. a , b >. -> ( ( M ` ( M ` A ) ) = A <-> ( M ` ( a M b ) ) = <. a , b >. ) )
28 21 27 syl5ibrcom 
 |-  ( ( a e. I /\ b e. 2o ) -> ( A = <. a , b >. -> ( M ` ( M ` A ) ) = A ) )
29 28 rexlimivv 
 |-  ( E. a e. I E. b e. 2o A = <. a , b >. -> ( M ` ( M ` A ) ) = A )
30 2 29 sylbi 
 |-  ( A e. ( I X. 2o ) -> ( M ` ( M ` A ) ) = A )