Metamath Proof Explorer

Theorem lautset

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

Ref Expression
Hypotheses lautset.b ⊢ B = Base K
lautset.l ⊢ ≤ ˙ = ≤ K
lautset.i ⊢ I = LAut ⁡ K
Assertion lautset ⊢ K ∈ A → I = f | f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y

Proof

Step Hyp Ref Expression
1 lautset.b ⊢ B = Base K
2 lautset.l ⊢ ≤ ˙ = ≤ K
3 lautset.i ⊢ I = LAut ⁡ K
4 elex ⊢ K ∈ A → K ∈ V
5 fveq2 ⊢ k = K → Base k = Base K
6 5 1 eqtr4di ⊢ k = K → Base k = B
7 6 f1oeq2d ⊢ k = K → f : Base k ⟶ 1-1 onto Base k ↔ f : B ⟶ 1-1 onto Base k
8 f1oeq3 ⊢ Base k = B → f : B ⟶ 1-1 onto Base k ↔ f : B ⟶ 1-1 onto B
9 6 8 syl ⊢ k = K → f : B ⟶ 1-1 onto Base k ↔ f : B ⟶ 1-1 onto B
10 7 9 bitrd ⊢ k = K → f : Base k ⟶ 1-1 onto Base k ↔ f : B ⟶ 1-1 onto B
11 fveq2 ⊢ k = K → ≤ k = ≤ K
12 11 2 eqtr4di ⊢ k = K → ≤ k = ≤ ˙
13 12 breqd ⊢ k = K → x ≤ k y ↔ x ≤ ˙ y
14 12 breqd ⊢ k = K → f ⁡ x ≤ k f ⁡ y ↔ f ⁡ x ≤ ˙ f ⁡ y
15 13 14 bibi12d ⊢ k = K → x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y ↔ x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y
16 6 15 raleqbidv ⊢ k = K → ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y ↔ ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y
17 6 16 raleqbidv ⊢ k = K → ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y ↔ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y
18 10 17 anbi12d ⊢ k = K → f : Base k ⟶ 1-1 onto Base k ∧ ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y ↔ f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y
19 18 abbidv ⊢ k = K → f | f : Base k ⟶ 1-1 onto Base k ∧ ∀ x ∈ Base k ∀ y ∈ Base k x ≤ k y ↔ f ⁡ x ≤ k f ⁡ y = f | f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y
20 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
21 1 fvexi ⊢ B ∈ V
22 21 21 mapval ⊢ B B = f | f : B ⟶ B
23 ovex ⊢ B B ∈ V
24 22 23 eqeltrri ⊢ f | f : B ⟶ B ∈ V
25 f1of ⊢ f : B ⟶ 1-1 onto B → f : B ⟶ B
26 25 ss2abi ⊢ f | f : B ⟶ 1-1 onto B ⊆ f | f : B ⟶ B
27 24 26 ssexi ⊢ f | f : B ⟶ 1-1 onto B ∈ V
28 simpl ⊢ f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y → f : B ⟶ 1-1 onto B
29 28 ss2abi ⊢ f | f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y ⊆ f | f : B ⟶ 1-1 onto B
30 27 29 ssexi ⊢ f | f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y ∈ V
31 19 20 30 fvmpt ⊢ K ∈ V → LAut ⁡ K = f | f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y
32 3 31 syl5eq ⊢ K ∈ V → I = f | f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y
33 4 32 syl ⊢ K ∈ A → I = f | f : B ⟶ 1-1 onto B ∧ ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ f ⁡ x ≤ ˙ f ⁡ y