Step | Hyp | Ref
| Expression |
1 | | lubprop.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | lubprop.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | lubprop.u |
. . . 4
β’ π = (lubβπΎ) |
4 | | biid 260 |
. . . 4
β’
((βπ¦ β
π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
5 | | lubprop.k |
. . . 4
β’ (π β πΎ β π) |
6 | | lubprop.s |
. . . . 5
β’ (π β π β dom π) |
7 | 1, 2, 3, 5, 6 | lubelss 18169 |
. . . 4
β’ (π β π β π΅) |
8 | 1, 2, 3, 4, 5, 7 | lubval 18171 |
. . 3
β’ (π β (πβπ) = (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
9 | 8 | eqcomd 2742 |
. 2
β’ (π β (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) = (πβπ)) |
10 | 1, 3, 5, 6 | lubcl 18172 |
. . 3
β’ (π β (πβπ) β π΅) |
11 | 1, 2, 3, 4, 5, 6 | lubeu 18170 |
. . 3
β’ (π β β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
12 | | breq2 5096 |
. . . . . 6
β’ (π₯ = (πβπ) β (π¦ β€ π₯ β π¦ β€ (πβπ))) |
13 | 12 | ralbidv 3170 |
. . . . 5
β’ (π₯ = (πβπ) β (βπ¦ β π π¦ β€ π₯ β βπ¦ β π π¦ β€ (πβπ))) |
14 | | breq1 5095 |
. . . . . . 7
β’ (π₯ = (πβπ) β (π₯ β€ π§ β (πβπ) β€ π§)) |
15 | 14 | imbi2d 340 |
. . . . . 6
β’ (π₯ = (πβπ) β ((βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§))) |
16 | 15 | ralbidv 3170 |
. . . . 5
β’ (π₯ = (πβπ) β (βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§))) |
17 | 13, 16 | anbi12d 631 |
. . . 4
β’ (π₯ = (πβπ) β ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦ β€ (πβπ) β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§)))) |
18 | 17 | riota2 7319 |
. . 3
β’ (((πβπ) β π΅ β§ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) β ((βπ¦ β π π¦ β€ (πβπ) β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§)) β (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) = (πβπ))) |
19 | 10, 11, 18 | syl2anc 584 |
. 2
β’ (π β ((βπ¦ β π π¦ β€ (πβπ) β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§)) β (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) = (πβπ))) |
20 | 9, 19 | mpbird 256 |
1
β’ (π β (βπ¦ β π π¦ β€ (πβπ) β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β (πβπ) β€ π§))) |