Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2731 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
3 | | eqid 2731 |
. . 3
β’
(lubβπΎ) =
(lubβπΎ) |
4 | | biid 260 |
. . 3
β’
((βπ¦ β
π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§)) β (βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))) |
5 | | lubeldm2d.k |
. . 3
β’ (π β πΎ β Poset) |
6 | 1, 2, 3, 4, 5 | lubeldm2 47678 |
. 2
β’ (π β (π β dom (lubβπΎ) β (π β (BaseβπΎ) β§ βπ₯ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))))) |
7 | | lubeldm2d.u |
. . . 4
β’ (π β π = (lubβπΎ)) |
8 | 7 | dmeqd 5906 |
. . 3
β’ (π β dom π = dom (lubβπΎ)) |
9 | 8 | eleq2d 2818 |
. 2
β’ (π β (π β dom π β π β dom (lubβπΎ))) |
10 | | lubeldm2d.b |
. . . 4
β’ (π β π΅ = (BaseβπΎ)) |
11 | 10 | sseq2d 4015 |
. . 3
β’ (π β (π β π΅ β π β (BaseβπΎ))) |
12 | | lubeldm2d.p |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
13 | | lubeldm2d.l |
. . . . . . . . . . 11
β’ (π β β€ = (leβπΎ)) |
14 | 13 | breqd 5160 |
. . . . . . . . . 10
β’ (π β (π¦ β€ π₯ β π¦(leβπΎ)π₯)) |
15 | 14 | ralbidv 3176 |
. . . . . . . . 9
β’ (π β (βπ¦ β π π¦ β€ π₯ β βπ¦ β π π¦(leβπΎ)π₯)) |
16 | 13 | breqd 5160 |
. . . . . . . . . . . 12
β’ (π β (π¦ β€ π§ β π¦(leβπΎ)π§)) |
17 | 16 | ralbidv 3176 |
. . . . . . . . . . 11
β’ (π β (βπ¦ β π π¦ β€ π§ β βπ¦ β π π¦(leβπΎ)π§)) |
18 | 13 | breqd 5160 |
. . . . . . . . . . 11
β’ (π β (π₯ β€ π§ β π₯(leβπΎ)π§)) |
19 | 17, 18 | imbi12d 343 |
. . . . . . . . . 10
β’ (π β ((βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β (βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))) |
20 | 10, 19 | raleqbidv 3341 |
. . . . . . . . 9
β’ (π β (βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))) |
21 | 15, 20 | anbi12d 630 |
. . . . . . . 8
β’ (π β ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§)))) |
22 | 21 | adantr 480 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§)))) |
23 | 12, 22 | bitrd 278 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β (π β (βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§)))) |
24 | 23 | pm5.32da 578 |
. . . . 5
β’ (π β ((π₯ β π΅ β§ π) β (π₯ β π΅ β§ (βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))))) |
25 | 10 | eleq2d 2818 |
. . . . . 6
β’ (π β (π₯ β π΅ β π₯ β (BaseβπΎ))) |
26 | 25 | anbi1d 629 |
. . . . 5
β’ (π β ((π₯ β π΅ β§ (βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))) β (π₯ β (BaseβπΎ) β§ (βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))))) |
27 | 24, 26 | bitrd 278 |
. . . 4
β’ (π β ((π₯ β π΅ β§ π) β (π₯ β (BaseβπΎ) β§ (βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))))) |
28 | 27 | rexbidv2 3173 |
. . 3
β’ (π β (βπ₯ β π΅ π β βπ₯ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§)))) |
29 | 11, 28 | anbi12d 630 |
. 2
β’ (π β ((π β π΅ β§ βπ₯ β π΅ π) β (π β (BaseβπΎ) β§ βπ₯ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π₯ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π¦(leβπΎ)π§ β π₯(leβπΎ)π§))))) |
30 | 6, 9, 29 | 3bitr4d 310 |
1
β’ (π β (π β dom π β (π β π΅ β§ βπ₯ β π΅ π))) |