Metamath Proof Explorer


Theorem lautcl

Description: A lattice automorphism value belongs to the base set. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses laut1o.b 𝐵 = ( Base ‘ 𝐾 )
laut1o.i 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautcl ( ( ( 𝐾𝑉𝐹𝐼 ) ∧ 𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 laut1o.b 𝐵 = ( Base ‘ 𝐾 )
2 laut1o.i 𝐼 = ( LAut ‘ 𝐾 )
3 1 2 laut1o ( ( 𝐾𝑉𝐹𝐼 ) → 𝐹 : 𝐵1-1-onto𝐵 )
4 f1of ( 𝐹 : 𝐵1-1-onto𝐵𝐹 : 𝐵𝐵 )
5 3 4 syl ( ( 𝐾𝑉𝐹𝐼 ) → 𝐹 : 𝐵𝐵 )
6 5 ffvelrnda ( ( ( 𝐾𝑉𝐹𝐼 ) ∧ 𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ 𝐵 )