Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
2 | | isdrs.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
3 | 1, 2 | eqtr4di 2791 |
. . . . 5
β’ (π = πΎ β (Baseβπ) = π΅) |
4 | | fveq2 6846 |
. . . . . . 7
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
5 | | isdrs.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΎ β (leβπ) = β€ ) |
7 | 6 | sbceq1d 3748 |
. . . . 5
β’ (π = πΎ β ([(leβπ) / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)) β [ β€ / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)))) |
8 | 3, 7 | sbceqbid 3750 |
. . . 4
β’ (π = πΎ β ([(Baseβπ) / π][(leβπ) / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)) β [π΅ / π][ β€ / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)))) |
9 | 2 | fvexi 6860 |
. . . . 5
β’ π΅ β V |
10 | 5 | fvexi 6860 |
. . . . 5
β’ β€ β
V |
11 | | neeq1 3003 |
. . . . . . 7
β’ (π = π΅ β (π β β
β π΅ β β
)) |
12 | 11 | adantr 482 |
. . . . . 6
β’ ((π = π΅ β§ π = β€ ) β (π β β
β π΅ β β
)) |
13 | | rexeq 3309 |
. . . . . . . . 9
β’ (π = π΅ β (βπ§ β π (π₯ππ§ β§ π¦ππ§) β βπ§ β π΅ (π₯ππ§ β§ π¦ππ§))) |
14 | 13 | raleqbi1dv 3306 |
. . . . . . . 8
β’ (π = π΅ β (βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§) β βπ¦ β π΅ βπ§ β π΅ (π₯ππ§ β§ π¦ππ§))) |
15 | 14 | raleqbi1dv 3306 |
. . . . . . 7
β’ (π = π΅ β (βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ππ§ β§ π¦ππ§))) |
16 | | breq 5111 |
. . . . . . . . . 10
β’ (π = β€ β (π₯ππ§ β π₯ β€ π§)) |
17 | | breq 5111 |
. . . . . . . . . 10
β’ (π = β€ β (π¦ππ§ β π¦ β€ π§)) |
18 | 16, 17 | anbi12d 632 |
. . . . . . . . 9
β’ (π = β€ β ((π₯ππ§ β§ π¦ππ§) β (π₯ β€ π§ β§ π¦ β€ π§))) |
19 | 18 | rexbidv 3172 |
. . . . . . . 8
β’ (π = β€ β (βπ§ β π΅ (π₯ππ§ β§ π¦ππ§) β βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§))) |
20 | 19 | 2ralbidv 3209 |
. . . . . . 7
β’ (π = β€ β (βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ππ§ β§ π¦ππ§) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§))) |
21 | 15, 20 | sylan9bb 511 |
. . . . . 6
β’ ((π = π΅ β§ π = β€ ) β (βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§))) |
22 | 12, 21 | anbi12d 632 |
. . . . 5
β’ ((π = π΅ β§ π = β€ ) β ((π β β
β§
βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)) β (π΅ β β
β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§)))) |
23 | 9, 10, 22 | sbc2ie 3826 |
. . . 4
β’
([π΅ / π][ β€ / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)) β (π΅ β β
β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§))) |
24 | 8, 23 | bitrdi 287 |
. . 3
β’ (π = πΎ β ([(Baseβπ) / π][(leβπ) / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§)) β (π΅ β β
β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§)))) |
25 | | df-drs 18193 |
. . 3
β’ Dirset =
{π β Proset β£
[(Baseβπ) /
π][(leβπ) / π](π β β
β§ βπ₯ β π βπ¦ β π βπ§ β π (π₯ππ§ β§ π¦ππ§))} |
26 | 24, 25 | elrab2 3652 |
. 2
β’ (πΎ β Dirset β (πΎ β Proset β§ (π΅ β β
β§
βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§)))) |
27 | | 3anass 1096 |
. 2
β’ ((πΎ β Proset β§ π΅ β β
β§
βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§)) β (πΎ β Proset β§ (π΅ β β
β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§)))) |
28 | 26, 27 | bitr4i 278 |
1
β’ (πΎ β Dirset β (πΎ β Proset β§ π΅ β β
β§
βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π§ β§ π¦ β€ π§))) |