Metamath Proof Explorer

Theorem idlaut

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

Ref Expression
Hypotheses idlaut.b ⊢ B = Base K
idlaut.i ⊢ I = LAut ⁡ K
Assertion idlaut ⊢ K ∈ A → I ↾ B ∈ I

Proof

Step Hyp Ref Expression
1 idlaut.b ⊢ B = Base K
2 idlaut.i ⊢ I = LAut ⁡ K
3 f1oi ⊢ I ↾ B : B ⟶ 1-1 onto B
4 3 a1i ⊢ K ∈ A → I ↾ B : B ⟶ 1-1 onto B
5 fvresi ⊢ x ∈ B → I ↾ B ⁡ x = x
6 fvresi ⊢ y ∈ B → I ↾ B ⁡ y = y
7 5 6 breqan12d ⊢ x ∈ B ∧ y ∈ B → I ↾ B ⁡ x ≤ K I ↾ B ⁡ y ↔ x ≤ K y
8 7 bicomd ⊢ x ∈ B ∧ y ∈ B → x ≤ K y ↔ I ↾ B ⁡ x ≤ K I ↾ B ⁡ y
9 8 rgen2 ⊢ ∀ x ∈ B ∀ y ∈ B x ≤ K y ↔ I ↾ B ⁡ x ≤ K I ↾ B ⁡ y
10 9 a1i ⊢ K ∈ A → ∀ x ∈ B ∀ y ∈ B x ≤ K y ↔ I ↾ B ⁡ x ≤ K I ↾ B ⁡ y
11 eqid ⊢ ≤ K = ≤ K
12 1 11 2 islaut ⊢ K ∈ A → I ↾ B ∈ I ↔ I ↾ B : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ K y ↔ I ↾ B ⁡ x ≤ K I ↾ B ⁡ y
13 4 10 12 mpbir2and ⊢ K ∈ A → I ↾ B ∈ I