Step | Hyp | Ref
| Expression |
1 | | isdrs.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | isdrs.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | 1, 2 | isdrs 18254 |
. . . 4
β’ (πΎ β Dirset β (πΎ β Proset β§ π΅ β β
β§
βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§))) |
4 | 3 | simp3bi 1148 |
. . 3
β’ (πΎ β Dirset β
βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§)) |
5 | | breq1 5152 |
. . . . . 6
β’ (π₯ = π β (π₯ β€ π§ β π β€ π§)) |
6 | 5 | anbi1d 631 |
. . . . 5
β’ (π₯ = π β ((π₯ β€ π§ β§ π¦ β€ π§) β (π β€ π§ β§ π¦ β€ π§))) |
7 | 6 | rexbidv 3179 |
. . . 4
β’ (π₯ = π β (βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§) β βπ§ β π΅ (π β€ π§ β§ π¦ β€ π§))) |
8 | | breq1 5152 |
. . . . . 6
β’ (π¦ = π β (π¦ β€ π§ β π β€ π§)) |
9 | 8 | anbi2d 630 |
. . . . 5
β’ (π¦ = π β ((π β€ π§ β§ π¦ β€ π§) β (π β€ π§ β§ π β€ π§))) |
10 | 9 | rexbidv 3179 |
. . . 4
β’ (π¦ = π β (βπ§ β π΅ (π β€ π§ β§ π¦ β€ π§) β βπ§ β π΅ (π β€ π§ β§ π β€ π§))) |
11 | 7, 10 | rspc2v 3623 |
. . 3
β’ ((π β π΅ β§ π β π΅) β (βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§) β βπ§ β π΅ (π β€ π§ β§ π β€ π§))) |
12 | 4, 11 | syl5com 31 |
. 2
β’ (πΎ β Dirset β ((π β π΅ β§ π β π΅) β βπ§ β π΅ (π β€ π§ β§ π β€ π§))) |
13 | 12 | 3impib 1117 |
1
β’ ((πΎ β Dirset β§ π β π΅ β§ π β π΅) β βπ§ β π΅ (π β€ π§ β§ π β€ π§)) |