Step | Hyp | Ref
| Expression |
1 | | isprsd.k |
. . . 4
β’ (π β πΎ β π) |
2 | 1 | elexd 3495 |
. . 3
β’ (π β πΎ β V) |
3 | | eqid 2733 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
4 | | eqid 2733 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
5 | 3, 4 | isprs 18250 |
. . . 4
β’ (πΎ β Proset β (πΎ β V β§ βπ₯ β (BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
6 | 5 | baib 537 |
. . 3
β’ (πΎ β V β (πΎ β Proset β
βπ₯ β
(BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
7 | 2, 6 | syl 17 |
. 2
β’ (π β (πΎ β Proset β βπ₯ β (BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
8 | | isprsd.b |
. . 3
β’ (π β π΅ = (BaseβπΎ)) |
9 | | isprsd.l |
. . . . . . 7
β’ (π β β€ = (leβπΎ)) |
10 | 9 | breqd 5160 |
. . . . . 6
β’ (π β (π₯ β€ π₯ β π₯(leβπΎ)π₯)) |
11 | 9 | breqd 5160 |
. . . . . . . 8
β’ (π β (π₯ β€ π¦ β π₯(leβπΎ)π¦)) |
12 | 9 | breqd 5160 |
. . . . . . . 8
β’ (π β (π¦ β€ π§ β π¦(leβπΎ)π§)) |
13 | 11, 12 | anbi12d 632 |
. . . . . . 7
β’ (π β ((π₯ β€ π¦ β§ π¦ β€ π§) β (π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§))) |
14 | 9 | breqd 5160 |
. . . . . . 7
β’ (π β (π₯ β€ π§ β π₯(leβπΎ)π§)) |
15 | 13, 14 | imbi12d 345 |
. . . . . 6
β’ (π β (((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§) β ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§))) |
16 | 10, 15 | anbi12d 632 |
. . . . 5
β’ (π β ((π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β (π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
17 | 8, 16 | raleqbidv 3343 |
. . . 4
β’ (π β (βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
18 | 8, 17 | raleqbidv 3343 |
. . 3
β’ (π β (βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
19 | 8, 18 | raleqbidv 3343 |
. 2
β’ (π β (βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)) β βπ₯ β (BaseβπΎ)βπ¦ β (BaseβπΎ)βπ§ β (BaseβπΎ)(π₯(leβπΎ)π₯ β§ ((π₯(leβπΎ)π¦ β§ π¦(leβπΎ)π§) β π₯(leβπΎ)π§)))) |
20 | 7, 19 | bitr4d 282 |
1
β’ (π β (πΎ β Proset β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ β€ π₯ β§ ((π₯ β€ π¦ β§ π¦ β€ π§) β π₯ β€ π§)))) |