| Step | Hyp | Ref
| Expression |
|---|
| 1 | | meetval2.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
| 2 | | meetval2.l |
. . . . 5
β’ β€ =
(leβπΎ) |
| 3 | | meetval2.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
| 4 | | meetval2.k |
. . . . 5
β’ (π β πΎ β π) |
| 5 | | meetval2.x |
. . . . 5
β’ (π β π β π΅) |
| 6 | | meetval2.y |
. . . . 5
β’ (π β π β π΅) |
| 7 | | meetlem.e |
. . . . 5
β’ (π β β¨π, πβ© β dom β§ ) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | meeteu 18328 |
. . . 4
β’ (π β β!π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯))) |
| 9 | | riotasbc 7365 |
. . . 4
β’
(β!π₯ β
π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)) β [(β©π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯))) / π₯]((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯))) |
| 10 | 8, 9 | syl 17 |
. . 3
β’ (π β
[(β©π₯
β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯))) / π₯]((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯))) |
| 11 | 1, 2, 3, 4, 5, 6 | meetval2 18327 |
. . . 4
β’ (π β (π β§ π) = (β©π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)))) |
| 12 | 11 | sbceq1d 3775 |
. . 3
β’ (π β ([(π β§ π) / π₯]((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)) β [(β©π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯))) / π₯]((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)))) |
| 13 | 10, 12 | mpbird 256 |
. 2
β’ (π β [(π β§ π) / π₯]((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯))) |
| 14 | | ovex 7423 |
. . 3
β’ (π β§ π) β V |
| 15 | | breq1 5141 |
. . . . 5
β’ (π₯ = (π β§ π) β (π₯ β€ π β (π β§ π) β€ π)) |
| 16 | | breq1 5141 |
. . . . 5
β’ (π₯ = (π β§ π) β (π₯ β€ π β (π β§ π) β€ π)) |
| 17 | 15, 16 | anbi12d 631 |
. . . 4
β’ (π₯ = (π β§ π) β ((π₯ β€ π β§ π₯ β€ π) β ((π β§ π) β€ π β§ (π β§ π) β€ π))) |
| 18 | | breq2 5142 |
. . . . . 6
β’ (π₯ = (π β§ π) β (π§ β€ π₯ β π§ β€ (π β§ π))) |
| 19 | 18 | imbi2d 340 |
. . . . 5
β’ (π₯ = (π β§ π) β (((π§ β€ π β§ π§ β€ π) β π§ β€ π₯) β ((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π)))) |
| 20 | 19 | ralbidv 3176 |
. . . 4
β’ (π₯ = (π β§ π) β (βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯) β βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π)))) |
| 21 | 17, 20 | anbi12d 631 |
. . 3
β’ (π₯ = (π β§ π) β (((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)) β (((π β§ π) β€ π β§ (π β§ π) β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π))))) |
| 22 | 14, 21 | sbcie 3813 |
. 2
β’
([(π β§ π) / π₯]((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)) β (((π β§ π) β€ π β§ (π β§ π) β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π)))) |
| 23 | 13, 22 | sylib 217 |
1
β’ (π β (((π β§ π) β€ π β§ (π β§ π) β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ (π β§ π)))) |
