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

Theorem op1cl 29300
Description: An orthoposet has a unit element. (helch 22594 analog.) (Contributed by NM, 22-Oct-2011.)
Hypotheses
Ref Expression
op1cl.b  |-  B  =  ( Base `  K
)
op1cl.u  |-  .1.  =  ( 1. `  K )
Assertion
Ref Expression
op1cl  |-  ( K  e.  OP  ->  .1.  e.  B )

Proof of Theorem op1cl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 op1cl.b . . 3  |-  B  =  ( Base `  K
)
2 eqid 2387 . . 3  |-  ( le
`  K )  =  ( le `  K
)
3 eqid 2387 . . 3  |-  ( oc
`  K )  =  ( oc `  K
)
4 eqid 2387 . . 3  |-  ( join `  K )  =  (
join `  K )
5 eqid 2387 . . 3  |-  ( meet `  K )  =  (
meet `  K )
6 eqid 2387 . . 3  |-  ( 0.
`  K )  =  ( 0. `  K
)
7 op1cl.u . . 3  |-  .1.  =  ( 1. `  K )
81, 2, 3, 4, 5, 6, 7isopos 29295 . 2  |-  ( K  e.  OP  <->  ( ( K  e.  Poset  /\  ( 0. `  K )  e.  B  /\  .1.  e.  B )  /\  A. x  e.  B  A. y  e.  B  (
( ( ( oc
`  K ) `  x )  e.  B  /\  ( ( oc `  K ) `  (
( oc `  K
) `  x )
)  =  x  /\  ( x ( le
`  K ) y  ->  ( ( oc
`  K ) `  y ) ( le
`  K ) ( ( oc `  K
) `  x )
) )  /\  (
x ( join `  K
) ( ( oc
`  K ) `  x ) )  =  .1.  /\  ( x ( meet `  K
) ( ( oc
`  K ) `  x ) )  =  ( 0. `  K
) ) ) )
9 simpl3 962 . 2  |-  ( ( ( K  e.  Poset  /\  ( 0. `  K
)  e.  B  /\  .1.  e.  B )  /\  A. x  e.  B  A. y  e.  B  (
( ( ( oc
`  K ) `  x )  e.  B  /\  ( ( oc `  K ) `  (
( oc `  K
) `  x )
)  =  x  /\  ( x ( le
`  K ) y  ->  ( ( oc
`  K ) `  y ) ( le
`  K ) ( ( oc `  K
) `  x )
) )  /\  (
x ( join `  K
) ( ( oc
`  K ) `  x ) )  =  .1.  /\  ( x ( meet `  K
) ( ( oc
`  K ) `  x ) )  =  ( 0. `  K
) ) )  ->  .1.  e.  B )
108, 9sylbi 188 1  |-  ( K  e.  OP  ->  .1.  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1717   A.wral 2649   class class class wbr 4153   ` cfv 5394  (class class class)co 6020   Basecbs 13396   lecple 13463   occoc 13464   Posetcpo 14324   joincjn 14328   meetcmee 14329   0.cp0 14393   1.cp1 14394   OPcops 29287
This theorem is referenced by:  ople1  29306  op1le  29307  glb0N  29308  opoc1  29317  opoc0  29318  olm11  29342  olm12  29343  ncvr1  29387  hlhgt2  29503  hl0lt1N  29504  hl2at  29519  athgt  29570  1cvrco  29586  1cvrjat  29589  pmap1N  29881  pol1N  30024  lhp2lt  30115  lhpexnle  30120  dih1  31401  dih1rn  31402  dih1cnv  31403  dihglb2  31457  dochocss  31481  dihjatc  31532
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-nul 4279
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023  df-oposet 29291
  Copyright terms: Public domain W3C validator