Detailed syntax breakdown of Definition df-atl
Step | Hyp | Ref
| Expression |
1 | | cal 36901 |
. 2
class
AtLat |
2 | | vk |
. . . . . . 7
setvar 𝑘 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑘 |
4 | | cbs 16586 |
. . . . . 6
class
Base |
5 | 3, 4 | cfv 6339 |
. . . . 5
class
(Base‘𝑘) |
6 | | cglb 17669 |
. . . . . . 7
class
glb |
7 | 3, 6 | cfv 6339 |
. . . . . 6
class
(glb‘𝑘) |
8 | 7 | cdm 5525 |
. . . . 5
class dom
(glb‘𝑘) |
9 | 5, 8 | wcel 2114 |
. . . 4
wff
(Base‘𝑘)
∈ dom (glb‘𝑘) |
10 | | vx |
. . . . . . . 8
setvar 𝑥 |
11 | 10 | cv 1541 |
. . . . . . 7
class 𝑥 |
12 | | cp0 17763 |
. . . . . . . 8
class
0. |
13 | 3, 12 | cfv 6339 |
. . . . . . 7
class
(0.‘𝑘) |
14 | 11, 13 | wne 2934 |
. . . . . 6
wff 𝑥 ≠ (0.‘𝑘) |
15 | | vp |
. . . . . . . . 9
setvar 𝑝 |
16 | 15 | cv 1541 |
. . . . . . . 8
class 𝑝 |
17 | | cple 16675 |
. . . . . . . . 9
class
le |
18 | 3, 17 | cfv 6339 |
. . . . . . . 8
class
(le‘𝑘) |
19 | 16, 11, 18 | wbr 5030 |
. . . . . . 7
wff 𝑝(le‘𝑘)𝑥 |
20 | | catm 36900 |
. . . . . . . 8
class
Atoms |
21 | 3, 20 | cfv 6339 |
. . . . . . 7
class
(Atoms‘𝑘) |
22 | 19, 15, 21 | wrex 3054 |
. . . . . 6
wff
∃𝑝 ∈
(Atoms‘𝑘)𝑝(le‘𝑘)𝑥 |
23 | 14, 22 | wi 4 |
. . . . 5
wff (𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥) |
24 | 23, 10, 5 | wral 3053 |
. . . 4
wff
∀𝑥 ∈
(Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥) |
25 | 9, 24 | wa 399 |
. . 3
wff
((Base‘𝑘)
∈ dom (glb‘𝑘)
∧ ∀𝑥 ∈
(Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥)) |
26 | | clat 17771 |
. . 3
class
Lat |
27 | 25, 2, 26 | crab 3057 |
. 2
class {𝑘 ∈ Lat ∣
((Base‘𝑘) ∈ dom
(glb‘𝑘) ∧
∀𝑥 ∈
(Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))} |
28 | 1, 27 | wceq 1542 |
1
wff AtLat =
{𝑘 ∈ Lat ∣
((Base‘𝑘) ∈ dom
(glb‘𝑘) ∧
∀𝑥 ∈
(Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))} |