| Step | Hyp | Ref
| Expression |
|---|
| 1 | | elex 3492 |
. 2
β’ (π β CLat β π β V) |
| 2 | | noel 4330 |
. . . . 5
β’ Β¬
((lubββ
)ββ
) β β
|
| 3 | | ssid 4004 |
. . . . . 6
β’ β
β β
|
| 4 | | base0 17153 |
. . . . . . 7
β’ β
=
(Baseββ
) |
| 5 | | eqid 2732 |
. . . . . . 7
β’
(lubββ
) = (lubββ
) |
| 6 | 4, 5 | clatlubcl 18460 |
. . . . . 6
β’ ((β
β CLat β§ β
β β
) β
((lubββ
)ββ
) β β
) |
| 7 | 3, 6 | mpan2 689 |
. . . . 5
β’ (β
β CLat β ((lubββ
)ββ
) β
β
) |
| 8 | 2, 7 | mto 196 |
. . . 4
β’ Β¬
β
β CLat |
| 9 | | oduclatb.d |
. . . . . 6
β’ π· = (ODualβπ) |
| 10 | | fvprc 6883 |
. . . . . 6
β’ (Β¬
π β V β
(ODualβπ) =
β
) |
| 11 | 9, 10 | eqtrid 2784 |
. . . . 5
β’ (Β¬
π β V β π· = β
) |
| 12 | 11 | eleq1d 2818 |
. . . 4
β’ (Β¬
π β V β (π· β CLat β β
β CLat)) |
| 13 | 8, 12 | mtbiri 326 |
. . 3
β’ (Β¬
π β V β Β¬
π· β
CLat) |
| 14 | 13 | con4i 114 |
. 2
β’ (π· β CLat β π β V) |
| 15 | 9 | oduposb 18286 |
. . . 4
β’ (π β V β (π β Poset β π· β Poset)) |
| 16 | | ancom 461 |
. . . . 5
β’ ((dom
(lubβπ) = π«
(Baseβπ) β§ dom
(glbβπ) = π«
(Baseβπ)) β (dom
(glbβπ) = π«
(Baseβπ) β§ dom
(lubβπ) = π«
(Baseβπ))) |
| 17 | | eqid 2732 |
. . . . . . . . 9
β’
(glbβπ) =
(glbβπ) |
| 18 | 9, 17 | odulub 18364 |
. . . . . . . 8
β’ (π β V β
(glbβπ) =
(lubβπ·)) |
| 19 | 18 | dmeqd 5905 |
. . . . . . 7
β’ (π β V β dom
(glbβπ) = dom
(lubβπ·)) |
| 20 | 19 | eqeq1d 2734 |
. . . . . 6
β’ (π β V β (dom
(glbβπ) = π«
(Baseβπ) β dom
(lubβπ·) = π«
(Baseβπ))) |
| 21 | | eqid 2732 |
. . . . . . . . 9
β’
(lubβπ) =
(lubβπ) |
| 22 | 9, 21 | oduglb 18366 |
. . . . . . . 8
β’ (π β V β
(lubβπ) =
(glbβπ·)) |
| 23 | 22 | dmeqd 5905 |
. . . . . . 7
β’ (π β V β dom
(lubβπ) = dom
(glbβπ·)) |
| 24 | 23 | eqeq1d 2734 |
. . . . . 6
β’ (π β V β (dom
(lubβπ) = π«
(Baseβπ) β dom
(glbβπ·) = π«
(Baseβπ))) |
| 25 | 20, 24 | anbi12d 631 |
. . . . 5
β’ (π β V β ((dom
(glbβπ) = π«
(Baseβπ) β§ dom
(lubβπ) = π«
(Baseβπ)) β (dom
(lubβπ·) = π«
(Baseβπ) β§ dom
(glbβπ·) = π«
(Baseβπ)))) |
| 26 | 16, 25 | bitrid 282 |
. . . 4
β’ (π β V β ((dom
(lubβπ) = π«
(Baseβπ) β§ dom
(glbβπ) = π«
(Baseβπ)) β (dom
(lubβπ·) = π«
(Baseβπ) β§ dom
(glbβπ·) = π«
(Baseβπ)))) |
| 27 | 15, 26 | anbi12d 631 |
. . 3
β’ (π β V β ((π β Poset β§ (dom
(lubβπ) = π«
(Baseβπ) β§ dom
(glbβπ) = π«
(Baseβπ))) β
(π· β Poset β§ (dom
(lubβπ·) = π«
(Baseβπ) β§ dom
(glbβπ·) = π«
(Baseβπ))))) |
| 28 | | eqid 2732 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
| 29 | 28, 21, 17 | isclat 18457 |
. . 3
β’ (π β CLat β (π β Poset β§ (dom
(lubβπ) = π«
(Baseβπ) β§ dom
(glbβπ) = π«
(Baseβπ)))) |
| 30 | 9, 28 | odubas 18248 |
. . . 4
β’
(Baseβπ) =
(Baseβπ·) |
| 31 | | eqid 2732 |
. . . 4
β’
(lubβπ·) =
(lubβπ·) |
| 32 | | eqid 2732 |
. . . 4
β’
(glbβπ·) =
(glbβπ·) |
| 33 | 30, 31, 32 | isclat 18457 |
. . 3
β’ (π· β CLat β (π· β Poset β§ (dom
(lubβπ·) = π«
(Baseβπ) β§ dom
(glbβπ·) = π«
(Baseβπ)))) |
| 34 | 27, 29, 33 | 3bitr4g 313 |
. 2
β’ (π β V β (π β CLat β π· β CLat)) |
| 35 | 1, 14, 34 | pm5.21nii 379 |
1
β’ (π β CLat β π· β CLat) |
