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 ‘ 𝑘 ) ( 𝑓 ‘ 𝑦 ) ) ) } )