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

Theorem glbconN 33360
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 3445 . . . 4  |-  ( B  i^i  S )  =  { x  e.  B  |  x  e.  S }
2 sseqin2 3678 . . . . 5  |-  ( S 
C_  B  <->  ( B  i^i  S )  =  S )
32biimpi 194 . . . 4  |-  ( S 
C_  B  ->  ( B  i^i  S )  =  S )
41, 3syl5reqr 2510 . . 3  |-  ( S 
C_  B  ->  S  =  { x  e.  B  |  x  e.  S } )
54fveq2d 5804 . 2  |-  ( S 
C_  B  ->  ( G `  S )  =  ( G `  { x  e.  B  |  x  e.  S } ) )
6 glbcon.b . . . 4  |-  B  =  ( Base `  K
)
7 eqid 2454 . . . 4  |-  ( le
`  K )  =  ( le `  K
)
8 glbcon.g . . . 4  |-  G  =  ( glb `  K
)
9 biid 236 . . . 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 3546 . . . . 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 15287 . . 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 33346 . . . 4  |-  ( K  e.  HL  ->  K  e.  OP )
15 hlclat 33342 . . . . . . 7  |-  ( K  e.  HL  ->  K  e.  CLat )
166, 8clatglbcl 15404 . . . . . . 7  |-  ( ( K  e.  CLat  /\  {
x  e.  B  |  x  e.  S }  C_  B )  ->  ( G `  { x  e.  B  |  x  e.  S } )  e.  B )
1715, 11, 16sylancl 662 . . . . . 6  |-  ( K  e.  HL  ->  ( G `  { x  e.  B  |  x  e.  S } )  e.  B )
1813, 17eqeltrrd 2543 . . . . 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 5810 . . . . . . 7  |-  ( Base `  K )  e.  _V
206, 19eqeltri 2538 . . . . . 6  |-  B  e. 
_V
2120riotaclbBAD 32945 . . . . 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 212 . . . 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 4404 . . . . . . 7  |-  ( y  =  (  ._|_  `  v
)  ->  ( y
( le `  K
) z  <->  (  ._|_  `  v ) ( le
`  K ) z ) )
2524ralbidv 2846 . . . . . 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 4405 . . . . . . . 8  |-  ( y  =  (  ._|_  `  v
)  ->  ( w
( le `  K
) y  <->  w ( le `  K ) ( 
._|_  `  v ) ) )
2726imbi2d 316 . . . . . . 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 2846 . . . . . 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 710 . . . . 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 33193 . . . 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 661 . . 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 725 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  K  e.  OP )
336, 23opoccl 33178 . . . . . . . . . . 11  |-  ( ( K  e.  OP  /\  u  e.  B )  ->  (  ._|_  `  u )  e.  B )
3432, 33sylancom 667 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  (  ._|_  `  u )  e.  B
)
3514ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  K  e.  OP )
366, 23opoccl 33178 . . . . . . . . . . . 12  |-  ( ( K  e.  OP  /\  z  e.  B )  ->  (  ._|_  `  z )  e.  B )
3735, 36sylancom 667 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  (  ._|_  `  z )  e.  B
)
386, 23opococ 33179 . . . . . . . . . . . . 13  |-  ( ( K  e.  OP  /\  z  e.  B )  ->  (  ._|_  `  (  ._|_  `  z ) )  =  z )
3935, 38sylancom 667 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  (  ._|_  `  (  ._|_  `  z ) )  =  z )
4039eqcomd 2462 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  z  =  (  ._|_  `  (  ._|_  `  z ) ) )
41 fveq2 5800 . . . . . . . . . . . . 13  |-  ( u  =  (  ._|_  `  z
)  ->  (  ._|_  `  u )  =  ( 
._|_  `  (  ._|_  `  z
) ) )
4241eqeq2d 2468 . . . . . . . . . . . 12  |-  ( u  =  (  ._|_  `  z
)  ->  ( z  =  (  ._|_  `  u
)  <->  z  =  ( 
._|_  `  (  ._|_  `  z
) ) ) )
4342rspcev 3179 . . . . . . . . . . 11  |-  ( ( (  ._|_  `  z )  e.  B  /\  z  =  (  ._|_  `  (  ._|_  `  z ) ) )  ->  E. u  e.  B  z  =  (  ._|_  `  u )
)
4437, 40, 43syl2anc 661 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  z  e.  B
)  ->  E. u  e.  B  z  =  (  ._|_  `  u )
)
45 eleq1 2526 . . . . . . . . . . . 12  |-  ( z  =  (  ._|_  `  u
)  ->  ( z  e.  S  <->  (  ._|_  `  u
)  e.  S ) )
46 breq2 4405 . . . . . . . . . . . 12  |-  ( z  =  (  ._|_  `  u
)  ->  ( (  ._|_  `  v ) ( le `  K ) z  <->  (  ._|_  `  v
) ( le `  K ) (  ._|_  `  u ) ) )
4745, 46imbi12d 320 . . . . . . . . . . 11  |-  ( z  =  (  ._|_  `  u
)  ->  ( (
z  e.  S  -> 
(  ._|_  `  v )
( le `  K
) z )  <->  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  v ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
4847adantl 466 . . . . . . . . . 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 4615 . . . . . . . . 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 461 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  u  e.  B )
51 simplr 754 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  v  e.  B )
526, 7, 23oplecon3b 33184 . . . . . . . . . . . 12  |-  ( ( K  e.  OP  /\  u  e.  B  /\  v  e.  B )  ->  ( u ( le
`  K ) v  <-> 
(  ._|_  `  v )
( le `  K
) (  ._|_  `  u
) ) )
5332, 50, 51, 52syl3anc 1219 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  u  e.  B
)  ->  ( u
( le `  K
) v  <->  (  ._|_  `  v ) ( le
`  K ) ( 
._|_  `  u ) ) )
5453imbi2d 316 . . . . . . . . . 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 2844 . . . . . . . . 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 256 . . . . . . . 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 2526 . . . . . . . . 9  |-  ( x  =  z  ->  (
x  e.  S  <->  z  e.  S ) )
5857ralrab 3228 . . . . . . . 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 5800 . . . . . . . . . 10  |-  ( x  =  u  ->  (  ._|_  `  x )  =  (  ._|_  `  u ) )
6059eleq1d 2523 . . . . . . . . 9  |-  ( x  =  u  ->  (
(  ._|_  `  x )  e.  S  <->  (  ._|_  `  u
)  e.  S ) )
6160ralrab 3228 . . . . . . . 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 288 . . . . . . 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 725 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  K  e.  OP )
646, 23opoccl 33178 . . . . . . . . . 10  |-  ( ( K  e.  OP  /\  t  e.  B )  ->  (  ._|_  `  t )  e.  B )
6563, 64sylancom 667 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  (  ._|_  `  t )  e.  B
)
6614ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  K  e.  OP )
676, 23opoccl 33178 . . . . . . . . . . 11  |-  ( ( K  e.  OP  /\  w  e.  B )  ->  (  ._|_  `  w )  e.  B )
6866, 67sylancom 667 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  (  ._|_  `  w )  e.  B
)
696, 23opococ 33179 . . . . . . . . . . . 12  |-  ( ( K  e.  OP  /\  w  e.  B )  ->  (  ._|_  `  (  ._|_  `  w ) )  =  w )
7066, 69sylancom 667 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  (  ._|_  `  (  ._|_  `  w ) )  =  w )
7170eqcomd 2462 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  w  =  (  ._|_  `  (  ._|_  `  w ) ) )
72 fveq2 5800 . . . . . . . . . . . 12  |-  ( t  =  (  ._|_  `  w
)  ->  (  ._|_  `  t )  =  ( 
._|_  `  (  ._|_  `  w
) ) )
7372eqeq2d 2468 . . . . . . . . . . 11  |-  ( t  =  (  ._|_  `  w
)  ->  ( w  =  (  ._|_  `  t
)  <->  w  =  (  ._|_  `  (  ._|_  `  w
) ) ) )
7473rspcev 3179 . . . . . . . . . 10  |-  ( ( (  ._|_  `  w )  e.  B  /\  w  =  (  ._|_  `  (  ._|_  `  w ) ) )  ->  E. t  e.  B  w  =  (  ._|_  `  t )
)
7568, 71, 74syl2anc 661 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  w  e.  B
)  ->  E. t  e.  B  w  =  (  ._|_  `  t )
)
76 breq1 4404 . . . . . . . . . . . 12  |-  ( w  =  (  ._|_  `  t
)  ->  ( w
( le `  K
) z  <->  (  ._|_  `  t ) ( le
`  K ) z ) )
7776ralbidv 2846 . . . . . . . . . . 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 4404 . . . . . . . . . . 11  |-  ( w  =  (  ._|_  `  t
)  ->  ( w
( le `  K
) (  ._|_  `  v
)  <->  (  ._|_  `  t
) ( le `  K ) (  ._|_  `  v ) ) )
7977, 78imbi12d 320 . . . . . . . . . 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 466 . . . . . . . . 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 4615 . . . . . . . 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 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  K  e.  OP )
83 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  u  e.  B )
84 simplr 754 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  t  e.  B )
856, 7, 23oplecon3b 33184 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  OP  /\  u  e.  B  /\  t  e.  B )  ->  ( u ( le
`  K ) t  <-> 
(  ._|_  `  t )
( le `  K
) (  ._|_  `  u
) ) )
8682, 83, 84, 85syl3anc 1219 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  (
u ( le `  K ) t  <->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  u ) ) )
8786imbi2d 316 . . . . . . . . . . . . 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 2844 . . . . . . . . . . . 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 667 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  u  e.  B )  ->  (  ._|_  `  u )  e.  B )
9014ad3antrrr 729 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  K  e.  OP )
9190, 36sylancom 667 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  (  ._|_  `  z )  e.  B )
9290, 38sylancom 667 . . . . . . . . . . . . . . 15  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  (  ._|_  `  (  ._|_  `  z
) )  =  z )
9392eqcomd 2462 . . . . . . . . . . . . . 14  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  z  =  (  ._|_  `  (  ._|_  `  z ) ) )
9491, 93, 43syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B )  /\  z  e.  B )  ->  E. u  e.  B  z  =  (  ._|_  `  u )
)
95 breq2 4405 . . . . . . . . . . . . . . 15  |-  ( z  =  (  ._|_  `  u
)  ->  ( (  ._|_  `  t ) ( le `  K ) z  <->  (  ._|_  `  t
) ( le `  K ) (  ._|_  `  u ) ) )
9645, 95imbi12d 320 . . . . . . . . . . . . . 14  |-  ( z  =  (  ._|_  `  u
)  ->  ( (
z  e.  S  -> 
(  ._|_  `  t )
( le `  K
) z )  <->  ( (  ._|_  `  u )  e.  S  ->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  u ) ) ) )
9796adantl 466 . . . . . . . . . . . . 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 4615 . . . . . . . . . . . 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 256 . . . . . . . . . . 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 3228 . . . . . . . . . . 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 3228 . . . . . . . . . . 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 288 . . . . . . . . . 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 754 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  v  e.  B )
104 simpr 461 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  t  e.  B )
1056, 7, 23oplecon3b 33184 . . . . . . . . . . 11  |-  ( ( K  e.  OP  /\  v  e.  B  /\  t  e.  B )  ->  ( v ( le
`  K ) t  <-> 
(  ._|_  `  t )
( le `  K
) (  ._|_  `  v
) ) )
10663, 103, 104, 105syl3anc 1219 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  v  e.  B )  /\  t  e.  B
)  ->  ( v
( le `  K
) t  <->  (  ._|_  `  t ) ( le
`  K ) ( 
._|_  `  v ) ) )
107102, 106imbi12d 320 . . . . . . . . 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 2844 . . . . . . . 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 256 . . . . . . 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 710 . . . . . 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 6179 . . . . 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 3546 . . . . . 6  |-  { x  e.  B  |  (  ._|_  `  x )  e.  S }  C_  B
113 glbcon.u . . . . . . 7  |-  U  =  ( lub `  K
)
114 biid 236 . . . . . . 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 457 . . . . . . 7  |-  ( ( K  e.  HL  /\  { x  e.  B  | 
(  ._|_  `  x )  e.  S }  C_  B
)  ->  K  e.  HL )
116 simpr 461 . . . . . . 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 15274 . . . . . 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 671 . . . . 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 2498 . . . 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 5804 . . 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 2499 . 2  |-  ( K  e.  HL  ->  ( G `  { x  e.  B  |  x  e.  S } )  =  (  ._|_  `  ( U `
 { x  e.  B  |  (  ._|_  `  x )  e.  S } ) ) )
1225, 121sylan9eqr 2517 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 184    /\ wa 369    = wceq 1370    e. wcel 1758   A.wral 2799   E.wrex 2800   E!wreu 2801   {crab 2803   _Vcvv 3078    i^i cin 3436    C_ wss 3437   class class class wbr 4401   ` cfv 5527   iota_crio 6161   Basecbs 14293   lecple 14365   occoc 14366   lubclub 15232   glbcglb 15233   CLatccla 15397   OPcops 33156   HLchlt 33334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4512  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-riotaBAD 32943
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-id 4745  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-undef 6903  df-lub 15264  df-glb 15265  df-clat 15398  df-oposet 33160  df-ol 33162  df-oml 33163  df-hlat 33335
This theorem is referenced by:  glbconxN  33361
  Copyright terms: Public domain W3C validator