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

Metamath Proof Explorer

Definition df-laut

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

Ref Expression
Assertion df-laut LAut = ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 claut ⊢ LAut
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vf ⊢ 𝑓
4 3 cv ⊢ 𝑓
5 cbs ⊢ Base
6 1 cv ⊢ 𝑘
7 6 5 cfv ⊢ ( Base ‘ 𝑘 )
8 7 7 4 wf1o ⊢ 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 )
9 vx ⊢ 𝑥
10 vy ⊢ 𝑦
11 9 cv ⊢ 𝑥
12 cple ⊢ le
13 6 12 cfv ⊢ ( le ‘ 𝑘 )
14 10 cv ⊢ 𝑦
15 11 14 13 wbr ⊢ 𝑥 ( le ‘ 𝑘 ) 𝑦
16 11 4 cfv ⊢ ( 𝑓 ‘ 𝑥 )
17 14 4 cfv ⊢ ( 𝑓 ‘ 𝑦 )
18 16 17 13 wbr ⊢ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 )
19 15 18 wb ⊢ ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) )
20 19 10 7 wral ⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) )
21 20 9 7 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) )
22 8 21 wa ⊢ ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) )
23 22 3 cab ⊢ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ) }
24 1 2 23 cmpt ⊢ ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
25 0 24 wceq ⊢ LAut = ( 𝑘 ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑘 ) –1-1-onto→ ( Base ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ∀ 𝑦 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ( le ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ) } )