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 )