Step | Hyp | Ref
| Expression |
1 | | tosglb.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | tosglb.l |
. . . . 5
β’ < =
(ltβπΎ) |
3 | | tosglb.1 |
. . . . 5
β’ (π β πΎ β Toset) |
4 | | tosglb.2 |
. . . . 5
β’ (π β π΄ β π΅) |
5 | | eqid 2733 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
6 | 1, 2, 3, 4, 5 | tosglblem 31883 |
. . . 4
β’ ((π β§ π β π΅) β ((βπ β π΄ π(leβπΎ)π β§ βπ β π΅ (βπ β π΄ π(leβπΎ)π β π(leβπΎ)π)) β (βπ β π΄ Β¬ πβ‘
<
π β§ βπ β π΅ (πβ‘
<
π β βπ β π΄ πβ‘
<
π)))) |
7 | 6 | riotabidva 7334 |
. . 3
β’ (π β (β©π β π΅ (βπ β π΄ π(leβπΎ)π β§ βπ β π΅ (βπ β π΄ π(leβπΎ)π β π(leβπΎ)π))) = (β©π β π΅ (βπ β π΄ Β¬ πβ‘
<
π β§ βπ β π΅ (πβ‘
<
π β βπ β π΄ πβ‘
<
π)))) |
8 | | eqid 2733 |
. . . 4
β’
(glbβπΎ) =
(glbβπΎ) |
9 | | biid 261 |
. . . 4
β’
((βπ β
π΄ π(leβπΎ)π β§ βπ β π΅ (βπ β π΄ π(leβπΎ)π β π(leβπΎ)π)) β (βπ β π΄ π(leβπΎ)π β§ βπ β π΅ (βπ β π΄ π(leβπΎ)π β π(leβπΎ)π))) |
10 | 1, 5, 8, 9, 3, 4 | glbval 18263 |
. . 3
β’ (π β ((glbβπΎ)βπ΄) = (β©π β π΅ (βπ β π΄ π(leβπΎ)π β§ βπ β π΅ (βπ β π΄ π(leβπΎ)π β π(leβπΎ)π)))) |
11 | 1, 5, 2 | tosso 18313 |
. . . . . . 7
β’ (πΎ β Toset β (πΎ β Toset β ( < Or π΅ β§ ( I βΎ π΅) β (leβπΎ)))) |
12 | 11 | ibi 267 |
. . . . . 6
β’ (πΎ β Toset β ( < Or π΅ β§ ( I βΎ π΅) β (leβπΎ))) |
13 | 12 | simpld 496 |
. . . . 5
β’ (πΎ β Toset β < Or π΅) |
14 | | cnvso 6241 |
. . . . 5
β’ ( < Or π΅ β β‘ < Or π΅) |
15 | 13, 14 | sylib 217 |
. . . 4
β’ (πΎ β Toset β β‘ < Or π΅) |
16 | | id 22 |
. . . . 5
β’ (β‘ < Or π΅ β β‘ < Or π΅) |
17 | 16 | supval2 9396 |
. . . 4
β’ (β‘ < Or π΅ β sup(π΄, π΅, β‘
< ) =
(β©π β
π΅ (βπ β π΄ Β¬ πβ‘
<
π β§ βπ β π΅ (πβ‘
<
π β βπ β π΄ πβ‘
<
π)))) |
18 | 3, 15, 17 | 3syl 18 |
. . 3
β’ (π β sup(π΄, π΅, β‘
< ) =
(β©π β
π΅ (βπ β π΄ Β¬ πβ‘
<
π β§ βπ β π΅ (πβ‘
<
π β βπ β π΄ πβ‘
<
π)))) |
19 | 7, 10, 18 | 3eqtr4d 2783 |
. 2
β’ (π β ((glbβπΎ)βπ΄) = sup(π΄, π΅, β‘
<
)) |
20 | | df-inf 9384 |
. . . 4
β’ inf(π΄, π΅, < ) = sup(π΄, π΅, β‘
<
) |
21 | 20 | eqcomi 2742 |
. . 3
β’ sup(π΄, π΅, β‘
< ) =
inf(π΄, π΅, < ) |
22 | 21 | a1i 11 |
. 2
β’ (π β sup(π΄, π΅, β‘
< ) =
inf(π΄, π΅, < )) |
23 | 19, 22 | eqtrd 2773 |
1
β’ (π β ((glbβπΎ)βπ΄) = inf(π΄, π΅, < )) |