Step | Hyp | Ref
| Expression |
1 | | lautset.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | lautset.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | lautset.i |
. . . 4
β’ πΌ = (LAutβπΎ) |
4 | 1, 2, 3 | lautset 38591 |
. . 3
β’ (πΎ β π΄ β πΌ = {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))}) |
5 | 4 | eleq2d 2820 |
. 2
β’ (πΎ β π΄ β (πΉ β πΌ β πΉ β {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))})) |
6 | | f1of 6785 |
. . . . 5
β’ (πΉ:π΅β1-1-ontoβπ΅ β πΉ:π΅βΆπ΅) |
7 | 1 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
8 | | fex 7177 |
. . . . 5
β’ ((πΉ:π΅βΆπ΅ β§ π΅ β V) β πΉ β V) |
9 | 6, 7, 8 | sylancl 587 |
. . . 4
β’ (πΉ:π΅β1-1-ontoβπ΅ β πΉ β V) |
10 | 9 | adantr 482 |
. . 3
β’ ((πΉ:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))) β πΉ β V) |
11 | | f1oeq1 6773 |
. . . 4
β’ (π = πΉ β (π:π΅β1-1-ontoβπ΅ β πΉ:π΅β1-1-ontoβπ΅)) |
12 | | fveq1 6842 |
. . . . . . 7
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
13 | | fveq1 6842 |
. . . . . . 7
β’ (π = πΉ β (πβπ¦) = (πΉβπ¦)) |
14 | 12, 13 | breq12d 5119 |
. . . . . 6
β’ (π = πΉ β ((πβπ₯) β€ (πβπ¦) β (πΉβπ₯) β€ (πΉβπ¦))) |
15 | 14 | bibi2d 343 |
. . . . 5
β’ (π = πΉ β ((π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)) β (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)))) |
16 | 15 | 2ralbidv 3209 |
. . . 4
β’ (π = πΉ β (βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)) β βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)))) |
17 | 11, 16 | anbi12d 632 |
. . 3
β’ (π = πΉ β ((π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦))) β (πΉ:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))))) |
18 | 10, 17 | elab3 3639 |
. 2
β’ (πΉ β {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))} β (πΉ:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)))) |
19 | 5, 18 | bitrdi 287 |
1
β’ (πΎ β π΄ β (πΉ β πΌ β (πΉ:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦))))) |