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	syl5eq	⊢ ( 𝐾 ∈ V → 𝐼 = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } )
33	4 32	syl	⊢ ( 𝐾 ∈ 𝐴 → 𝐼 = { 𝑓 ∣ ( 𝑓 : 𝐵 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑓 ‘ 𝑥 ) ≤ ( 𝑓 ‘ 𝑦 ) ) ) } )