| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . . . 6
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) | 
| 2 |  | isatlat.b | . . . . . 6
⊢ 𝐵 = (Base‘𝐾) | 
| 3 | 1, 2 | eqtr4di 2795 | . . . . 5
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) | 
| 4 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (glb‘𝑘) = (glb‘𝐾)) | 
| 5 |  | isatlat.g | . . . . . . 7
⊢ 𝐺 = (glb‘𝐾) | 
| 6 | 4, 5 | eqtr4di 2795 | . . . . . 6
⊢ (𝑘 = 𝐾 → (glb‘𝑘) = 𝐺) | 
| 7 | 6 | dmeqd 5916 | . . . . 5
⊢ (𝑘 = 𝐾 → dom (glb‘𝑘) = dom 𝐺) | 
| 8 | 3, 7 | eleq12d 2835 | . . . 4
⊢ (𝑘 = 𝐾 → ((Base‘𝑘) ∈ dom (glb‘𝑘) ↔ 𝐵 ∈ dom 𝐺)) | 
| 9 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (0.‘𝑘) = (0.‘𝐾)) | 
| 10 |  | isatlat.z | . . . . . . . 8
⊢  0 =
(0.‘𝐾) | 
| 11 | 9, 10 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (0.‘𝑘) = 0 ) | 
| 12 | 11 | neeq2d 3001 | . . . . . 6
⊢ (𝑘 = 𝐾 → (𝑥 ≠ (0.‘𝑘) ↔ 𝑥 ≠ 0 )) | 
| 13 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) | 
| 14 |  | isatlat.a | . . . . . . . 8
⊢ 𝐴 = (Atoms‘𝐾) | 
| 15 | 13, 14 | eqtr4di 2795 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) | 
| 16 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) | 
| 17 |  | isatlat.l | . . . . . . . . 9
⊢  ≤ =
(le‘𝐾) | 
| 18 | 16, 17 | eqtr4di 2795 | . . . . . . . 8
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) | 
| 19 | 18 | breqd 5154 | . . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑦(le‘𝑘)𝑥 ↔ 𝑦 ≤ 𝑥)) | 
| 20 | 15, 19 | rexeqbidv 3347 | . . . . . 6
⊢ (𝑘 = 𝐾 → (∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) | 
| 21 | 12, 20 | imbi12d 344 | . . . . 5
⊢ (𝑘 = 𝐾 → ((𝑥 ≠ (0.‘𝑘) → ∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥) ↔ (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))) | 
| 22 | 3, 21 | raleqbidv 3346 | . . . 4
⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥) ↔ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))) | 
| 23 | 8, 22 | anbi12d 632 | . . 3
⊢ (𝑘 = 𝐾 → (((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥)) ↔ (𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)))) | 
| 24 |  | df-atl 39299 | . . 3
⊢ AtLat =
{𝑘 ∈ Lat ∣
((Base‘𝑘) ∈ dom
(glb‘𝑘) ∧
∀𝑥 ∈
(Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑦 ∈ (Atoms‘𝑘)𝑦(le‘𝑘)𝑥))} | 
| 25 | 23, 24 | elrab2 3695 | . 2
⊢ (𝐾 ∈ AtLat ↔ (𝐾 ∈ Lat ∧ (𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)))) | 
| 26 |  | 3anass 1095 | . 2
⊢ ((𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) ↔ (𝐾 ∈ Lat ∧ (𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)))) | 
| 27 | 25, 26 | bitr4i 278 | 1
⊢ (𝐾 ∈ AtLat ↔ (𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))) |