Theorem ishlatiN 39611

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 39609	. 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 1541   ∈ wcel 2113   ≠ wne 2932  ∀wral 3051  ∃wrex 3060   class class class wbr 5098  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  lecple 17184  ltcplt 18231  joincjn 18234  0.cp0 18344  1.cp1 18345  CLatccla 18421  OMLcoml 39431  Atomscatm 39519  AtLatcal 39520  HLchlt 39606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-cvlat 39578  df-hlat 39607

This theorem is referenced by: (None)