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

Theorem isomliN 36367
Description: Properties that determine an orthomodular lattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
isomli.0 𝐾 ∈ OL
isomli.b 𝐵 = (Base‘𝐾)
isomli.l = (le‘𝐾)
isomli.j = (join‘𝐾)
isomli.m = (meet‘𝐾)
isomli.o = (oc‘𝐾)
isomli.7 ((𝑥𝐵𝑦𝐵) → (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥)))))
Assertion
Ref Expression
isomliN 𝐾 ∈ OML
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐾,𝑦
Allowed substitution hints:   (𝑥,𝑦)   (𝑥,𝑦)   (𝑥,𝑦)   (𝑥,𝑦)

Proof of Theorem isomliN
StepHypRef Expression
1 isomli.0 . 2 𝐾 ∈ OL
2 isomli.7 . . 3 ((𝑥𝐵𝑦𝐵) → (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥)))))
32rgen2 3201 . 2 𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥))))
4 isomli.b . . 3 𝐵 = (Base‘𝐾)
5 isomli.l . . 3 = (le‘𝐾)
6 isomli.j . . 3 = (join‘𝐾)
7 isomli.m . . 3 = (meet‘𝐾)
8 isomli.o . . 3 = (oc‘𝐾)
94, 5, 6, 7, 8isoml 36366 . 2 (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥))))))
101, 3, 9mpbir2an 709 1 𝐾 ∈ OML
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1531  wcel 2108  wral 3136   class class class wbr 5057  cfv 6348  (class class class)co 7148  Basecbs 16475  lecple 16564  occoc 16565  joincjn 17546  meetcmee 17547  OLcol 36302  OMLcoml 36303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-oml 36307
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator