Theorem ishlat2 37346

Description: The predicate "is a Hilbert lattice". Here we replace 𝐾 ∈ CvLat with the weaker 𝐾 ∈ AtLat and show the exchange property explicitly. (Contributed by NM, 5-Nov-2012.)

Hypotheses

Ref	Expression
ishlat.b	⊢ 𝐵 = (Base‘𝐾)
ishlat.l	⊢ ≤ = (le‘𝐾)
ishlat.s	⊢ < = (lt‘𝐾)
ishlat.j	⊢ ∨ = (join‘𝐾)
ishlat.z	⊢ 0 = (0.‘𝐾)
ishlat.u	⊢ 1 = (1.‘𝐾)
ishlat.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
ishlat2	⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))

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

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

Proof of Theorem ishlat2

Step	Hyp	Ref	Expression
1		ishlat.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		ishlat.l	. . 3 ⊢ ≤ = (le‘𝐾)
3		ishlat.s	. . 3 ⊢ < = (lt‘𝐾)
4		ishlat.j	. . 3 ⊢ ∨ = (join‘𝐾)
5		ishlat.z	. . 3 ⊢ 0 = (0.‘𝐾)
6		ishlat.u	. . 3 ⊢ 1 = (1.‘𝐾)
7		ishlat.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	ishlat1 37345	. 2 ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
9	1, 2, 4, 7	iscvlat 37316	. . . . 5 ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
10	9	3anbi3i 1157	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ↔ (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ (𝐾 ∈ AtLat ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)))))
11		anass 468	. . . . 5 ⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ AtLat) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ (𝐾 ∈ AtLat ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)))))
12		df-3an 1087	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ AtLat))
13	12	anbi1i 623	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ↔ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ AtLat) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
14		df-3an 1087	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ (𝐾 ∈ AtLat ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)))) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ (𝐾 ∈ AtLat ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)))))
15	11, 13, 14	3bitr4ri 303	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ (𝐾 ∈ AtLat ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)))) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
16	10, 15	bitri 274	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
17	16	anbi1i 623	. 2 ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) ↔ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
18		anass 468	. . 3 ⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))))
19		anass 468	. . . . 5 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
20		ancom 460	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
21		r19.26-2 3097	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
22	20, 21	bitr4i 277	. . . . . 6 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))))
23	22	anbi1i 623	. . . . 5 ⊢ (((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))
24	19, 23	bitr3i 276	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))
25	24	anbi2i 622	. . 3 ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
26	18, 25	bitri 274	. 2 ⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
27	8, 17, 26	3bitri 296	1 ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109   ≠ wne 2944  ∀wral 3065  ∃wrex 3066   class class class wbr 5078  ‘cfv 6430  (class class class)co 7268  Basecbs 16893  lecple 16950  ltcplt 18007  joincjn 18010  0.cp0 18122  1.cp1 18123  CLatccla 18197  OMLcoml 37168  Atomscatm 37256  AtLatcal 37257  CvLatclc 37258  HLchlt 37343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271  df-cvlat 37315  df-hlat 37344

This theorem is referenced by:  ishlatiN  37348  hlsuprexch  37374  hlhgt4  37381