Step | Hyp | Ref
| Expression |
1 | | mreclat.i |
. . . 4
β’ πΌ = (toIncβπΆ) |
2 | 1 | ipopos 18489 |
. . 3
β’ πΌ β Poset |
3 | 2 | a1i 11 |
. 2
β’ (πΆ β (Mooreβπ) β πΌ β Poset) |
4 | | eqid 2733 |
. . . . . . . 8
β’
(mrClsβπΆ) =
(mrClsβπΆ) |
5 | | eqid 2733 |
. . . . . . . 8
β’
(lubβπΌ) =
(lubβπΌ) |
6 | 1, 4, 5 | mrelatlub 18515 |
. . . . . . 7
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ) β ((lubβπΌ)βπ₯) = ((mrClsβπΆ)ββͺ π₯)) |
7 | | uniss 4917 |
. . . . . . . . . 10
β’ (π₯ β πΆ β βͺ π₯ β βͺ πΆ) |
8 | 7 | adantl 483 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ) β βͺ π₯ β βͺ πΆ) |
9 | | mreuni 17544 |
. . . . . . . . . 10
β’ (πΆ β (Mooreβπ) β βͺ πΆ =
π) |
10 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ) β βͺ πΆ = π) |
11 | 8, 10 | sseqtrd 4023 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ) β βͺ π₯ β π) |
12 | 4 | mrccl 17555 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ βͺ π₯
β π) β
((mrClsβπΆ)ββͺ π₯) β πΆ) |
13 | 11, 12 | syldan 592 |
. . . . . . 7
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ) β ((mrClsβπΆ)ββͺ π₯) β πΆ) |
14 | 6, 13 | eqeltrd 2834 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ) β ((lubβπΌ)βπ₯) β πΆ) |
15 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π₯ = β
β
((glbβπΌ)βπ₯) = ((glbβπΌ)ββ
)) |
16 | 15 | adantl 483 |
. . . . . . . . 9
β’ (((πΆ β (Mooreβπ) β§ π₯ β πΆ) β§ π₯ = β
) β ((glbβπΌ)βπ₯) = ((glbβπΌ)ββ
)) |
17 | | eqid 2733 |
. . . . . . . . . . 11
β’
(glbβπΌ) =
(glbβπΌ) |
18 | 1, 17 | mrelatglb0 18514 |
. . . . . . . . . 10
β’ (πΆ β (Mooreβπ) β ((glbβπΌ)ββ
) = π) |
19 | 18 | ad2antrr 725 |
. . . . . . . . 9
β’ (((πΆ β (Mooreβπ) β§ π₯ β πΆ) β§ π₯ = β
) β ((glbβπΌ)ββ
) = π) |
20 | 16, 19 | eqtrd 2773 |
. . . . . . . 8
β’ (((πΆ β (Mooreβπ) β§ π₯ β πΆ) β§ π₯ = β
) β ((glbβπΌ)βπ₯) = π) |
21 | | mre1cl 17538 |
. . . . . . . . 9
β’ (πΆ β (Mooreβπ) β π β πΆ) |
22 | 21 | ad2antrr 725 |
. . . . . . . 8
β’ (((πΆ β (Mooreβπ) β§ π₯ β πΆ) β§ π₯ = β
) β π β πΆ) |
23 | 20, 22 | eqeltrd 2834 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ π₯ β πΆ) β§ π₯ = β
) β ((glbβπΌ)βπ₯) β πΆ) |
24 | 1, 17 | mrelatglb 18513 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ β§ π₯ β β
) β ((glbβπΌ)βπ₯) = β© π₯) |
25 | | mreintcl 17539 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ β§ π₯ β β
) β β© π₯
β πΆ) |
26 | 24, 25 | eqeltrd 2834 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ β§ π₯ β β
) β ((glbβπΌ)βπ₯) β πΆ) |
27 | 26 | 3expa 1119 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ π₯ β πΆ) β§ π₯ β β
) β ((glbβπΌ)βπ₯) β πΆ) |
28 | 23, 27 | pm2.61dane 3030 |
. . . . . 6
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ) β ((glbβπΌ)βπ₯) β πΆ) |
29 | 14, 28 | jca 513 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π₯ β πΆ) β (((lubβπΌ)βπ₯) β πΆ β§ ((glbβπΌ)βπ₯) β πΆ)) |
30 | 29 | ex 414 |
. . . 4
β’ (πΆ β (Mooreβπ) β (π₯ β πΆ β (((lubβπΌ)βπ₯) β πΆ β§ ((glbβπΌ)βπ₯) β πΆ))) |
31 | 1 | ipobas 18484 |
. . . . 5
β’ (πΆ β (Mooreβπ) β πΆ = (BaseβπΌ)) |
32 | | sseq2 4009 |
. . . . . 6
β’ (πΆ = (BaseβπΌ) β (π₯ β πΆ β π₯ β (BaseβπΌ))) |
33 | | eleq2 2823 |
. . . . . . 7
β’ (πΆ = (BaseβπΌ) β (((lubβπΌ)βπ₯) β πΆ β ((lubβπΌ)βπ₯) β (BaseβπΌ))) |
34 | | eleq2 2823 |
. . . . . . 7
β’ (πΆ = (BaseβπΌ) β (((glbβπΌ)βπ₯) β πΆ β ((glbβπΌ)βπ₯) β (BaseβπΌ))) |
35 | 33, 34 | anbi12d 632 |
. . . . . 6
β’ (πΆ = (BaseβπΌ) β ((((lubβπΌ)βπ₯) β πΆ β§ ((glbβπΌ)βπ₯) β πΆ) β (((lubβπΌ)βπ₯) β (BaseβπΌ) β§ ((glbβπΌ)βπ₯) β (BaseβπΌ)))) |
36 | 32, 35 | imbi12d 345 |
. . . . 5
β’ (πΆ = (BaseβπΌ) β ((π₯ β πΆ β (((lubβπΌ)βπ₯) β πΆ β§ ((glbβπΌ)βπ₯) β πΆ)) β (π₯ β (BaseβπΌ) β (((lubβπΌ)βπ₯) β (BaseβπΌ) β§ ((glbβπΌ)βπ₯) β (BaseβπΌ))))) |
37 | 31, 36 | syl 17 |
. . . 4
β’ (πΆ β (Mooreβπ) β ((π₯ β πΆ β (((lubβπΌ)βπ₯) β πΆ β§ ((glbβπΌ)βπ₯) β πΆ)) β (π₯ β (BaseβπΌ) β (((lubβπΌ)βπ₯) β (BaseβπΌ) β§ ((glbβπΌ)βπ₯) β (BaseβπΌ))))) |
38 | 30, 37 | mpbid 231 |
. . 3
β’ (πΆ β (Mooreβπ) β (π₯ β (BaseβπΌ) β (((lubβπΌ)βπ₯) β (BaseβπΌ) β§ ((glbβπΌ)βπ₯) β (BaseβπΌ)))) |
39 | 38 | alrimiv 1931 |
. 2
β’ (πΆ β (Mooreβπ) β βπ₯(π₯ β (BaseβπΌ) β (((lubβπΌ)βπ₯) β (BaseβπΌ) β§ ((glbβπΌ)βπ₯) β (BaseβπΌ)))) |
40 | | isclatBAD. |
. 2
β’ (πΌ β CLat β (πΌ β Poset β§
βπ₯(π₯ β (BaseβπΌ) β (((lubβπΌ)βπ₯) β (BaseβπΌ) β§ ((glbβπΌ)βπ₯) β (BaseβπΌ))))) |
41 | 3, 39, 40 | sylanbrc 584 |
1
β’ (πΆ β (Mooreβπ) β πΌ β CLat) |