Step | Hyp | Ref
| Expression |
1 | | breq2 5153 |
. . . . 5
β’ (π§ = π β (π β€ π§ β π β€ π)) |
2 | | breq2 5153 |
. . . . 5
β’ (π§ = π β (π β€ π§ β π β€ π)) |
3 | 1, 2 | anbi12d 632 |
. . . 4
β’ (π§ = π β ((π β€ π§ β§ π β€ π§) β (π β€ π β§ π β€ π))) |
4 | | breq2 5153 |
. . . 4
β’ (π§ = π β ((π β¨ π) β€ π§ β (π β¨ π) β€ π)) |
5 | 3, 4 | imbi12d 345 |
. . 3
β’ (π§ = π β (((π β€ π§ β§ π β€ π§) β (π β¨ π) β€ π§) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π))) |
6 | | joinle.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
7 | | joinle.l |
. . . . 5
β’ β€ =
(leβπΎ) |
8 | | joinle.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
9 | | joinle.k |
. . . . 5
β’ (π β πΎ β Poset) |
10 | | joinle.x |
. . . . 5
β’ (π β π β π΅) |
11 | | joinle.y |
. . . . 5
β’ (π β π β π΅) |
12 | | joinle.e |
. . . . 5
β’ (π β β¨π, πβ© β dom β¨ ) |
13 | 6, 7, 8, 9, 10, 11, 12 | joinlem 18336 |
. . . 4
β’ (π β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ βπ§ β π΅ ((π β€ π§ β§ π β€ π§) β (π β¨ π) β€ π§))) |
14 | 13 | simprd 497 |
. . 3
β’ (π β βπ§ β π΅ ((π β€ π§ β§ π β€ π§) β (π β¨ π) β€ π§)) |
15 | | joinle.z |
. . 3
β’ (π β π β π΅) |
16 | 5, 14, 15 | rspcdva 3614 |
. 2
β’ (π β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
17 | 6, 7, 8, 9, 10, 11, 12 | lejoin1 18337 |
. . . 4
β’ (π β π β€ (π β¨ π)) |
18 | 6, 8, 9, 10, 11, 12 | joincl 18331 |
. . . . 5
β’ (π β (π β¨ π) β π΅) |
19 | 6, 7 | postr 18273 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ (π β¨ π) β π΅ β§ π β π΅)) β ((π β€ (π β¨ π) β§ (π β¨ π) β€ π) β π β€ π)) |
20 | 9, 10, 18, 15, 19 | syl13anc 1373 |
. . . 4
β’ (π β ((π β€ (π β¨ π) β§ (π β¨ π) β€ π) β π β€ π)) |
21 | 17, 20 | mpand 694 |
. . 3
β’ (π β ((π β¨ π) β€ π β π β€ π)) |
22 | 6, 7, 8, 9, 10, 11, 12 | lejoin2 18338 |
. . . 4
β’ (π β π β€ (π β¨ π)) |
23 | 6, 7 | postr 18273 |
. . . . 5
β’ ((πΎ β Poset β§ (π β π΅ β§ (π β¨ π) β π΅ β§ π β π΅)) β ((π β€ (π β¨ π) β§ (π β¨ π) β€ π) β π β€ π)) |
24 | 9, 11, 18, 15, 23 | syl13anc 1373 |
. . . 4
β’ (π β ((π β€ (π β¨ π) β§ (π β¨ π) β€ π) β π β€ π)) |
25 | 22, 24 | mpand 694 |
. . 3
β’ (π β ((π β¨ π) β€ π β π β€ π)) |
26 | 21, 25 | jcad 514 |
. 2
β’ (π β ((π β¨ π) β€ π β (π β€ π β§ π β€ π))) |
27 | 16, 26 | impbid 211 |
1
β’ (π β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |