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

Metamath Proof Explorer

Theorem idlaut

Description: The identity function is a lattice automorphism. (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses idlaut.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
idlaut.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion idlaut ( 𝐾 ∈ 𝐴 → ( I ↾ 𝐵 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 idlaut.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 idlaut.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
3 f1oi ⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵
4 3 a1i ⊢ ( 𝐾 ∈ 𝐴 → ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 )
5 fvresi ⊢ ( 𝑥 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
6 fvresi ⊢ ( 𝑦 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
7 5 6 breqan12d ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ↔ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) )
8 7 bicomd ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) )
9 8 rgen2 ⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) )
10 9 a1i ⊢ ( 𝐾 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) )
11 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12 1 11 2 islaut ⊢ ( 𝐾 ∈ 𝐴 → ( ( I ↾ 𝐵 ) ∈ 𝐼 ↔ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( le ‘ 𝐾 ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ) ) )
13 4 10 12 mpbir2and ⊢ ( 𝐾 ∈ 𝐴 → ( I ↾ 𝐵 ) ∈ 𝐼 )