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

Theorem op1cl 29910
Description: An orthoposet has a unit element. (helch 22738 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 2435 . . 3  |-  ( le
`  K )  =  ( le `  K
)
3 eqid 2435 . . 3  |-  ( oc
`  K )  =  ( oc `  K
)
4 eqid 2435 . . 3  |-  ( join `  K )  =  (
join `  K )
5 eqid 2435 . . 3  |-  ( meet `  K )  =  (
meet `  K )
6 eqid 2435 . . 3  |-  ( 0.
`  K )  =  ( 0. `  K
)
7 op1cl.u . . 3  |-  .1.  =  ( 1. `  K )
81, 2, 3, 4, 5, 6, 7isopos 29905 . 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 1652    e. wcel 1725   A.wral 2697   class class class wbr 4204   ` cfv 5446  (class class class)co 6073   Basecbs 13461   lecple 13528   occoc 13529   Posetcpo 14389   joincjn 14393   meetcmee 14394   0.cp0 14458   1.cp1 14459   OPcops 29897
This theorem is referenced by:  ople1  29916  op1le  29917  glb0N  29918  opoc1  29927  opoc0  29928  olm11  29952  olm12  29953  ncvr1  29997  hlhgt2  30113  hl0lt1N  30114  hl2at  30129  athgt  30180  1cvrco  30196  1cvrjat  30199  pmap1N  30491  pol1N  30634  lhp2lt  30725  lhpexnle  30730  dih1  32011  dih1rn  32012  dih1cnv  32013  dihglb2  32067  dochocss  32091  dihjatc  32142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-nul 4330
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-oposet 29901
  Copyright terms: Public domain W3C validator