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 e. V /\ F e. I ) /\ X e. B ) -> ( `' F ` X ) e. B )

Proof

Step Hyp Ref Expression
1 laut1o.b
 |-  B = ( Base ` K )
2 laut1o.i
 |-  I = ( LAut ` K )
3 1 2 laut1o
 |-  ( ( K e. V /\ F e. I ) -> F : B -1-1-onto-> B )
4 f1ocnvdm
 |-  ( ( F : B -1-1-onto-> B /\ X e. B ) -> ( `' F ` X ) e. B )
5 3 4 sylan
 |-  ( ( ( K e. V /\ F e. I ) /\ X e. B ) -> ( `' F ` X ) e. B )