Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
โข
(Baseโ๐พ) =
(Baseโ๐พ) |
2 | | eqid 2737 |
. . 3
โข
(lubโ๐พ) =
(lubโ๐พ) |
3 | | eqid 2737 |
. . 3
โข
(glbโ๐พ) =
(glbโ๐พ) |
4 | | eqid 2737 |
. . 3
โข
(leโ๐พ) =
(leโ๐พ) |
5 | | eqid 2737 |
. . 3
โข
(ocโ๐พ) =
(ocโ๐พ) |
6 | | eqid 2737 |
. . 3
โข
(joinโ๐พ) =
(joinโ๐พ) |
7 | | eqid 2737 |
. . 3
โข
(meetโ๐พ) =
(meetโ๐พ) |
8 | | eqid 2737 |
. . 3
โข
(0.โ๐พ) =
(0.โ๐พ) |
9 | | eqid 2737 |
. . 3
โข
(1.โ๐พ) =
(1.โ๐พ) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | isopos 37645 |
. 2
โข (๐พ โ OP โ ((๐พ โ Poset โง
(Baseโ๐พ) โ dom
(lubโ๐พ) โง
(Baseโ๐พ) โ dom
(glbโ๐พ)) โง
โ๐ฅ โ
(Baseโ๐พ)โ๐ฆ โ (Baseโ๐พ)((((ocโ๐พ)โ๐ฅ) โ (Baseโ๐พ) โง ((ocโ๐พ)โ((ocโ๐พ)โ๐ฅ)) = ๐ฅ โง (๐ฅ(leโ๐พ)๐ฆ โ ((ocโ๐พ)โ๐ฆ)(leโ๐พ)((ocโ๐พ)โ๐ฅ))) โง (๐ฅ(joinโ๐พ)((ocโ๐พ)โ๐ฅ)) = (1.โ๐พ) โง (๐ฅ(meetโ๐พ)((ocโ๐พ)โ๐ฅ)) = (0.โ๐พ)))) |
11 | | simpl1 1192 |
. 2
โข (((๐พ โ Poset โง
(Baseโ๐พ) โ dom
(lubโ๐พ) โง
(Baseโ๐พ) โ dom
(glbโ๐พ)) โง
โ๐ฅ โ
(Baseโ๐พ)โ๐ฆ โ (Baseโ๐พ)((((ocโ๐พ)โ๐ฅ) โ (Baseโ๐พ) โง ((ocโ๐พ)โ((ocโ๐พ)โ๐ฅ)) = ๐ฅ โง (๐ฅ(leโ๐พ)๐ฆ โ ((ocโ๐พ)โ๐ฆ)(leโ๐พ)((ocโ๐พ)โ๐ฅ))) โง (๐ฅ(joinโ๐พ)((ocโ๐พ)โ๐ฅ)) = (1.โ๐พ) โง (๐ฅ(meetโ๐พ)((ocโ๐พ)โ๐ฅ)) = (0.โ๐พ))) โ ๐พ โ Poset) |
12 | 10, 11 | sylbi 216 |
1
โข (๐พ โ OP โ ๐พ โ Poset) |