Step | Hyp | Ref
| Expression |
1 | | elex 3465 |
. 2
β’ (πΎ β π΄ β πΎ β V) |
2 | | lautset.i |
. . 3
β’ πΌ = (LAutβπΎ) |
3 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
4 | | lautset.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΎ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = πΎ β (Baseβπ) = π΅) |
6 | 5 | f1oeq2d 6784 |
. . . . . . 7
β’ (π = πΎ β (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β π:π΅β1-1-ontoβ(Baseβπ))) |
7 | | f1oeq3 6778 |
. . . . . . . 8
β’
((Baseβπ) =
π΅ β (π:π΅β1-1-ontoβ(Baseβπ) β π:π΅β1-1-ontoβπ΅)) |
8 | 5, 7 | syl 17 |
. . . . . . 7
β’ (π = πΎ β (π:π΅β1-1-ontoβ(Baseβπ) β π:π΅β1-1-ontoβπ΅)) |
9 | 6, 8 | bitrd 279 |
. . . . . 6
β’ (π = πΎ β (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β π:π΅β1-1-ontoβπ΅)) |
10 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
11 | | lautset.l |
. . . . . . . . . . 11
β’ β€ =
(leβπΎ) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π = πΎ β (leβπ) = β€ ) |
13 | 12 | breqd 5120 |
. . . . . . . . 9
β’ (π = πΎ β (π₯(leβπ)π¦ β π₯ β€ π¦)) |
14 | 12 | breqd 5120 |
. . . . . . . . 9
β’ (π = πΎ β ((πβπ₯)(leβπ)(πβπ¦) β (πβπ₯) β€ (πβπ¦))) |
15 | 13, 14 | bibi12d 346 |
. . . . . . . 8
β’ (π = πΎ β ((π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)) β (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))) |
16 | 5, 15 | raleqbidv 3318 |
. . . . . . 7
β’ (π = πΎ β (βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)) β βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))) |
17 | 5, 16 | raleqbidv 3318 |
. . . . . 6
β’ (π = πΎ β (βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)) β βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))) |
18 | 9, 17 | anbi12d 632 |
. . . . 5
β’ (π = πΎ β ((π:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦))) β (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦))))) |
19 | 18 | abbidv 2802 |
. . . 4
β’ (π = πΎ β {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)))} = {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))}) |
20 | | df-laut 38502 |
. . . 4
β’ LAut =
(π β V β¦ {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)))}) |
21 | 4 | fvexi 6860 |
. . . . . . . 8
β’ π΅ β V |
22 | 21, 21 | mapval 8783 |
. . . . . . 7
β’ (π΅ βm π΅) = {π β£ π:π΅βΆπ΅} |
23 | | ovex 7394 |
. . . . . . 7
β’ (π΅ βm π΅) β V |
24 | 22, 23 | eqeltrri 2831 |
. . . . . 6
β’ {π β£ π:π΅βΆπ΅} β V |
25 | | f1of 6788 |
. . . . . . 7
β’ (π:π΅β1-1-ontoβπ΅ β π:π΅βΆπ΅) |
26 | 25 | ss2abi 4027 |
. . . . . 6
β’ {π β£ π:π΅β1-1-ontoβπ΅} β {π β£ π:π΅βΆπ΅} |
27 | 24, 26 | ssexi 5283 |
. . . . 5
β’ {π β£ π:π΅β1-1-ontoβπ΅} β V |
28 | | simpl 484 |
. . . . . 6
β’ ((π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦))) β π:π΅β1-1-ontoβπ΅) |
29 | 28 | ss2abi 4027 |
. . . . 5
β’ {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))} β {π β£ π:π΅β1-1-ontoβπ΅} |
30 | 27, 29 | ssexi 5283 |
. . . 4
β’ {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))} β V |
31 | 19, 20, 30 | fvmpt 6952 |
. . 3
β’ (πΎ β V β
(LAutβπΎ) = {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))}) |
32 | 2, 31 | eqtrid 2785 |
. 2
β’ (πΎ β V β πΌ = {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))}) |
33 | 1, 32 | syl 17 |
1
β’ (πΎ β π΄ β πΌ = {π β£ (π:π΅β1-1-ontoβπ΅ β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ β€ π¦ β (πβπ₯) β€ (πβπ¦)))}) |