# Metamath Proof Explorer

## Theorem lautcnvle

Description: Less-than or equal property of lattice automorphism converse. (Contributed by NM, 19-May-2012)

Ref Expression
Hypotheses lautcnvle.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
lautcnvle.l
lautcnvle.i ${⊢}{I}=\mathrm{LAut}\left({K}\right)$
Assertion lautcnvle

### Proof

Step Hyp Ref Expression
1 lautcnvle.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 lautcnvle.l
3 lautcnvle.i ${⊢}{I}=\mathrm{LAut}\left({K}\right)$
4 simpl ${⊢}\left(\left({K}\in {V}\wedge {F}\in {I}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({K}\in {V}\wedge {F}\in {I}\right)$
5 1 3 laut1o ${⊢}\left({K}\in {V}\wedge {F}\in {I}\right)\to {F}:{B}\underset{1-1 onto}{⟶}{B}$
6 5 adantr ${⊢}\left(\left({K}\in {V}\wedge {F}\in {I}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {F}:{B}\underset{1-1 onto}{⟶}{B}$
7 simprl ${⊢}\left(\left({K}\in {V}\wedge {F}\in {I}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
8 f1ocnvdm ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{B}\wedge {X}\in {B}\right)\to {{F}}^{-1}\left({X}\right)\in {B}$
9 6 7 8 syl2anc ${⊢}\left(\left({K}\in {V}\wedge {F}\in {I}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {{F}}^{-1}\left({X}\right)\in {B}$
10 simprr ${⊢}\left(\left({K}\in {V}\wedge {F}\in {I}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {Y}\in {B}$
11 f1ocnvdm ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{B}\wedge {Y}\in {B}\right)\to {{F}}^{-1}\left({Y}\right)\in {B}$
12 6 10 11 syl2anc ${⊢}\left(\left({K}\in {V}\wedge {F}\in {I}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {{F}}^{-1}\left({Y}\right)\in {B}$
13 1 2 3 lautle
14 4 9 12 13 syl12anc
15 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{B}\wedge {X}\in {B}\right)\to {F}\left({{F}}^{-1}\left({X}\right)\right)={X}$
16 6 7 15 syl2anc ${⊢}\left(\left({K}\in {V}\wedge {F}\in {I}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {F}\left({{F}}^{-1}\left({X}\right)\right)={X}$
17 f1ocnvfv2 ${⊢}\left({F}:{B}\underset{1-1 onto}{⟶}{B}\wedge {Y}\in {B}\right)\to {F}\left({{F}}^{-1}\left({Y}\right)\right)={Y}$
18 6 10 17 syl2anc ${⊢}\left(\left({K}\in {V}\wedge {F}\in {I}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {F}\left({{F}}^{-1}\left({Y}\right)\right)={Y}$
19 16 18 breq12d
20 14 19 bitr2d