# Metamath Proof Explorer

## Theorem glbconN

Description: De Morgan's law for GLB and LUB. This holds in any complete ortholattice, although we assume HL for convenience. (Contributed by NM, 17-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses glbcon.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
glbcon.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
glbcon.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
glbcon.o
Assertion glbconN

### Proof

Step Hyp Ref Expression
1 glbcon.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 glbcon.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
3 glbcon.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
4 glbcon.o
5 dfin5 ${⊢}{B}\cap {S}=\left\{{x}\in {B}|{x}\in {S}\right\}$
6 sseqin2 ${⊢}{S}\subseteq {B}↔{B}\cap {S}={S}$
7 6 biimpi ${⊢}{S}\subseteq {B}\to {B}\cap {S}={S}$
8 5 7 syl5reqr ${⊢}{S}\subseteq {B}\to {S}=\left\{{x}\in {B}|{x}\in {S}\right\}$
9 8 fveq2d ${⊢}{S}\subseteq {B}\to {G}\left({S}\right)={G}\left(\left\{{x}\in {B}|{x}\in {S}\right\}\right)$
10 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
11 biid ${⊢}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\wedge \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{w}{\le }_{{K}}{z}\to {w}{\le }_{{K}}{y}\right)\right)↔\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\wedge \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{w}{\le }_{{K}}{z}\to {w}{\le }_{{K}}{y}\right)\right)$
12 id ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{HL}$
13 ssrab2 ${⊢}\left\{{x}\in {B}|{x}\in {S}\right\}\subseteq {B}$
14 13 a1i ${⊢}{K}\in \mathrm{HL}\to \left\{{x}\in {B}|{x}\in {S}\right\}\subseteq {B}$
15 1 10 3 11 12 14 glbval ${⊢}{K}\in \mathrm{HL}\to {G}\left(\left\{{x}\in {B}|{x}\in {S}\right\}\right)=\left(\iota {y}\in {B}|\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\wedge \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{w}{\le }_{{K}}{z}\to {w}{\le }_{{K}}{y}\right)\right)\right)$
16 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
17 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
18 1 3 clatglbcl ${⊢}\left({K}\in \mathrm{CLat}\wedge \left\{{x}\in {B}|{x}\in {S}\right\}\subseteq {B}\right)\to {G}\left(\left\{{x}\in {B}|{x}\in {S}\right\}\right)\in {B}$
19 17 13 18 sylancl ${⊢}{K}\in \mathrm{HL}\to {G}\left(\left\{{x}\in {B}|{x}\in {S}\right\}\right)\in {B}$
20 15 19 eqeltrrd ${⊢}{K}\in \mathrm{HL}\to \left(\iota {y}\in {B}|\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\wedge \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{w}{\le }_{{K}}{z}\to {w}{\le }_{{K}}{y}\right)\right)\right)\in {B}$
21 1 fvexi ${⊢}{B}\in \mathrm{V}$
22 21 riotaclbBAD ${⊢}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\wedge \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{w}{\le }_{{K}}{z}\to {w}{\le }_{{K}}{y}\right)\right)↔\left(\iota {y}\in {B}|\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\wedge \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{w}{\le }_{{K}}{z}\to {w}{\le }_{{K}}{y}\right)\right)\right)\in {B}$
23 20 22 sylibr ${⊢}{K}\in \mathrm{HL}\to \exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{y}{\le }_{{K}}{z}\wedge \forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\forall {z}\in \left\{{x}\in {B}|{x}\in {S}\right\}\phantom{\rule{.4em}{0ex}}{w}{\le }_{{K}}{z}\to {w}{\le }_{{K}}{y}\right)\right)$
24 breq1
25 24 ralbidv
26 breq2
27 26 imbi2d
28 27 ralbidv
29 25 28 anbi12d
30 1 4 29 riotaocN
31 16 23 30 syl2anc
32 16 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {u}\in {B}\right)\to {K}\in \mathrm{OP}$
33 1 4 opoccl
34 32 33 sylancom
35 16 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {z}\in {B}\right)\to {K}\in \mathrm{OP}$
36 1 4 opoccl
37 35 36 sylancom
38 1 4 opococ
39 35 38 sylancom
40 39 eqcomd
41 fveq2
42 41 rspceeqv
43 37 40 42 syl2anc
44 eleq1
45 breq2
46 44 45 imbi12d
48 34 43 47 ralxfrd
49 simpr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {u}\in {B}\right)\to {u}\in {B}$
50 simplr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {u}\in {B}\right)\to {v}\in {B}$
51 1 10 4 oplecon3b
52 32 49 50 51 syl3anc
53 52 imbi2d
54 53 ralbidva
55 48 54 bitr4d
56 eleq1 ${⊢}{x}={z}\to \left({x}\in {S}↔{z}\in {S}\right)$
57 56 ralrab
58 fveq2
59 58 eleq1d
60 59 ralrab
61 55 57 60 3bitr4g
62 16 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {t}\in {B}\right)\to {K}\in \mathrm{OP}$
63 1 4 opoccl
64 62 63 sylancom
65 16 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {w}\in {B}\right)\to {K}\in \mathrm{OP}$
66 1 4 opoccl
67 65 66 sylancom
68 1 4 opococ
69 65 68 sylancom
70 69 eqcomd
71 fveq2
72 71 rspceeqv
73 67 70 72 syl2anc
74 breq1
75 74 ralbidv
76 breq1
77 75 76 imbi12d
79 64 73 78 ralxfrd
80 16 ad3antrrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {t}\in {B}\right)\wedge {u}\in {B}\right)\to {K}\in \mathrm{OP}$
81 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {t}\in {B}\right)\wedge {u}\in {B}\right)\to {u}\in {B}$
82 simplr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {t}\in {B}\right)\wedge {u}\in {B}\right)\to {t}\in {B}$
83 1 10 4 oplecon3b
84 80 81 82 83 syl3anc
85 84 imbi2d
86 85 ralbidva
87 80 33 sylancom
88 16 ad3antrrr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {t}\in {B}\right)\wedge {z}\in {B}\right)\to {K}\in \mathrm{OP}$
89 88 36 sylancom
90 88 38 sylancom
91 90 eqcomd
92 89 91 42 syl2anc
93 breq2
94 44 93 imbi12d
96 87 92 95 ralxfrd
97 86 96 bitr4d
98 59 ralrab
99 56 ralrab
100 97 98 99 3bitr4g
101 simplr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {t}\in {B}\right)\to {v}\in {B}$
102 simpr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {v}\in {B}\right)\wedge {t}\in {B}\right)\to {t}\in {B}$
103 1 10 4 oplecon3b
104 62 101 102 103 syl3anc
105 100 104 imbi12d
106 105 ralbidva
107 79 106 bitr4d
108 61 107 anbi12d
109 108 riotabidva
110 ssrab2
111 biid
112 simpl
113 simpr
114 1 10 2 111 112 113 lubval
115 110 114 mpan2
116 109 115 eqtr4d
117 116 fveq2d
118 15 31 117 3eqtrd
119 9 118 sylan9eqr