Step |
Hyp |
Ref |
Expression |
1 |
|
olj0.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
olj0.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
olj0.z |
⊢ 0 = ( 0. ‘ 𝐾 ) |
4 |
|
olop |
⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP ) |
5 |
1 3
|
op0cl |
⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 ) |
6 |
4 5
|
syl |
⊢ ( 𝐾 ∈ OL → 0 ∈ 𝐵 ) |
7 |
6
|
adantr |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 ) |
8 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
9 |
|
ollat |
⊢ ( 𝐾 ∈ OL → 𝐾 ∈ Lat ) |
10 |
9
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → 𝐾 ∈ Lat ) |
11 |
1 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑋 ∨ 0 ) ∈ 𝐵 ) |
12 |
9 11
|
syl3an1 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑋 ∨ 0 ) ∈ 𝐵 ) |
13 |
|
simp2 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 ) |
14 |
1 8
|
latref |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) 𝑋 ) |
15 |
9 14
|
sylan |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) 𝑋 ) |
16 |
15
|
3adant3 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) 𝑋 ) |
17 |
1 8 3
|
op0le |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 0 ( le ‘ 𝐾 ) 𝑋 ) |
18 |
4 17
|
sylan |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 0 ( le ‘ 𝐾 ) 𝑋 ) |
19 |
18
|
3adant3 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → 0 ( le ‘ 𝐾 ) 𝑋 ) |
20 |
|
simp3 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → 0 ∈ 𝐵 ) |
21 |
1 8 2
|
latjle12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑋 ∧ 0 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑋 ∨ 0 ) ( le ‘ 𝐾 ) 𝑋 ) ) |
22 |
10 13 20 13 21
|
syl13anc |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑋 ∧ 0 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑋 ∨ 0 ) ( le ‘ 𝐾 ) 𝑋 ) ) |
23 |
16 19 22
|
mpbi2and |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑋 ∨ 0 ) ( le ‘ 𝐾 ) 𝑋 ) |
24 |
1 8 2
|
latlej1 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 0 ) ) |
25 |
9 24
|
syl3an1 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 0 ) ) |
26 |
1 8 10 12 13 23 25
|
latasymd |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑋 ∨ 0 ) = 𝑋 ) |
27 |
7 26
|
mpd3an3 |
⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ 0 ) = 𝑋 ) |