Metamath Proof Explorer


Theorem laut1o

Description: A lattice automorphism is one-to-one and onto. (Contributed by NM, 19-May-2012)

Ref Expression
Hypotheses laut1o.b 𝐵 = ( Base ‘ 𝐾 )
laut1o.i 𝐼 = ( LAut ‘ 𝐾 )
Assertion laut1o ( ( 𝐾𝐴𝐹𝐼 ) → 𝐹 : 𝐵1-1-onto𝐵 )

Proof

Step Hyp Ref Expression
1 laut1o.b 𝐵 = ( Base ‘ 𝐾 )
2 laut1o.i 𝐼 = ( LAut ‘ 𝐾 )
3 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 1 3 2 islaut ( 𝐾𝐴 → ( 𝐹𝐼 ↔ ( 𝐹 : 𝐵1-1-onto𝐵 ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( 𝐹𝑥 ) ( le ‘ 𝐾 ) ( 𝐹𝑦 ) ) ) ) )
5 4 simprbda ( ( 𝐾𝐴𝐹𝐼 ) → 𝐹 : 𝐵1-1-onto𝐵 )