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

Metamath Proof Explorer

Theorem lautj

Description: Meet property of a lattice automorphism. (Contributed by NM, 25-May-2012)

Ref Expression
Hypotheses lautj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lautj.j ⊢ ∨ = ( join ‘ 𝐾 )
lautj.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
Assertion lautj ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lautj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lautj.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lautj.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 simpl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
6 simpr1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐹 ∈ 𝐼 )
7 5 6 jca ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) )
8 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
9 8 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
10 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∈ 𝐵 )
11 7 9 10 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∈ 𝐵 )
12 simpr2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
13 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
14 7 12 13 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
15 simpr3 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
16 1 3 lautcl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
17 7 15 16 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 )
18 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 )
19 5 14 17 18 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 )
20 1 3 laut1o ⊢ ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
21 20 3ad2antr1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
22 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )
23 21 9 22 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )
24 1 4 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )
25 5 14 17 24 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )
26 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) = ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )
27 21 19 26 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) = ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )
28 25 27 breqtrrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) )
29 f1ocnvdm ⊢ ( ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 )
30 21 19 29 syl2anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 )
31 1 4 3 lautle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 ) ) → ( 𝑋 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
32 7 12 30 31 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
33 28 32 mpbird ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) )
34 1 4 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )
35 5 14 17 34 syl3anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )
36 35 27 breqtrrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) )
37 1 4 3 lautle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 ) ) → ( 𝑌 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
38 7 15 30 37 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑌 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ↔ ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) ) )
39 36 38 mpbird ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) )
40 1 4 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑌 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) ↔ ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) )
41 5 12 15 30 40 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑌 ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) ↔ ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) )
42 33 39 41 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∨ 𝑌 ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) )
43 23 42 eqbrtrd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) )
44 1 4 3 lautcnvle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ∈ 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ↔ ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) )
45 7 11 19 44 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ↔ ( ◡ 𝐹 ‘ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) ( le ‘ 𝐾 ) ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ) ) )
46 43 45 mpbird ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ( le ‘ 𝐾 ) ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )
47 1 4 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
48 47 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
49 1 4 3 lautle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) ) → ( 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ↔ ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) )
50 7 12 9 49 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ↔ ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) )
51 48 50 mpbid ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) )
52 1 4 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
53 52 3adant3r1 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
54 1 4 3 lautle ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝐹 ∈ 𝐼 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) ) → ( 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ↔ ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) )
55 7 15 9 54 syl12anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑌 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ↔ ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) )
56 53 55 mpbid ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) )
57 1 4 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∧ ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) )
58 5 14 17 11 57 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ∧ ( 𝐹 ‘ 𝑌 ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) ) )
59 51 56 58 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) ( le ‘ 𝐾 ) ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) )
60 1 4 5 11 19 46 59 latasymd ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) ∨ ( 𝐹 ‘ 𝑌 ) ) )