Step | Hyp | Ref
| Expression |
1 | | breq1 5151 |
. . . . 5
β’ (π§ = π β (π§ β€ π β π β€ π)) |
2 | | breq1 5151 |
. . . . 5
β’ (π§ = π β (π§ β€ π β π β€ π)) |
3 | 1, 2 | anbi12d 630 |
. . . 4
β’ (π§ = π β ((π§ β€ π β§ π§ β€ π) β (π β€ π β§ π β€ π))) |
4 | | breq1 5151 |
. . . 4
β’ (π§ = π β (π§ β€ (π β§ π) β π β€ (π β§ π))) |
5 | 3, 4 | imbi12d 344 |
. . 3
β’ (π§ = π β (((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π)) β ((π β€ π β§ π β€ π) β π β€ (π β§ π)))) |
6 | | meetle.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
7 | | meetle.l |
. . . . 5
β’ β€ =
(leβπΎ) |
8 | | meetle.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
9 | | meetle.k |
. . . . 5
β’ (π β πΎ β Poset) |
10 | | meetle.x |
. . . . 5
β’ (π β π β π΅) |
11 | | meetle.y |
. . . . 5
β’ (π β π β π΅) |
12 | | meetle.e |
. . . . 5
β’ (π β β¨π, πβ© β dom β§ ) |
13 | 6, 7, 8, 9, 10, 11, 12 | meetlem 18355 |
. . . 4
β’ (π β (((π β§ π) β€ π β§ (π β§ π) β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π)))) |
14 | 13 | simprd 495 |
. . 3
β’ (π β βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π))) |
15 | | meetle.z |
. . 3
β’ (π β π β π΅) |
16 | 5, 14, 15 | rspcdva 3613 |
. 2
β’ (π β ((π β€ π β§ π β€ π) β π β€ (π β§ π))) |
17 | 6, 7, 8, 9, 10, 11, 12 | lemeet1 18356 |
. . . 4
β’ (π β (π β§ π) β€ π) |
18 | 6, 8, 9, 10, 11, 12 | meetcl 18350 |
. . . . 5
β’ (π β (π β§ π) β π΅) |
19 | 6, 7 | postr 18278 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ (π β§ π) β π΅ β§ π β π΅)) β ((π β€ (π β§ π) β§ (π β§ π) β€ π) β π β€ π)) |
20 | 9, 15, 18, 10, 19 | syl13anc 1371 |
. . . 4
β’ (π β ((π β€ (π β§ π) β§ (π β§ π) β€ π) β π β€ π)) |
21 | 17, 20 | mpan2d 691 |
. . 3
β’ (π β (π β€ (π β§ π) β π β€ π)) |
22 | 6, 7, 8, 9, 10, 11, 12 | lemeet2 18357 |
. . . 4
β’ (π β (π β§ π) β€ π) |
23 | 6, 7 | postr 18278 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ (π β§ π) β π΅ β§ π β π΅)) β ((π β€ (π β§ π) β§ (π β§ π) β€ π) β π β€ π)) |
24 | 9, 15, 18, 11, 23 | syl13anc 1371 |
. . . 4
β’ (π β ((π β€ (π β§ π) β§ (π β§ π) β€ π) β π β€ π)) |
25 | 22, 24 | mpan2d 691 |
. . 3
β’ (π β (π β€ (π β§ π) β π β€ π)) |
26 | 21, 25 | jcad 512 |
. 2
β’ (π β (π β€ (π β§ π) β (π β€ π β§ π β€ π))) |
27 | 16, 26 | impbid 211 |
1
β’ (π β ((π β€ π β§ π β€ π) β π β€ (π β§ π))) |