# Metamath Proof Explorer

## Theorem oldmm1

Description: De Morgan's law for meet in an ortholattice. ( chdmm1 analog.) (Contributed by NM, 6-Nov-2011)

Ref Expression
Hypotheses oldmm1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
oldmm1.j
oldmm1.m
oldmm1.o
Assertion oldmm1

### Proof

Step Hyp Ref Expression
1 oldmm1.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 oldmm1.j
3 oldmm1.m
4 oldmm1.o
5 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
6 ollat ${⊢}{K}\in \mathrm{OL}\to {K}\in \mathrm{Lat}$
7 6 3ad2ant1 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{Lat}$
8 olop ${⊢}{K}\in \mathrm{OL}\to {K}\in \mathrm{OP}$
9 8 3ad2ant1 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{OP}$
10 1 3 latmcl
11 6 10 syl3an1
12 1 4 opoccl
13 9 11 12 syl2anc
14 1 4 opoccl
15 8 14 sylan
17 1 4 opoccl
18 8 17 sylan
20 1 2 latjcl
21 7 16 19 20 syl3anc
22 1 5 2 latlej1
23 7 16 19 22 syl3anc
24 simp2 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {B}$
25 1 5 4 oplecon1b
26 9 24 21 25 syl3anc
27 23 26 mpbid
28 1 5 2 latlej2
29 7 16 19 28 syl3anc
30 simp3 ${⊢}\left({K}\in \mathrm{OL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
31 1 5 4 oplecon1b
32 9 30 21 31 syl3anc
33 29 32 mpbid
34 1 4 opoccl
35 9 21 34 syl2anc
36 1 5 3 latlem12
37 7 35 24 30 36 syl13anc
38 27 33 37 mpbi2and
39 1 5 4 oplecon1b
40 9 21 11 39 syl3anc
41 38 40 mpbid
42 1 5 3 latmle1
43 6 42 syl3an1
44 1 5 4 oplecon3b
45 9 11 24 44 syl3anc
46 43 45 mpbid
47 1 5 3 latmle2
48 6 47 syl3an1
49 1 5 4 oplecon3b
50 9 11 30 49 syl3anc
51 48 50 mpbid
52 1 5 2 latjle12
53 7 16 19 13 52 syl13anc
54 46 51 53 mpbi2and
55 1 5 7 13 21 41 54 latasymd