Step | Hyp | Ref
| Expression |
1 | | clc 38135 |
. 2
class
CvLat |
2 | | va |
. . . . . . . . . . 11
setvar π |
3 | 2 | cv 1541 |
. . . . . . . . . 10
class π |
4 | | vc |
. . . . . . . . . . 11
setvar π |
5 | 4 | cv 1541 |
. . . . . . . . . 10
class π |
6 | | vk |
. . . . . . . . . . . 12
setvar π |
7 | 6 | cv 1541 |
. . . . . . . . . . 11
class π |
8 | | cple 17204 |
. . . . . . . . . . 11
class
le |
9 | 7, 8 | cfv 6544 |
. . . . . . . . . 10
class
(leβπ) |
10 | 3, 5, 9 | wbr 5149 |
. . . . . . . . 9
wff π(leβπ)π |
11 | 10 | wn 3 |
. . . . . . . 8
wff Β¬
π(leβπ)π |
12 | | vb |
. . . . . . . . . . 11
setvar π |
13 | 12 | cv 1541 |
. . . . . . . . . 10
class π |
14 | | cjn 18264 |
. . . . . . . . . . 11
class
join |
15 | 7, 14 | cfv 6544 |
. . . . . . . . . 10
class
(joinβπ) |
16 | 5, 13, 15 | co 7409 |
. . . . . . . . 9
class (π(joinβπ)π) |
17 | 3, 16, 9 | wbr 5149 |
. . . . . . . 8
wff π(leβπ)(π(joinβπ)π) |
18 | 11, 17 | wa 397 |
. . . . . . 7
wff (Β¬
π(leβπ)π β§ π(leβπ)(π(joinβπ)π)) |
19 | 5, 3, 15 | co 7409 |
. . . . . . . 8
class (π(joinβπ)π) |
20 | 13, 19, 9 | wbr 5149 |
. . . . . . 7
wff π(leβπ)(π(joinβπ)π) |
21 | 18, 20 | wi 4 |
. . . . . 6
wff ((Β¬
π(leβπ)π β§ π(leβπ)(π(joinβπ)π)) β π(leβπ)(π(joinβπ)π)) |
22 | | cbs 17144 |
. . . . . . 7
class
Base |
23 | 7, 22 | cfv 6544 |
. . . . . 6
class
(Baseβπ) |
24 | 21, 4, 23 | wral 3062 |
. . . . 5
wff
βπ β
(Baseβπ)((Β¬ π(leβπ)π β§ π(leβπ)(π(joinβπ)π)) β π(leβπ)(π(joinβπ)π)) |
25 | | catm 38133 |
. . . . . 6
class
Atoms |
26 | 7, 25 | cfv 6544 |
. . . . 5
class
(Atomsβπ) |
27 | 24, 12, 26 | wral 3062 |
. . . 4
wff
βπ β
(Atomsβπ)βπ β (Baseβπ)((Β¬ π(leβπ)π β§ π(leβπ)(π(joinβπ)π)) β π(leβπ)(π(joinβπ)π)) |
28 | 27, 2, 26 | wral 3062 |
. . 3
wff
βπ β
(Atomsβπ)βπ β (Atomsβπ)βπ β (Baseβπ)((Β¬ π(leβπ)π β§ π(leβπ)(π(joinβπ)π)) β π(leβπ)(π(joinβπ)π)) |
29 | | cal 38134 |
. . 3
class
AtLat |
30 | 28, 6, 29 | crab 3433 |
. 2
class {π β AtLat β£
βπ β
(Atomsβπ)βπ β (Atomsβπ)βπ β (Baseβπ)((Β¬ π(leβπ)π β§ π(leβπ)(π(joinβπ)π)) β π(leβπ)(π(joinβπ)π))} |
31 | 1, 30 | wceq 1542 |
1
wff CvLat =
{π β AtLat β£
βπ β
(Atomsβπ)βπ β (Atomsβπ)βπ β (Baseβπ)((Β¬ π(leβπ)π β§ π(leβπ)(π(joinβπ)π)) β π(leβπ)(π(joinβπ)π))} |