| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . . 6
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) | 
| 2 |  | ishlat.a | . . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) | 
| 3 | 1, 2 | eqtr4di 2794 | . . . . 5
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) | 
| 4 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) | 
| 5 |  | ishlat.l | . . . . . . . . . . . 12
⊢  ≤ =
(le‘𝐾) | 
| 6 | 4, 5 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) | 
| 7 | 6 | breqd 5153 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦) ↔ 𝑧 ≤ (𝑥(join‘𝑘)𝑦))) | 
| 8 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) | 
| 9 |  | ishlat.j | . . . . . . . . . . . . 13
⊢  ∨ =
(join‘𝐾) | 
| 10 | 8, 9 | eqtr4di 2794 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) | 
| 11 | 10 | oveqd 7449 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)𝑦) = (𝑥 ∨ 𝑦)) | 
| 12 | 11 | breq2d 5154 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑧 ≤ (𝑥(join‘𝑘)𝑦) ↔ 𝑧 ≤ (𝑥 ∨ 𝑦))) | 
| 13 | 7, 12 | bitrd 279 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦) ↔ 𝑧 ≤ (𝑥 ∨ 𝑦))) | 
| 14 | 13 | 3anbi3d 1443 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → ((𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦)) ↔ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))) | 
| 15 | 3, 14 | rexeqbidv 3346 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦)) ↔ ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))) | 
| 16 | 15 | imbi2d 340 | . . . . . 6
⊢ (𝑘 = 𝐾 → ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))))) | 
| 17 | 3, 16 | raleqbidv 3345 | . . . . 5
⊢ (𝑘 = 𝐾 → (∀𝑦 ∈ (Atoms‘𝑘)(𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))))) | 
| 18 | 3, 17 | raleqbidv 3345 | . . . 4
⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Atoms‘𝑘)∀𝑦 ∈ (Atoms‘𝑘)(𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))))) | 
| 19 |  | fveq2 6905 | . . . . . 6
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) | 
| 20 |  | ishlat.b | . . . . . 6
⊢ 𝐵 = (Base‘𝐾) | 
| 21 | 19, 20 | eqtr4di 2794 | . . . . 5
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) | 
| 22 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (lt‘𝑘) = (lt‘𝐾)) | 
| 23 |  | ishlat.s | . . . . . . . . . . . 12
⊢  < =
(lt‘𝐾) | 
| 24 | 22, 23 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (lt‘𝑘) = < ) | 
| 25 | 24 | breqd 5153 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ((0.‘𝑘)(lt‘𝑘)𝑥 ↔ (0.‘𝑘) < 𝑥)) | 
| 26 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (0.‘𝑘) = (0.‘𝐾)) | 
| 27 |  | ishlat.z | . . . . . . . . . . . 12
⊢  0 =
(0.‘𝐾) | 
| 28 | 26, 27 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (0.‘𝑘) = 0 ) | 
| 29 | 28 | breq1d 5152 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ((0.‘𝑘) < 𝑥 ↔ 0 < 𝑥)) | 
| 30 | 25, 29 | bitrd 279 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((0.‘𝑘)(lt‘𝑘)𝑥 ↔ 0 < 𝑥)) | 
| 31 | 24 | breqd 5153 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑥(lt‘𝑘)𝑦 ↔ 𝑥 < 𝑦)) | 
| 32 | 30, 31 | anbi12d 632 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ↔ ( 0 < 𝑥 ∧ 𝑥 < 𝑦))) | 
| 33 | 24 | breqd 5153 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑦(lt‘𝑘)𝑧 ↔ 𝑦 < 𝑧)) | 
| 34 | 24 | breqd 5153 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑧(lt‘𝑘)(1.‘𝑘) ↔ 𝑧 < (1.‘𝑘))) | 
| 35 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (1.‘𝑘) = (1.‘𝐾)) | 
| 36 |  | ishlat.u | . . . . . . . . . . . 12
⊢  1 =
(1.‘𝐾) | 
| 37 | 35, 36 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (1.‘𝑘) = 1 ) | 
| 38 | 37 | breq2d 5154 | . . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (𝑧 < (1.‘𝑘) ↔ 𝑧 < 1 )) | 
| 39 | 34, 38 | bitrd 279 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (𝑧(lt‘𝑘)(1.‘𝑘) ↔ 𝑧 < 1 )) | 
| 40 | 33, 39 | anbi12d 632 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → ((𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘)) ↔ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))) | 
| 41 | 32, 40 | anbi12d 632 | . . . . . . 7
⊢ (𝑘 = 𝐾 → ((((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘))) ↔ (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) | 
| 42 | 21, 41 | rexeqbidv 3346 | . . . . . 6
⊢ (𝑘 = 𝐾 → (∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘))) ↔ ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) | 
| 43 | 21, 42 | rexeqbidv 3346 | . . . . 5
⊢ (𝑘 = 𝐾 → (∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘))) ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) | 
| 44 | 21, 43 | rexeqbidv 3346 | . . . 4
⊢ (𝑘 = 𝐾 → (∃𝑥 ∈ (Base‘𝑘)∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘))) ↔ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) | 
| 45 | 18, 44 | anbi12d 632 | . . 3
⊢ (𝑘 = 𝐾 → ((∀𝑥 ∈ (Atoms‘𝑘)∀𝑦 ∈ (Atoms‘𝑘)(𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ∧ ∃𝑥 ∈ (Base‘𝑘)∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘)))) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))) | 
| 46 |  | df-hlat 39353 | . . 3
⊢ HL =
{𝑘 ∈ ((OML ∩ CLat)
∩ CvLat) ∣ (∀𝑥 ∈ (Atoms‘𝑘)∀𝑦 ∈ (Atoms‘𝑘)(𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ∧ ∃𝑥 ∈ (Base‘𝑘)∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘))))} | 
| 47 | 45, 46 | elrab2 3694 | . 2
⊢ (𝐾 ∈ HL ↔ (𝐾 ∈ ((OML ∩ CLat) ∩
CvLat) ∧ (∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))) | 
| 48 |  | elin 3966 | . . . . 5
⊢ (𝐾 ∈ (OML ∩ CLat) ↔
(𝐾 ∈ OML ∧ 𝐾 ∈ CLat)) | 
| 49 | 48 | anbi1i 624 | . . . 4
⊢ ((𝐾 ∈ (OML ∩ CLat) ∧
𝐾 ∈ CvLat) ↔
((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ CvLat)) | 
| 50 |  | elin 3966 | . . . 4
⊢ (𝐾 ∈ ((OML ∩ CLat) ∩
CvLat) ↔ (𝐾 ∈
(OML ∩ CLat) ∧ 𝐾
∈ CvLat)) | 
| 51 |  | df-3an 1088 | . . . 4
⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ CvLat)) | 
| 52 | 49, 50, 51 | 3bitr4ri 304 | . . 3
⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ↔ 𝐾 ∈ ((OML ∩ CLat) ∩
CvLat)) | 
| 53 | 52 | anbi1i 624 | . 2
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) ↔ (𝐾 ∈ ((OML ∩ CLat) ∩
CvLat) ∧ (∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))) | 
| 54 | 47, 53 | bitr4i 278 | 1
⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))) |