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

Metamath Proof Explorer

Theorem isoid

Description: Identity law for isomorphism. Proposition 6.30(1) of TakeutiZaring p. 33. (Contributed by NM, 27-Apr-2004)

Ref Expression
Assertion isoid 
|- ( _I |` A ) Isom R , R ( A , A )

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` A ) : A -1-1-onto-> A
2 fvresi 
 |-  ( x e. A -> ( ( _I |` A ) ` x ) = x )
3 fvresi 
 |-  ( y e. A -> ( ( _I |` A ) ` y ) = y )
4 2 3 breqan12d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( ( _I |` A ) ` x ) R ( ( _I |` A ) ` y ) <-> x R y ) )
5 4 bicomd 
 |-  ( ( x e. A /\ y e. A ) -> ( x R y <-> ( ( _I |` A ) ` x ) R ( ( _I |` A ) ` y ) ) )
6 5 rgen2 
 |-  A. x e. A A. y e. A ( x R y <-> ( ( _I |` A ) ` x ) R ( ( _I |` A ) ` y ) )
7 df-isom 
 |-  ( ( _I |` A ) Isom R , R ( A , A ) <-> ( ( _I |` A ) : A -1-1-onto-> A /\ A. x e. A A. y e. A ( x R y <-> ( ( _I |` A ) ` x ) R ( ( _I |` A ) ` y ) ) ) )
8 1 6 7 mpbir2an 
 |-  ( _I |` A ) Isom R , R ( A , A )