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 = Base K
glbcon.u U = lub K
glbcon.g G = glb K
glbcon.o ˙ = oc K
Assertion glbconxN K HL i I S B G x | i I x = S = ˙ U x | i I 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 vex y V
6 eqeq1 x = y x = S y = S
7 6 rexbidv x = y i I x = S i I y = S
8 5 7 elab y x | i I x = S i I y = S
9 nfra1 i i I S B
10 nfv i y B
11 rsp i I S B i I S B
12 eleq1a S B y = S y B
13 11 12 syl6 i I S B i I y = S y B
14 9 10 13 rexlimd i I S B i I y = S y B
15 8 14 syl5bi i I S B y x | i I x = S y B
16 15 ssrdv i I S B x | i I x = S B
17 1 2 3 4 glbconN K HL x | i I x = S B G x | i I x = S = ˙ U y B | ˙ y x | i I x = S
18 16 17 sylan2 K HL i I S B G x | i I x = S = ˙ U y B | ˙ y x | i I x = S
19 fvex ˙ y V
20 eqeq1 x = ˙ y x = S ˙ y = S
21 20 rexbidv x = ˙ y i I x = S i I ˙ y = S
22 19 21 elab ˙ y x | i I x = S i I ˙ y = S
23 22 rabbii y B | ˙ y x | i I x = S = y B | i I ˙ y = S
24 df-rab y B | i I ˙ y = S = y | y B i I ˙ y = S
25 23 24 eqtri y B | ˙ y x | i I x = S = y | y B i I ˙ y = S
26 nfv i K HL
27 26 9 nfan i K HL i I S B
28 rspa i I S B i I S B
29 hlop K HL K OP
30 1 4 opoccl K OP S B ˙ S B
31 29 30 sylan K HL S B ˙ S B
32 eleq1a ˙ S B y = ˙ S y B
33 31 32 syl K HL S B y = ˙ S y B
34 33 pm4.71rd K HL S B y = ˙ S y B y = ˙ S
35 1 4 opcon2b K OP S B y B S = ˙ y y = ˙ S
36 29 35 syl3an1 K HL S B y B S = ˙ y y = ˙ S
37 36 3expa K HL S B y B S = ˙ y y = ˙ S
38 eqcom S = ˙ y ˙ y = S
39 37 38 bitr3di K HL S B y B y = ˙ S ˙ y = S
40 39 pm5.32da K HL S B y B y = ˙ S y B ˙ y = S
41 34 40 bitrd K HL S B y = ˙ S y B ˙ y = S
42 28 41 sylan2 K HL i I S B i I y = ˙ S y B ˙ y = S
43 42 anassrs K HL i I S B i I y = ˙ S y B ˙ y = S
44 27 43 rexbida K HL i I S B i I y = ˙ S i I y B ˙ y = S
45 r19.42v i I y B ˙ y = S y B i I ˙ y = S
46 44 45 bitr2di K HL i I S B y B i I ˙ y = S i I y = ˙ S
47 46 abbidv K HL i I S B y | y B i I ˙ y = S = y | i I y = ˙ S
48 eqeq1 y = x y = ˙ S x = ˙ S
49 48 rexbidv y = x i I y = ˙ S i I x = ˙ S
50 49 cbvabv y | i I y = ˙ S = x | i I x = ˙ S
51 47 50 eqtrdi K HL i I S B y | y B i I ˙ y = S = x | i I x = ˙ S
52 25 51 syl5eq K HL i I S B y B | ˙ y x | i I x = S = x | i I x = ˙ S
53 52 fveq2d K HL i I S B U y B | ˙ y x | i I x = S = U x | i I x = ˙ S
54 53 fveq2d K HL i I S B ˙ U y B | ˙ y x | i I x = S = ˙ U x | i I x = ˙ S
55 18 54 eqtrd K HL i I S B G x | i I x = S = ˙ U x | i I x = ˙ S