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

Theorem ishlatiN 29363
Description: Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
ishlati.1  |-  K  e. 
OML
ishlati.2  |-  K  e. 
CLat
ishlati.3  |-  K  e. 
AtLat
ishlati.b  |-  B  =  ( Base `  K
)
ishlati.l  |-  .<_  =  ( le `  K )
ishlati.s  |-  .<  =  ( lt `  K )
ishlati.j  |-  .\/  =  ( join `  K )
ishlati.z  |-  .0.  =  ( 0. `  K )
ishlati.u  |-  .1.  =  ( 1. `  K )
ishlati.a  |-  A  =  ( Atoms `  K )
ishlati.9  |-  A. x  e.  A  A. y  e.  A  ( (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )
ishlati.10  |-  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) )
Assertion
Ref Expression
ishlatiN  |-  K  e.  HL
Distinct variable groups:    x, y,
z, A    x, B, y, z    x, K, y, z
Allowed substitution hints:    .< ( x, y,
z)    .1. ( x, y, z)    .\/ ( x, y, z)    .<_ ( x, y, z)    .0. ( x, y, z)

Proof of Theorem ishlatiN
StepHypRef Expression
1 ishlati.1 . . 3  |-  K  e. 
OML
2 ishlati.2 . . 3  |-  K  e. 
CLat
3 ishlati.3 . . 3  |-  K  e. 
AtLat
41, 2, 33pm3.2i 1130 . 2  |-  ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)
5 ishlati.9 . . 3  |-  A. x  e.  A  A. y  e.  A  ( (
x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )
6 ishlati.10 . . 3  |-  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0.  .<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) )
75, 6pm3.2i 441 . 2  |-  ( A. x  e.  A  A. y  e.  A  (
( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0. 
.<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) )
8 ishlati.b . . 3  |-  B  =  ( Base `  K
)
9 ishlati.l . . 3  |-  .<_  =  ( le `  K )
10 ishlati.s . . 3  |-  .<  =  ( lt `  K )
11 ishlati.j . . 3  |-  .\/  =  ( join `  K )
12 ishlati.z . . 3  |-  .0.  =  ( 0. `  K )
13 ishlati.u . . 3  |-  .1.  =  ( 1. `  K )
14 ishlati.a . . 3  |-  A  =  ( Atoms `  K )
158, 9, 10, 11, 12, 13, 14ishlat2 29361 . 2  |-  ( K  e.  HL  <->  ( ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  AtLat
)  /\  ( A. x  e.  A  A. y  e.  A  (
( x  =/=  y  ->  E. z  e.  A  ( z  =/=  x  /\  z  =/=  y  /\  z  .<_  ( x 
.\/  y ) ) )  /\  A. z  e.  B  ( ( -.  x  .<_  z  /\  x  .<_  ( z  .\/  y ) )  -> 
y  .<_  ( z  .\/  x ) ) )  /\  E. x  e.  B  E. y  e.  B  E. z  e.  B  ( (  .0. 
.<  x  /\  x  .<  y )  /\  (
y  .<  z  /\  z  .<  .1.  ) ) ) ) )
164, 7, 15mpbir2an 886 1  |-  K  e.  HL
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1633    e. wcel 1701    =/= wne 2479   A.wral 2577   E.wrex 2578   class class class wbr 4060   ` cfv 5292  (class class class)co 5900   Basecbs 13195   lecple 13262   ltcplt 14124   joincjn 14127   0.cp0 14192   1.cp1 14193   CLatccla 14262   OMLcoml 29183   Atomscatm 29271   AtLatcal 29272   HLchlt 29358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-cvlat 29330  df-hlat 29359
  Copyright terms: Public domain W3C validator