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

Theorem op0cl 29447
Description: An orthoposet has a zero element. (h0elch 21836 analog.) (Contributed by NM, 12-Oct-2011.)
Hypotheses
Ref Expression
op0cl.b  |-  B  =  ( Base `  K
)
op0cl.z  |-  .0.  =  ( 0. `  K )
Assertion
Ref Expression
op0cl  |-  ( K  e.  OP  ->  .0.  e.  B )

Proof of Theorem op0cl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 op0cl.b . . 3  |-  B  =  ( Base `  K
)
2 eqid 2285 . . 3  |-  ( le
`  K )  =  ( le `  K
)
3 eqid 2285 . . 3  |-  ( oc
`  K )  =  ( oc `  K
)
4 eqid 2285 . . 3  |-  ( join `  K )  =  (
join `  K )
5 eqid 2285 . . 3  |-  ( meet `  K )  =  (
meet `  K )
6 op0cl.z . . 3  |-  .0.  =  ( 0. `  K )
7 eqid 2285 . . 3  |-  ( 1.
`  K )  =  ( 1. `  K
)
81, 2, 3, 4, 5, 6, 7isopos 29443 . 2  |-  ( K  e.  OP  <->  ( ( K  e.  Poset  /\  .0.  e.  B  /\  ( 1. `  K )  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. `  K
)  /\  ( x
( meet `  K )
( ( oc `  K ) `  x
) )  =  .0.  ) ) )
9 simpl2 959 . 2  |-  ( ( ( K  e.  Poset  /\  .0.  e.  B  /\  ( 1. `  K )  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. `  K
)  /\  ( x
( meet `  K )
( ( oc `  K ) `  x
) )  =  .0.  ) )  ->  .0.  e.  B )
108, 9sylbi 187 1  |-  ( K  e.  OP  ->  .0.  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1625    e. wcel 1686   A.wral 2545   class class class wbr 4025   ` cfv 5257  (class class class)co 5860   Basecbs 13150   lecple 13217   occoc 13218   Posetcpo 14076   joincjn 14080   meetcmee 14081   0.cp0 14145   1.cp1 14146   OPcops 29435
This theorem is referenced by:  op0le  29449  ople0  29450  lub0N  29452  opltn0  29453  opoc1  29465  opoc0  29466  olj01  29488  olj02  29489  olm01  29499  olm02  29500  0ltat  29554  leatb  29555  hlhgt2  29651  hl0lt1N  29652  hl2at  29667  atcvr0eq  29688  lnnat  29689  atle  29698  athgt  29718  1cvratex  29735  ps-2  29740  dalemcea  29922  pmapeq0  30028  2atm2atN  30047  lhp0lt  30265  lhpn0  30266  ltrnatb  30399  ltrnmw  30413  cdleme3c  30492  cdleme7e  30509  dia0eldmN  31303  dia2dimlem2  31328  dia2dimlem3  31329  dib0  31427  dih0  31543  dih0bN  31544  dih0rn  31547  dihlspsnssN  31595  dihlspsnat  31596  dihatexv  31601
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-nul 4151
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-iota 5221  df-fv 5265  df-ov 5863  df-oposet 29439
  Copyright terms: Public domain W3C validator