Metamath Proof Explorer

Theorem ishlat2

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

Ref Expression
Hypotheses ishlat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ishlat.l ⊢ ≤ = ( le ‘ 𝐾 )
ishlat.s ⊢ < = ( lt ‘ 𝐾 )
ishlat.j ⊢ ∨ = ( join ‘ 𝐾 )
ishlat.z ⊢ 0 = ( 0. ‘ 𝐾 )
ishlat.u ⊢ 1 = ( 1. ‘ 𝐾 )
ishlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion ishlat2 ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( ¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ ( 𝑧 ∨ 𝑦 ) ) → 𝑦 ≤ ( 𝑧 ∨ 𝑥 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )

Proof

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