Theorem isolat 17868

Description: The predicate "is an ortholattice."

Assertion

Ref	Expression
isolat	|- (K e. OL <-> (K e. Lat /\ K e. OP))

Proof of Theorem isolat

Step	Hyp	Ref	Expression
1		df-ol 17835	. . 3 |- OL = (Lat i^i OP)
2	1	eleq2i 2237	. 2 |- (K e. OL <-> K e. (Lat i^i OP))
3		elin 3031	. 2 |- (K e. (Lat i^i OP) <-> (K e. Lat /\ K e. OP))
4	2, 3	bitri 306	1 |- (K e. OL <-> (K e. Lat /\ K e. OP))

Syntax hints:   <-> wb 231   /\ wa 433   e. wcel 1617   i^i cin 2858  Latclat 9751  OPcops 17828  OLcol 17830

This theorem is referenced by:  ollat 17869  olop 17870  isolati 17872

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

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-v 2571  df-in 2866  df-ol 17835

Copyright terms: Public domain