Metamath Proof Explorer


Theorem lautcnvclN

Description: Reverse closure of a lattice automorphism. (Contributed by NM, 25-May-2012) (New usage is discouraged.)

Ref Expression
Hypotheses laut1o.b B = Base K
laut1o.i I = LAut K
Assertion lautcnvclN K V F I X B F -1 X B

Proof

Step Hyp Ref Expression
1 laut1o.b B = Base K
2 laut1o.i I = LAut K
3 1 2 laut1o K V F I F : B 1-1 onto B
4 f1ocnvdm F : B 1-1 onto B X B F -1 X B
5 3 4 sylan K V F I X B F -1 X B