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

Metamath Proof Explorer

Theorem lautset

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

Ref Expression
Hypotheses lautset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lautset.l ⊢ ≤ = ( le ‘ 𝐾 )
lautset.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautset ( 𝐾 ∈ 𝐴 → 𝐼 = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } )

Proof

Step Hyp Ref Expression
1 lautset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lautset.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lautset.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
4 elex ⊢ ( 𝐾 ∈ 𝐴 → 𝐾 ∈ V )
5 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
6 5 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
7 6 f1oeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ↔ 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ 𝑘 ) ) )
8 f1oeq3 ⊢ ( ( Base ‘ 𝑘 ) = 𝐵 → ( 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ 𝑘 ) ↔ 𝑓 : 𝐵 –1-1-onto→ 𝐵 ) )
9 6 8 syl ⊢ ( 𝑘 = 𝐾 → ( 𝑓 : 𝐵 –1-1-onto→ ( Base ‘ 𝑘 ) ↔ 𝑓 : 𝐵 –1-1-onto→ 𝐵 ) )
10 7 9 bitrd ⊢ ( 𝑘 = 𝐾 → ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ↔ 𝑓 : 𝐵 –1-1-onto→ 𝐵 ) )
11 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
12 11 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
13 12 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
14 12 breqd ⊢ ( 𝑘 = 𝐾 → ( ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) )
15 13 14 bibi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) )
16 6 15 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) )
17 6 16 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) )
18 10 17 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) ) )
19 18 abbidv ⊢ ( 𝑘 = 𝐾 → { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } )
20 df-laut ⊢ LAut = ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
21 1 fvexi ⊢ 𝐵 ∈ V
22 21 21 mapval ⊢ ( 𝐵 ↑m 𝐵 ) = { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐵 }
23 ovex ⊢ ( 𝐵 ↑m 𝐵 ) ∈ V
24 22 23 eqeltrri ⊢ { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐵 } ∈ V
25 f1of ⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 → 𝑓 : 𝐵 ⟶ 𝐵 )
26 25 ss2abi ⊢ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐵 } ⊆ { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐵 }
27 24 26 ssexi ⊢ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐵 } ∈ V
28 simpl ⊢ ( ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) → 𝑓 : 𝐵 –1-1-onto→ 𝐵 )
29 28 ss2abi ⊢ { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ { 𝑓 ∣ 𝑓 : 𝐵 –1-1-onto→ 𝐵 }
30 27 29 ssexi ⊢ { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V
31 19 20 30 fvmpt ⊢ ( 𝐾 ∈ V → ( LAut ‘ 𝐾 ) = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } )
32 3 31 eqtrid ⊢ ( 𝐾 ∈ V → 𝐼 = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } )
33 4 32 syl ⊢ ( 𝐾 ∈ 𝐴 → 𝐼 = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } )