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