# Metamath Proof Explorer

## Theorem glbconxN

Description: De Morgan's law for GLB and LUB. Index-set version of glbconN , where we read S as S ( i ) . (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 glbconxN

### 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 vex ${⊢}{y}\in \mathrm{V}$
6 eqeq1 ${⊢}{x}={y}\to \left({x}={S}↔{y}={S}\right)$
7 6 rexbidv ${⊢}{x}={y}\to \left(\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}={S}↔\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}={S}\right)$
8 5 7 elab ${⊢}{y}\in \left\{{x}|\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}={S}\right\}↔\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}={S}$
9 nfra1 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{S}\in {B}$
10 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
11 rsp ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{S}\in {B}\to \left({i}\in {I}\to {S}\in {B}\right)$
12 eleq1a ${⊢}{S}\in {B}\to \left({y}={S}\to {y}\in {B}\right)$
13 11 12 syl6 ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{S}\in {B}\to \left({i}\in {I}\to \left({y}={S}\to {y}\in {B}\right)\right)$
14 9 10 13 rexlimd ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{S}\in {B}\to \left(\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}{y}={S}\to {y}\in {B}\right)$
15 8 14 syl5bi ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{S}\in {B}\to \left({y}\in \left\{{x}|\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}={S}\right\}\to {y}\in {B}\right)$
16 15 ssrdv ${⊢}\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{S}\in {B}\to \left\{{x}|\exists {i}\in {I}\phantom{\rule{.4em}{0ex}}{x}={S}\right\}\subseteq {B}$
17 1 2 3 4 glbconN
18 16 17 sylan2
19 fvex
20 eqeq1
21 20 rexbidv
22 19 21 elab
23 22 rabbii
24 df-rab
25 23 24 eqtri
26 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{K}\in \mathrm{HL}$
27 26 9 nfan ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({K}\in \mathrm{HL}\wedge \forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{S}\in {B}\right)$
28 rspa ${⊢}\left(\forall {i}\in {I}\phantom{\rule{.4em}{0ex}}{S}\in {B}\wedge {i}\in {I}\right)\to {S}\in {B}$
29 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
30 1 4 opoccl
31 29 30 sylan
32 eleq1a
33 31 32 syl
34 33 pm4.71rd
35 eqcom
36 1 4 opcon2b
37 29 36 syl3an1
38 37 3expa
39 35 38 syl5rbbr
40 39 pm5.32da
41 34 40 bitrd
42 28 41 sylan2
43 42 anassrs
44 27 43 rexbida
45 r19.42v
46 44 45 syl6rbb
47 46 abbidv
48 eqeq1
49 48 rexbidv
50 49 cbvabv
51 47 50 syl6eq
52 25 51 syl5eq
53 52 fveq2d
54 53 fveq2d
55 18 54 eqtrd