Theorem ishlatiN 39341

Description: Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ishlati.1	⊢ 𝐾 ∈ OML
ishlati.2	⊢ 𝐾 ∈ CLat
ishlati.3	⊢ 𝐾 ∈ AtLat
ishlati.b	⊢ 𝐵 = (Base‘𝐾)
ishlati.l	⊢ ≤ = (le‘𝐾)
ishlati.s	⊢ < = (lt‘𝐾)
ishlati.j	⊢ ∨ = (join‘𝐾)
ishlati.z	⊢ 0 = (0.‘𝐾)
ishlati.u	⊢ 1 = (1.‘𝐾)
ishlati.a	⊢ 𝐴 = (Atoms‘𝐾)
ishlati.9	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)))
ishlati.10	⊢ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))

Assertion

Ref	Expression
ishlatiN	⊢ 𝐾 ∈ HL

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐾,𝑦,𝑧

Allowed substitution hints:   < (𝑥,𝑦,𝑧)   1 (𝑥,𝑦,𝑧)   ∨ (𝑥,𝑦,𝑧)   ≤ (𝑥,𝑦,𝑧)   0 (𝑥,𝑦,𝑧)

Proof of Theorem ishlatiN

Step	Hyp	Ref	Expression
1		ishlati.1	. . 3 ⊢ 𝐾 ∈ OML
2		ishlati.2	. . 3 ⊢ 𝐾 ∈ CLat
3		ishlati.3	. . 3 ⊢ 𝐾 ∈ AtLat
4	1, 2, 3	3pm3.2i 1340	. 2 ⊢ (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat)
5		ishlati.9	. . 3 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)))
6		ishlati.10	. . 3 ⊢ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))
7	5, 6	pm3.2i 470	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))
8		ishlati.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
9		ishlati.l	. . 3 ⊢ ≤ = (le‘𝐾)
10		ishlati.s	. . 3 ⊢ < = (lt‘𝐾)
11		ishlati.j	. . 3 ⊢ ∨ = (join‘𝐾)
12		ishlati.z	. . 3 ⊢ 0 = (0.‘𝐾)
13		ishlati.u	. . 3 ⊢ 1 = (1.‘𝐾)
14		ishlati.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
15	8, 9, 10, 11, 12, 13, 14	ishlat2 39339	. 2 ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
16	4, 7, 15	mpbir2an 711	1 ⊢ 𝐾 ∈ HL

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053   class class class wbr 5102  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  lecple 17203  ltcplt 18249  joincjn 18252  0.cp0 18362  1.cp1 18363  CLatccla 18439  OMLcoml 39161  Atomscatm 39249  AtLatcal 39250  HLchlt 39336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-cvlat 39308  df-hlat 39337

This theorem is referenced by: (None)