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 = Base K
glbcon.u U = lub K
glbcon.g G = glb K
glbcon.o ˙ = oc K
Assertion glbconN K HL S B G S = ˙ U x B | ˙ x S

Proof

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