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 ↾ 𝐴 ) Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		f1oi	⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴
2		fvresi	⊢ ( 𝑥 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑥 ) = 𝑥 )
3		fvresi	⊢ ( 𝑦 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑦 ) = 𝑦 )
4	2 3	breqan12d	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( I ↾ 𝐴 ) ‘ 𝑥 ) 𝑅 ( ( I ↾ 𝐴 ) ‘ 𝑦 ) ↔ 𝑥 𝑅 𝑦 ) )
5	4	bicomd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ( ( I ↾ 𝐴 ) ‘ 𝑥 ) 𝑅 ( ( I ↾ 𝐴 ) ‘ 𝑦 ) ) )
6	5	rgen2	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( I ↾ 𝐴 ) ‘ 𝑥 ) 𝑅 ( ( I ↾ 𝐴 ) ‘ 𝑦 ) )
7		df-isom	⊢ ( ( I ↾ 𝐴 ) Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 ) ↔ ( ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( I ↾ 𝐴 ) ‘ 𝑥 ) 𝑅 ( ( I ↾ 𝐴 ) ‘ 𝑦 ) ) ) )
8	1 6 7	mpbir2an	⊢ ( I ↾ 𝐴 ) Isom 𝑅 , 𝑅 ( 𝐴 , 𝐴 )