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