This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ B = {Base}_{K}$
	laut1o.i	$⊢ I = LAut (K)$
Assertion	laut1o	$⊢ (K \in A \land F \in I) \to F : B \underset{1-1 onto}{⟶} B$

Step	Hyp	Ref	Expression
1		laut1o.b	$⊢ B = {Base}_{K}$
2		laut1o.i	$⊢ I = LAut (K)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4	1 3 2	islaut	$⊢ K \in A \to (F \in I \leftrightarrow (F : B \underset{1-1 onto}{⟶} B \land \forall x \in B \forall y \in B (x \leq_{K} y \leftrightarrow F (x) \leq_{K} F (y))))$
5	4	simprbda	$⊢ (K \in A \land F \in I) \to F : B \underset{1-1 onto}{⟶} B$