Metamath Proof Explorer

Definition df-laut

Description: Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012)

Ref Expression
Assertion df-laut ⊢ LAut = k ∈ V ⟼ f | f : Base k ⟶ 1-1 onto Base k ∧ ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 claut class LAut
1 vk setvar k
2 cvv class V
3 vf setvar f
4 3 cv setvar f
5 cbs class Base
6 1 cv setvar k
7 6 5 cfv class Base k
8 7 7 4 wf1o wff f : Base k ⟶ 1-1 onto Base k
9 vx setvar x
10 vy setvar y
11 9 cv setvar x
12 cple class le
13 6 12 cfv class ≤ k
14 10 cv setvar y
15 11 14 13 wbr wff x ≤ k y
16 11 4 cfv class f ⁡ x
17 14 4 cfv class f ⁡ y
18 16 17 13 wbr wff f ⁡ x ≤ k f ⁡ y
19 15 18 wb wff x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y
20 19 10 7 wral wff ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y
21 20 9 7 wral wff ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y
22 8 21 wa wff f : Base k ⟶ 1-1 onto Base k ∧ ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y
23 22 3 cab class f | f : Base k ⟶ 1-1 onto Base k ∧ ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y
24 1 2 23 cmpt class k ∈ V ⟼ f | f : Base k ⟶ 1-1 onto Base k ∧ ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y
25 0 24 wceq wff LAut = k ∈ V ⟼ f | f : Base k ⟶ 1-1 onto Base k ∧ ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y