Detailed syntax breakdown of Definition df-cvlat
| Step | Hyp | Ref
| Expression |
| 1 | | clc 39266 |
. 2
class
CvLat |
| 2 | | va |
. . . . . . . . . . 11
setvar 𝑎 |
| 3 | 2 | cv 1539 |
. . . . . . . . . 10
class 𝑎 |
| 4 | | vc |
. . . . . . . . . . 11
setvar 𝑐 |
| 5 | 4 | cv 1539 |
. . . . . . . . . 10
class 𝑐 |
| 6 | | vk |
. . . . . . . . . . . 12
setvar 𝑘 |
| 7 | 6 | cv 1539 |
. . . . . . . . . . 11
class 𝑘 |
| 8 | | cple 17304 |
. . . . . . . . . . 11
class
le |
| 9 | 7, 8 | cfv 6561 |
. . . . . . . . . 10
class
(le‘𝑘) |
| 10 | 3, 5, 9 | wbr 5143 |
. . . . . . . . 9
wff 𝑎(le‘𝑘)𝑐 |
| 11 | 10 | wn 3 |
. . . . . . . 8
wff ¬
𝑎(le‘𝑘)𝑐 |
| 12 | | vb |
. . . . . . . . . . 11
setvar 𝑏 |
| 13 | 12 | cv 1539 |
. . . . . . . . . 10
class 𝑏 |
| 14 | | cjn 18357 |
. . . . . . . . . . 11
class
join |
| 15 | 7, 14 | cfv 6561 |
. . . . . . . . . 10
class
(join‘𝑘) |
| 16 | 5, 13, 15 | co 7431 |
. . . . . . . . 9
class (𝑐(join‘𝑘)𝑏) |
| 17 | 3, 16, 9 | wbr 5143 |
. . . . . . . 8
wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏) |
| 18 | 11, 17 | wa 395 |
. . . . . . 7
wff (¬
𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) |
| 19 | 5, 3, 15 | co 7431 |
. . . . . . . 8
class (𝑐(join‘𝑘)𝑎) |
| 20 | 13, 19, 9 | wbr 5143 |
. . . . . . 7
wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎) |
| 21 | 18, 20 | wi 4 |
. . . . . 6
wff ((¬
𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)) |
| 22 | | cbs 17247 |
. . . . . . 7
class
Base |
| 23 | 7, 22 | cfv 6561 |
. . . . . 6
class
(Base‘𝑘) |
| 24 | 21, 4, 23 | wral 3061 |
. . . . 5
wff
∀𝑐 ∈
(Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)) |
| 25 | | catm 39264 |
. . . . . 6
class
Atoms |
| 26 | 7, 25 | cfv 6561 |
. . . . 5
class
(Atoms‘𝑘) |
| 27 | 24, 12, 26 | wral 3061 |
. . . 4
wff
∀𝑏 ∈
(Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)) |
| 28 | 27, 2, 26 | wral 3061 |
. . 3
wff
∀𝑎 ∈
(Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)) |
| 29 | | cal 39265 |
. . 3
class
AtLat |
| 30 | 28, 6, 29 | crab 3436 |
. 2
class {𝑘 ∈ AtLat ∣
∀𝑎 ∈
(Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))} |
| 31 | 1, 30 | wceq 1540 |
1
wff CvLat =
{𝑘 ∈ AtLat ∣
∀𝑎 ∈
(Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))} |