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=BaseK
idlaut.i ⊢I=LAut⁡K
Assertion idlaut ⊢K∈A→I↾B∈I

Proof

Step Hyp Ref Expression
1 idlaut.b ⊢B=BaseK
2 idlaut.i ⊢I=LAut⁡K
3 f1oi ⊢I↾B:B⟶1-1 ontoB
4 3 a1i ⊢K∈A→I↾B:B⟶1-1 ontoB
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≤KI↾B⁡y↔x≤Ky
8 7 bicomd ⊢x∈B∧y∈B→x≤Ky↔I↾B⁡x≤KI↾B⁡y
9 8 rgen2 ⊢∀x∈B∀y∈Bx≤Ky↔I↾B⁡x≤KI↾B⁡y
10 9 a1i ⊢K∈A→∀x∈B∀y∈Bx≤Ky↔I↾B⁡x≤KI↾B⁡y
11 eqid ⊢≤K=≤K
12 1 11 2 islaut ⊢K∈A→I↾B∈I↔I↾B:B⟶1-1 ontoB∧∀x∈B∀y∈Bx≤Ky↔I↾B⁡x≤KI↾B⁡y
13 4 10 12 mpbir2and ⊢K∈A→I↾B∈I