Theorem chle0 11992

Description: No Hilbert lattice element is smaller than zero.

Assertion

Ref	Expression
chle0	|- (A e. CH -> (A C_ 0H <-> A = 0H))

Proof of Theorem chle0

Step	Hyp	Ref	Expression
1		chsh 11721	. 2 |- (A e. CH -> A e. SH)
2		shle0 11991	. 2 |- (A e. SH -> (A C_ 0H <-> A = 0H))
3	1, 2	syl 13	1 |- (A e. CH -> (A C_ 0H <-> A = 0H))

Syntax hints:   -> wi 3   <-> wb 231   = wceq 1615   e. wcel 1617   C_ wss 2859  SHcsh 11425  CHcch 11426  0Hc0h 11432

This theorem is referenced by:  chle0i 12000  chssoc 12044  hatomistici 12923  atcvat4i 12958

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-hilex 11497

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166  df-ral 2389  df-v 2571  df-in 2866  df-ss 2868  df-sn 3274  df-sh 11703  df-ch 11717  df-ch0 11750

Copyright terms: Public domain