Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  glbconN Structured version   Visualization version   Unicode version

Theorem glbconN 33013
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.)
Hypotheses
Ref Expression
glbcon.b  |-  B  =  ( Base `  K
)
glbcon.u  |-  U  =  ( lub `  K
)
glbcon.g  |-  G  =  ( glb `  K
)
glbcon.o  |-  ._|_  =  ( oc `  K )
Assertion
Ref Expression
glbconN  |-  ( ( K  e.  HL  /\  S  C_  B )  -> 
( G `  S
)  =  (  ._|_  `  ( U `  {
x  e.  B  | 
(  ._|_  `  x )  e.  S } ) ) )
Distinct variable groups:    x, B    x, 
._|_    x, S
Allowed substitution hints:    U( x)    G( x)    K( x)

Proof of Theorem glbconN
Dummy variables  u  t  v  w  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfin5 3398 . . . 4  |-  ( B  i^i  S )  =  { x  e.  B  |  x  e.  S }
2 sseqin2 3642 . . . . 5  |-  ( S 
C_  B  <->  ( B  i^i  S )  =  S )
32biimpi 199 . . . 4  |-  ( S 
C_  B  ->  ( B  i^i  S )  =  S )
41, 3syl5reqr 2520 . . 3  |-  ( S 
C_  B  ->  S  =  { x  e.  B  |  x  e.  S } )
54fveq2d 5883 . 2  |-  ( S 
C_  B  ->  ( G `  S )  =  ( G `  { x  e.  B  |  x  e.  S } ) )
6 glbcon.b . . . 4  |-  B  =  ( Base `  K
)
7 eqid 2471 . . . 4  |-  ( le
`  K )  =  ( le `  K
)
8 glbcon.g . . . 4  |-  G  =  ( glb `  K
)
9 biid 244 . . . 4  |-  ( ( A. z  e.  {
x  e.  B  |  x  e.  S }
y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) y ) )  <->  ( A. z  e.  { x  e.  B  |  x  e.  S } y ( le
`  K ) z  /\  A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le
`  K ) z  ->  w ( le
`  K ) y ) ) )
10 id 22 . . . 4  |-  ( K  e.  HL  ->  K  e.  HL )
11 ssrab2 3500 . . . . 5  |-  { x  e.  B  |  x  e.  S }  C_  B
1211a1i 11 . . . 4  |-  ( K  e.  HL  ->  { x  e.  B  |  x  e.  S }  C_  B
)
136, 7, 8, 9, 10, 12glbval 16321 . . 3  |-  ( K  e.  HL  ->  ( G `  { x  e.  B  |  x  e.  S } )  =  ( iota_ y  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) y ) ) ) )
14 hlop 32999 . . . 4  |-  ( K  e.  HL  ->  K  e.  OP )
15 hlclat 32995 . . . . . . 7  |-  ( K  e.  HL  ->  K  e.  CLat )
166, 8clatglbcl 16438 . . . . . . 7  |-  ( ( K  e.  CLat  /\  {
x  e.  B  |  x  e.  S }  C_  B )  ->  ( G `  { x  e.  B  |  x  e.  S } )  e.  B )
1715, 11, 16sylancl 675 . . . . . 6  |-  ( K  e.  HL  ->  ( G `  { x  e.  B  |  x  e.  S } )  e.  B )
1813, 17eqeltrrd 2550 . . . . 5  |-  ( K  e.  HL  ->  ( iota_ y  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) y ) ) )  e.  B
)
19 fvex 5889 . . . . . . 7  |-  ( Base `  K )  e.  _V
206, 19eqeltri 2545 . . . . . 6  |-  B  e. 
_V
2120riotaclbBAD 32591 . . . . 5  |-  ( E! y  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) y ) )  <->  ( iota_ y  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } y ( le
`  K ) z  /\  A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le
`  K ) z  ->  w ( le
`  K ) y ) ) )  e.  B )
2218, 21sylibr 217 . . . 4  |-  ( K  e.  HL  ->  E! y  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  ->  w ( le `  K ) y ) ) )
23 glbcon.o . . . . 5  |-  ._|_  =  ( oc `  K )
24 breq1 4398 . . . . . . 7  |-  ( y  =  (  ._|_  `  v
)  ->  ( y
( le `  K
) z  <->  (  ._|_  `  v ) ( le
`  K ) z ) )
2524ralbidv 2829 . . . . . 6  |-  ( y  =  (  ._|_  `  v
)  ->  ( A. z  e.  { x  e.  B  |  x  e.  S } y ( le `  K ) z  <->  A. z  e.  {
x  e.  B  |  x  e.  S } 
(  ._|_  `  v )
( le `  K
) z ) )
26 breq2 4399 . . . . . . . 8  |-  ( y  =  (  ._|_  `  v
)  ->  ( w
( le `  K
) y  <->  w ( le `  K ) ( 
._|_  `  v ) ) )
2726imbi2d 323 . . . . . . 7  |-  ( y  =  (  ._|_  `  v
)  ->  ( ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  ->  w ( le `  K ) y )  <->  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le
`  K ) z  ->  w ( le
`  K ) ( 
._|_  `  v ) ) ) )
2827ralbidv 2829 . . . . . 6  |-  ( y  =  (  ._|_  `  v
)  ->  ( A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  ->  w ( le `  K ) y )  <->  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) (  ._|_  `  v ) ) ) )
2925, 28anbi12d 725 . . . . 5  |-  ( y  =  (  ._|_  `  v
)  ->  ( ( A. z  e.  { x  e.  B  |  x  e.  S } y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  ->  w ( le `  K ) y ) )  <->  ( A. z  e.  { x  e.  B  |  x  e.  S }  (  ._|_  `  v ) ( le
`  K ) z  /\  A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le
`  K ) z  ->  w ( le
`  K ) ( 
._|_  `  v ) ) ) ) )
306, 23, 29riotaocN 32846 . . . 4  |-  ( ( K  e.  OP  /\  E! y  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) y ) ) )  ->  ( iota_ y  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) y ) ) )  =  ( 
._|_  `  ( iota_ v  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S }  (  ._|_  `  v
) ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) (  ._|_  `  v ) ) ) ) ) )
3114, 22, 30syl2anc 673 . . 3  |-  ( K  e.  HL  ->  ( iota_ y  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
y ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) y ) ) )  =  ( 
._|_  `  ( iota_ v  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S }  (  ._|_  `  v
) ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) (  ._|_  `  v ) ) ) ) ) )
3214ad2antrr 740 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  K  e.  OP )
336, 23opoccl 32831 . . . . . . . . . . 11  |-  ( ( K  e.  OP  /\  u  e.  B )  ->  (  ._|_  `  u )  e.  B )
3432, 33sylancom 680 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  (  ._|_  `  u )  e.  B
)
3514ad2antrr 740 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  K  e.  OP )
366, 23opoccl 32831 . . . . . . . . . . . 12  |-  ( ( K  e.  OP  /\  z  e.  B )  ->  (  ._|_  `  z )  e.  B )
3735, 36sylancom 680 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  (  ._|_  `  z )  e.  B
)
386, 23opococ 32832 . . . . . . . . . . . . 13  |-  ( ( K  e.  OP  /\  z  e.  B )  ->  (  ._|_  `  (  ._|_  `  z ) )  =  z )
3935, 38sylancom 680 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  (  ._|_  `  (  ._|_  `  z ) )  =  z )
4039eqcomd 2477 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  z  =  (  ._|_  `  (  ._|_  `  z ) ) )
41 fveq2 5879 . . . . . . . . . . . . 13  |-  ( u  =  (  ._|_  `  z
)  ->  (  ._|_  `  u )  =  ( 
._|_  `  (  ._|_  `  z
) ) )
4241eqeq2d 2481 . . . . . . . . . . . 12  |-  ( u  =  (  ._|_  `  z
)  ->  ( z  =  (  ._|_  `  u
)  <->  z  =  ( 
._|_  `  (  ._|_  `  z
) ) ) )
4342rspcev 3136 . . . . . . . . . . 11  |-  ( ( (  ._|_  `  z )  e.  B  /\  z  =  (  ._|_  `  (  ._|_  `  z ) ) )  ->  E. u  e.  B  z  =  (  ._|_  `  u )
)
4437, 40, 43syl2anc 673 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  E. u  e.  B  z  =  (  ._|_  `  u )
)
45 eleq1 2537 . . . . . . . . . . . 12  |-  ( z  =  (  ._|_  `  u
)  ->  ( z  e.  S  <->  (  ._|_  `  u
)  e.  S ) )
46 breq2 4399 . . . . . . . . . . . 12  |-  ( z  =  (  ._|_  `  u
)  ->  ( (  ._|_  `  v ) ( le `  K ) z  <->  (  ._|_  `  v
) ( le `  K ) (  ._|_  `  u ) ) )
4745, 46imbi12d 327 . . . . . . . . . . 11  |-  ( z  =  (  ._|_  `  u
)  ->  ( (
z  e.  S  -> 
(  ._|_  `  v )
( le `  K
) z )  <->  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  v ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
4847adantl 473 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  =  ( 
._|_  `  u ) )  ->  ( ( z  e.  S  ->  (  ._|_  `  v ) ( le `  K ) z )  <->  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  v ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
4934, 44, 48ralxfrd 4612 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  v  e.  B )  ->  ( A. z  e.  B  ( z  e.  S  ->  (  ._|_  `  v ) ( le
`  K ) z )  <->  A. u  e.  B  ( (  ._|_  `  u
)  e.  S  -> 
(  ._|_  `  v )
( le `  K
) (  ._|_  `  u
) ) ) )
50 simpr 468 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  u  e.  B )
51 simplr 770 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  v  e.  B )
526, 7, 23oplecon3b 32837 . . . . . . . . . . . 12  |-  ( ( K  e.  OP  /\  u  e.  B  /\  v  e.  B )  ->  ( u ( le
`  K ) v  <-> 
(  ._|_  `  v )
( le `  K
) (  ._|_  `  u
) ) )
5332, 50, 51, 52syl3anc 1292 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  ( u
( le `  K
) v  <->  (  ._|_  `  v ) ( le
`  K ) ( 
._|_  `  u ) ) )
5453imbi2d 323 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  ( (
(  ._|_  `  u )  e.  S  ->  u ( le `  K ) v )  <->  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  v ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
5554ralbidva 2828 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  v  e.  B )  ->  ( A. u  e.  B  ( (  ._|_  `  u )  e.  S  ->  u ( le `  K ) v )  <->  A. u  e.  B  ( (  ._|_  `  u
)  e.  S  -> 
(  ._|_  `  v )
( le `  K
) (  ._|_  `  u
) ) ) )
5649, 55bitr4d 264 . . . . . . . 8  |-  ( ( K  e.  HL  /\  v  e.  B )  ->  ( A. z  e.  B  ( z  e.  S  ->  (  ._|_  `  v ) ( le
`  K ) z )  <->  A. u  e.  B  ( (  ._|_  `  u
)  e.  S  ->  u ( le `  K ) v ) ) )
57 eleq1 2537 . . . . . . . . 9  |-  ( x  =  z  ->  (
x  e.  S  <->  z  e.  S ) )
5857ralrab 3188 . . . . . . . 8  |-  ( A. z  e.  { x  e.  B  |  x  e.  S }  (  ._|_  `  v ) ( le
`  K ) z  <->  A. z  e.  B  ( z  e.  S  ->  (  ._|_  `  v ) ( le `  K
) z ) )
59 fveq2 5879 . . . . . . . . . 10  |-  ( x  =  u  ->  (  ._|_  `  x )  =  (  ._|_  `  u ) )
6059eleq1d 2533 . . . . . . . . 9  |-  ( x  =  u  ->  (
(  ._|_  `  x )  e.  S  <->  (  ._|_  `  u
)  e.  S ) )
6160ralrab 3188 . . . . . . . 8  |-  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) v  <->  A. u  e.  B  ( (  ._|_  `  u
)  e.  S  ->  u ( le `  K ) v ) )
6256, 58, 613bitr4g 296 . . . . . . 7  |-  ( ( K  e.  HL  /\  v  e.  B )  ->  ( A. z  e. 
{ x  e.  B  |  x  e.  S }  (  ._|_  `  v
) ( le `  K ) z  <->  A. u  e.  { x  e.  B  |  (  ._|_  `  x
)  e.  S }
u ( le `  K ) v ) )
6314ad2antrr 740 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  K  e.  OP )
646, 23opoccl 32831 . . . . . . . . . 10  |-  ( ( K  e.  OP  /\  t  e.  B )  ->  (  ._|_  `  t )  e.  B )
6563, 64sylancom 680 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  (  ._|_  `  t )  e.  B
)
6614ad2antrr 740 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  K  e.  OP )
676, 23opoccl 32831 . . . . . . . . . . 11  |-  ( ( K  e.  OP  /\  w  e.  B )  ->  (  ._|_  `  w )  e.  B )
6866, 67sylancom 680 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  (  ._|_  `  w )  e.  B
)
696, 23opococ 32832 . . . . . . . . . . . 12  |-  ( ( K  e.  OP  /\  w  e.  B )  ->  (  ._|_  `  (  ._|_  `  w ) )  =  w )
7066, 69sylancom 680 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  (  ._|_  `  (  ._|_  `  w ) )  =  w )
7170eqcomd 2477 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  w  =  (  ._|_  `  (  ._|_  `  w ) ) )
72 fveq2 5879 . . . . . . . . . . . 12  |-  ( t  =  (  ._|_  `  w
)  ->  (  ._|_  `  t )  =  ( 
._|_  `  (  ._|_  `  w
) ) )
7372eqeq2d 2481 . . . . . . . . . . 11  |-  ( t  =  (  ._|_  `  w
)  ->  ( w  =  (  ._|_  `  t
)  <->  w  =  (  ._|_  `  (  ._|_  `  w
) ) ) )
7473rspcev 3136 . . . . . . . . . 10  |-  ( ( (  ._|_  `  w )  e.  B  /\  w  =  (  ._|_  `  (  ._|_  `  w ) ) )  ->  E. t  e.  B  w  =  (  ._|_  `  t )
)
7568, 71, 74syl2anc 673 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  E. t  e.  B  w  =  (  ._|_  `  t )
)
76 breq1 4398 . . . . . . . . . . . 12  |-  ( w  =  (  ._|_  `  t
)  ->  ( w
( le `  K
) z  <->  (  ._|_  `  t ) ( le
`  K ) z ) )
7776ralbidv 2829 . . . . . . . . . . 11  |-  ( w  =  (  ._|_  `  t
)  ->  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  <->  A. z  e.  {
x  e.  B  |  x  e.  S } 
(  ._|_  `  t )
( le `  K
) z ) )
78 breq1 4398 . . . . . . . . . . 11  |-  ( w  =  (  ._|_  `  t
)  ->  ( w
( le `  K
) (  ._|_  `  v
)  <->  (  ._|_  `  t
) ( le `  K ) (  ._|_  `  v ) ) )
7977, 78imbi12d 327 . . . . . . . . . 10  |-  ( w  =  (  ._|_  `  t
)  ->  ( ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  ->  w ( le `  K ) ( 
._|_  `  v ) )  <-> 
( A. z  e. 
{ x  e.  B  |  x  e.  S }  (  ._|_  `  t
) ( le `  K ) z  -> 
(  ._|_  `  t )
( le `  K
) (  ._|_  `  v
) ) ) )
8079adantl 473 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  =  ( 
._|_  `  t ) )  ->  ( ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  ->  w ( le `  K ) ( 
._|_  `  v ) )  <-> 
( A. z  e. 
{ x  e.  B  |  x  e.  S }  (  ._|_  `  t
) ( le `  K ) z  -> 
(  ._|_  `  t )
( le `  K
) (  ._|_  `  v
) ) ) )
8165, 75, 80ralxfrd 4612 . . . . . . . 8  |-  ( ( K  e.  HL  /\  v  e.  B )  ->  ( A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le
`  K ) z  ->  w ( le
`  K ) ( 
._|_  `  v ) )  <->  A. t  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S } 
(  ._|_  `  t )
( le `  K
) z  ->  (  ._|_  `  t ) ( le `  K ) (  ._|_  `  v ) ) ) )
8214ad3antrrr 744 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  K  e.  OP )
83 simpr 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  u  e.  B )
84 simplr 770 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  t  e.  B )
856, 7, 23oplecon3b 32837 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  OP  /\  u  e.  B  /\  t  e.  B )  ->  ( u ( le
`  K ) t  <-> 
(  ._|_  `  t )
( le `  K
) (  ._|_  `  u
) ) )
8682, 83, 84, 85syl3anc 1292 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  (
u ( le `  K ) t  <->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  u ) ) )
8786imbi2d 323 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  (
( (  ._|_  `  u
)  e.  S  ->  u ( le `  K ) t )  <-> 
( (  ._|_  `  u
)  e.  S  -> 
(  ._|_  `  t )
( le `  K
) (  ._|_  `  u
) ) ) )
8887ralbidva 2828 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  ( A. u  e.  B  (
(  ._|_  `  u )  e.  S  ->  u ( le `  K ) t )  <->  A. u  e.  B  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
8982, 33sylancom 680 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  (  ._|_  `  u )  e.  B )
9014ad3antrrr 744 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  K  e.  OP )
9190, 36sylancom 680 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  (  ._|_  `  z )  e.  B )
9290, 38sylancom 680 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  (  ._|_  `  (  ._|_  `  z
) )  =  z )
9392eqcomd 2477 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  z  =  (  ._|_  `  (  ._|_  `  z ) ) )
9491, 93, 43syl2anc 673 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  E. u  e.  B  z  =  (  ._|_  `  u )
)
95 breq2 4399 . . . . . . . . . . . . . . 15  |-  ( z  =  (  ._|_  `  u
)  ->  ( (  ._|_  `  t ) ( le `  K ) z  <->  (  ._|_  `  t
) ( le `  K ) (  ._|_  `  u ) ) )
9645, 95imbi12d 327 . . . . . . . . . . . . . 14  |-  ( z  =  (  ._|_  `  u
)  ->  ( (
z  e.  S  -> 
(  ._|_  `  t )
( le `  K
) z )  <->  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
9796adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  =  (  ._|_  `  u
) )  ->  (
( z  e.  S  ->  (  ._|_  `  t ) ( le `  K
) z )  <->  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
9889, 94, 97ralxfrd 4612 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  ( A. z  e.  B  (
z  e.  S  -> 
(  ._|_  `  t )
( le `  K
) z )  <->  A. u  e.  B  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
9988, 98bitr4d 264 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  ( A. u  e.  B  (
(  ._|_  `  u )  e.  S  ->  u ( le `  K ) t )  <->  A. z  e.  B  ( z  e.  S  ->  (  ._|_  `  t ) ( le
`  K ) z ) ) )
10060ralrab 3188 . . . . . . . . . . 11  |-  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) t  <->  A. u  e.  B  ( (  ._|_  `  u
)  e.  S  ->  u ( le `  K ) t ) )
10157ralrab 3188 . . . . . . . . . . 11  |-  ( A. z  e.  { x  e.  B  |  x  e.  S }  (  ._|_  `  t ) ( le
`  K ) z  <->  A. z  e.  B  ( z  e.  S  ->  (  ._|_  `  t ) ( le `  K
) z ) )
10299, 100, 1013bitr4g 296 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) t  <->  A. z  e.  {
x  e.  B  |  x  e.  S } 
(  ._|_  `  t )
( le `  K
) z ) )
103 simplr 770 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  v  e.  B )
104 simpr 468 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  t  e.  B )
1056, 7, 23oplecon3b 32837 . . . . . . . . . . 11  |-  ( ( K  e.  OP  /\  v  e.  B  /\  t  e.  B )  ->  ( v ( le
`  K ) t  <-> 
(  ._|_  `  t )
( le `  K
) (  ._|_  `  v
) ) )
10663, 103, 104, 105syl3anc 1292 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  ( v
( le `  K
) t  <->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  v ) ) )
107102, 106imbi12d 327 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  ( ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) t  ->  v ( le `  K ) t )  <->  ( A. z  e.  { x  e.  B  |  x  e.  S }  (  ._|_  `  t
) ( le `  K ) z  -> 
(  ._|_  `  t )
( le `  K
) (  ._|_  `  v
) ) ) )
108107ralbidva 2828 . . . . . . . 8  |-  ( ( K  e.  HL  /\  v  e.  B )  ->  ( A. t  e.  B  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x
)  e.  S }
u ( le `  K ) t  -> 
v ( le `  K ) t )  <->  A. t  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S } 
(  ._|_  `  t )
( le `  K
) z  ->  (  ._|_  `  t ) ( le `  K ) (  ._|_  `  v ) ) ) )
10981, 108bitr4d 264 . . . . . . 7  |-  ( ( K  e.  HL  /\  v  e.  B )  ->  ( A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le
`  K ) z  ->  w ( le
`  K ) ( 
._|_  `  v ) )  <->  A. t  e.  B  ( A. u  e.  {
x  e.  B  | 
(  ._|_  `  x )  e.  S } u ( le `  K ) t  ->  v ( le `  K ) t ) ) )
11062, 109anbi12d 725 . . . . . 6  |-  ( ( K  e.  HL  /\  v  e.  B )  ->  ( ( A. z  e.  { x  e.  B  |  x  e.  S }  (  ._|_  `  v
) ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) (  ._|_  `  v ) ) )  <-> 
( A. u  e. 
{ x  e.  B  |  (  ._|_  `  x
)  e.  S }
u ( le `  K ) v  /\  A. t  e.  B  ( A. u  e.  {
x  e.  B  | 
(  ._|_  `  x )  e.  S } u ( le `  K ) t  ->  v ( le `  K ) t ) ) ) )
111110riotabidva 6286 . . . . 5  |-  ( K  e.  HL  ->  ( iota_ v  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S } 
(  ._|_  `  v )
( le `  K
) z  /\  A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  ->  w ( le `  K ) ( 
._|_  `  v ) ) ) )  =  (
iota_ v  e.  B  ( A. u  e.  {
x  e.  B  | 
(  ._|_  `  x )  e.  S } u ( le `  K ) v  /\  A. t  e.  B  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) t  ->  v ( le `  K ) t ) ) ) )
112 ssrab2 3500 . . . . . 6  |-  { x  e.  B  |  (  ._|_  `  x )  e.  S }  C_  B
113 glbcon.u . . . . . . 7  |-  U  =  ( lub `  K
)
114 biid 244 . . . . . . 7  |-  ( ( A. u  e.  {
x  e.  B  | 
(  ._|_  `  x )  e.  S } u ( le `  K ) v  /\  A. t  e.  B  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) t  ->  v ( le `  K ) t ) )  <->  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) v  /\  A. t  e.  B  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) t  ->  v ( le `  K ) t ) ) )
115 simpl 464 . . . . . . 7  |-  ( ( K  e.  HL  /\  { x  e.  B  | 
(  ._|_  `  x )  e.  S }  C_  B
)  ->  K  e.  HL )
116 simpr 468 . . . . . . 7  |-  ( ( K  e.  HL  /\  { x  e.  B  | 
(  ._|_  `  x )  e.  S }  C_  B
)  ->  { x  e.  B  |  (  ._|_  `  x )  e.  S }  C_  B
)
1176, 7, 113, 114, 115, 116lubval 16308 . . . . . 6  |-  ( ( K  e.  HL  /\  { x  e.  B  | 
(  ._|_  `  x )  e.  S }  C_  B
)  ->  ( U `  { x  e.  B  |  (  ._|_  `  x
)  e.  S }
)  =  ( iota_ v  e.  B  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) v  /\  A. t  e.  B  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) t  ->  v ( le `  K ) t ) ) ) )
118112, 117mpan2 685 . . . . 5  |-  ( K  e.  HL  ->  ( U `  { x  e.  B  |  (  ._|_  `  x )  e.  S } )  =  ( iota_ v  e.  B  ( A. u  e.  {
x  e.  B  | 
(  ._|_  `  x )  e.  S } u ( le `  K ) v  /\  A. t  e.  B  ( A. u  e.  { x  e.  B  |  (  ._|_  `  x )  e.  S } u ( le `  K ) t  ->  v ( le `  K ) t ) ) ) )
119111, 118eqtr4d 2508 . . . 4  |-  ( K  e.  HL  ->  ( iota_ v  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S } 
(  ._|_  `  v )
( le `  K
) z  /\  A. w  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S } w ( le `  K ) z  ->  w ( le `  K ) ( 
._|_  `  v ) ) ) )  =  ( U `  { x  e.  B  |  (  ._|_  `  x )  e.  S } ) )
120119fveq2d 5883 . . 3  |-  ( K  e.  HL  ->  (  ._|_  `  ( iota_ v  e.  B  ( A. z  e.  { x  e.  B  |  x  e.  S }  (  ._|_  `  v
) ( le `  K ) z  /\  A. w  e.  B  ( A. z  e.  {
x  e.  B  |  x  e.  S }
w ( le `  K ) z  ->  w ( le `  K ) (  ._|_  `  v ) ) ) ) )  =  ( 
._|_  `  ( U `  { x  e.  B  |  (  ._|_  `  x
)  e.  S }
) ) )
12113, 31, 1203eqtrd 2509 . 2  |-  ( K  e.  HL  ->  ( G `  { x  e.  B  |  x  e.  S } )  =  (  ._|_  `  ( U `
 { x  e.  B  |  (  ._|_  `  x )  e.  S } ) ) )
1225, 121sylan9eqr 2527 1  |-  ( ( K  e.  HL  /\  S  C_  B )  -> 
( G `  S
)  =  (  ._|_  `  ( U `  {
x  e.  B  | 
(  ._|_  `  x )  e.  S } ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452    e. wcel 1904   A.wral 2756   E.wrex 2757   E!wreu 2758   {crab 2760   _Vcvv 3031    i^i cin 3389    C_ wss 3390   class class class wbr 4395   ` cfv 5589   iota_crio 6269   Basecbs 15199   lecple 15275   occoc 15276   lubclub 16265   glbcglb 16266   CLatccla 16431   OPcops 32809   HLchlt 32987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-riotaBAD 32589
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-undef 7038  df-lub 16298  df-glb 16299  df-clat 16432  df-oposet 32813  df-ol 32815  df-oml 32816  df-hlat 32988
This theorem is referenced by:  glbconxN  33014
  Copyright terms: Public domain W3C validator