Step | Hyp | Ref
| Expression |
1 | | tospos 18373 |
. 2
โข (๐พ โ Toset โ ๐พ โ Poset) |
2 | 1 | ad2antrr 725 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฅ(leโ๐พ)๐ฆ) โ ๐พ โ Poset) |
3 | | eqid 2733 |
. . . . . . 7
โข
(Baseโ๐พ) =
(Baseโ๐พ) |
4 | | simplrl 776 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฅ(leโ๐พ)๐ฆ) โ ๐ฅ โ (Baseโ๐พ)) |
5 | | simplrr 777 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฅ(leโ๐พ)๐ฆ) โ ๐ฆ โ (Baseโ๐พ)) |
6 | | eqid 2733 |
. . . . . . 7
โข
(leโ๐พ) =
(leโ๐พ) |
7 | | simpr 486 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฅ(leโ๐พ)๐ฆ) โ ๐ฅ(leโ๐พ)๐ฆ) |
8 | | eqidd 2734 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฅ(leโ๐พ)๐ฆ) โ {๐ฅ, ๐ฆ} = {๐ฅ, ๐ฆ}) |
9 | | eqid 2733 |
. . . . . . 7
โข
(lubโ๐พ) =
(lubโ๐พ) |
10 | 2, 3, 4, 5, 6, 7, 8, 9 | lubprdm 47596 |
. . . . . 6
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฅ(leโ๐พ)๐ฆ) โ {๐ฅ, ๐ฆ} โ dom (lubโ๐พ)) |
11 | 1 | ad2antrr 725 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฆ(leโ๐พ)๐ฅ) โ ๐พ โ Poset) |
12 | | simplrr 777 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฆ(leโ๐พ)๐ฅ) โ ๐ฆ โ (Baseโ๐พ)) |
13 | | simplrl 776 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฆ(leโ๐พ)๐ฅ) โ ๐ฅ โ (Baseโ๐พ)) |
14 | | simpr 486 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฆ(leโ๐พ)๐ฅ) โ ๐ฆ(leโ๐พ)๐ฅ) |
15 | | prcom 4737 |
. . . . . . . 8
โข {๐ฅ, ๐ฆ} = {๐ฆ, ๐ฅ} |
16 | 15 | a1i 11 |
. . . . . . 7
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฆ(leโ๐พ)๐ฅ) โ {๐ฅ, ๐ฆ} = {๐ฆ, ๐ฅ}) |
17 | 11, 3, 12, 13, 6, 14, 16, 9 | lubprdm 47596 |
. . . . . 6
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฆ(leโ๐พ)๐ฅ) โ {๐ฅ, ๐ฆ} โ dom (lubโ๐พ)) |
18 | 3, 6 | tleile 18374 |
. . . . . . 7
โข ((๐พ โ Toset โง ๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ)) โ (๐ฅ(leโ๐พ)๐ฆ โจ ๐ฆ(leโ๐พ)๐ฅ)) |
19 | 18 | 3expb 1121 |
. . . . . 6
โข ((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โ (๐ฅ(leโ๐พ)๐ฆ โจ ๐ฆ(leโ๐พ)๐ฅ)) |
20 | 10, 17, 19 | mpjaodan 958 |
. . . . 5
โข ((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โ {๐ฅ, ๐ฆ} โ dom (lubโ๐พ)) |
21 | 20 | ralrimivva 3201 |
. . . 4
โข (๐พ โ Toset โ
โ๐ฅ โ
(Baseโ๐พ)โ๐ฆ โ (Baseโ๐พ){๐ฅ, ๐ฆ} โ dom (lubโ๐พ)) |
22 | | eqid 2733 |
. . . . 5
โข
(joinโ๐พ) =
(joinโ๐พ) |
23 | 3, 1, 9, 22 | joindm2 47601 |
. . . 4
โข (๐พ โ Toset โ (dom
(joinโ๐พ) =
((Baseโ๐พ) ร
(Baseโ๐พ)) โ
โ๐ฅ โ
(Baseโ๐พ)โ๐ฆ โ (Baseโ๐พ){๐ฅ, ๐ฆ} โ dom (lubโ๐พ))) |
24 | 21, 23 | mpbird 257 |
. . 3
โข (๐พ โ Toset โ dom
(joinโ๐พ) =
((Baseโ๐พ) ร
(Baseโ๐พ))) |
25 | | eqid 2733 |
. . . . . . 7
โข
(glbโ๐พ) =
(glbโ๐พ) |
26 | 2, 3, 4, 5, 6, 7, 8, 25 | glbprdm 47599 |
. . . . . 6
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฅ(leโ๐พ)๐ฆ) โ {๐ฅ, ๐ฆ} โ dom (glbโ๐พ)) |
27 | 11, 3, 12, 13, 6, 14, 16, 25 | glbprdm 47599 |
. . . . . 6
โข (((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โง ๐ฆ(leโ๐พ)๐ฅ) โ {๐ฅ, ๐ฆ} โ dom (glbโ๐พ)) |
28 | 26, 27, 19 | mpjaodan 958 |
. . . . 5
โข ((๐พ โ Toset โง (๐ฅ โ (Baseโ๐พ) โง ๐ฆ โ (Baseโ๐พ))) โ {๐ฅ, ๐ฆ} โ dom (glbโ๐พ)) |
29 | 28 | ralrimivva 3201 |
. . . 4
โข (๐พ โ Toset โ
โ๐ฅ โ
(Baseโ๐พ)โ๐ฆ โ (Baseโ๐พ){๐ฅ, ๐ฆ} โ dom (glbโ๐พ)) |
30 | | eqid 2733 |
. . . . 5
โข
(meetโ๐พ) =
(meetโ๐พ) |
31 | 3, 1, 25, 30 | meetdm2 47603 |
. . . 4
โข (๐พ โ Toset โ (dom
(meetโ๐พ) =
((Baseโ๐พ) ร
(Baseโ๐พ)) โ
โ๐ฅ โ
(Baseโ๐พ)โ๐ฆ โ (Baseโ๐พ){๐ฅ, ๐ฆ} โ dom (glbโ๐พ))) |
32 | 29, 31 | mpbird 257 |
. . 3
โข (๐พ โ Toset โ dom
(meetโ๐พ) =
((Baseโ๐พ) ร
(Baseโ๐พ))) |
33 | 24, 32 | jca 513 |
. 2
โข (๐พ โ Toset โ (dom
(joinโ๐พ) =
((Baseโ๐พ) ร
(Baseโ๐พ)) โง dom
(meetโ๐พ) =
((Baseโ๐พ) ร
(Baseโ๐พ)))) |
34 | 3, 22, 30 | islat 18386 |
. 2
โข (๐พ โ Lat โ (๐พ โ Poset โง (dom
(joinโ๐พ) =
((Baseโ๐พ) ร
(Baseโ๐พ)) โง dom
(meetโ๐พ) =
((Baseโ๐พ) ร
(Baseโ๐พ))))) |
35 | 1, 33, 34 | sylanbrc 584 |
1
โข (๐พ โ Toset โ ๐พ โ Lat) |