Step |
Hyp |
Ref |
Expression |
0 |
|
cal |
⊢ AtLat |
1 |
|
vk |
⊢ 𝑘 |
2 |
|
clat |
⊢ Lat |
3 |
|
cbs |
⊢ Base |
4 |
1
|
cv |
⊢ 𝑘 |
5 |
4 3
|
cfv |
⊢ ( Base ‘ 𝑘 ) |
6 |
|
cglb |
⊢ glb |
7 |
4 6
|
cfv |
⊢ ( glb ‘ 𝑘 ) |
8 |
7
|
cdm |
⊢ dom ( glb ‘ 𝑘 ) |
9 |
5 8
|
wcel |
⊢ ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) |
10 |
|
vx |
⊢ 𝑥 |
11 |
10
|
cv |
⊢ 𝑥 |
12 |
|
cp0 |
⊢ 0. |
13 |
4 12
|
cfv |
⊢ ( 0. ‘ 𝑘 ) |
14 |
11 13
|
wne |
⊢ 𝑥 ≠ ( 0. ‘ 𝑘 ) |
15 |
|
vp |
⊢ 𝑝 |
16 |
|
catm |
⊢ Atoms |
17 |
4 16
|
cfv |
⊢ ( Atoms ‘ 𝑘 ) |
18 |
15
|
cv |
⊢ 𝑝 |
19 |
|
cple |
⊢ le |
20 |
4 19
|
cfv |
⊢ ( le ‘ 𝑘 ) |
21 |
18 11 20
|
wbr |
⊢ 𝑝 ( le ‘ 𝑘 ) 𝑥 |
22 |
21 15 17
|
wrex |
⊢ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 |
23 |
14 22
|
wi |
⊢ ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) |
24 |
23 10 5
|
wral |
⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) |
25 |
9 24
|
wa |
⊢ ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) ) |
26 |
25 1 2
|
crab |
⊢ { 𝑘 ∈ Lat ∣ ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) ) } |
27 |
0 26
|
wceq |
⊢ AtLat = { 𝑘 ∈ Lat ∣ ( ( Base ‘ 𝑘 ) ∈ dom ( glb ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ≠ ( 0. ‘ 𝑘 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( le ‘ 𝑘 ) 𝑥 ) ) } |