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