Step | Hyp | Ref
| Expression |
1 | | vex 3450 |
. . . . 5
β’ π₯ β V |
2 | | f1eq1 6734 |
. . . . 5
β’ (β = π₯ β (β:π΄β1-1βπ΄ β π₯:π΄β1-1βπ΄)) |
3 | 1, 2 | elab 3631 |
. . . 4
β’ (π₯ β {β β£ β:π΄β1-1βπ΄} β π₯:π΄β1-1βπ΄) |
4 | | f1f 6739 |
. . . . 5
β’ (π₯:π΄β1-1βπ΄ β π₯:π΄βΆπ΄) |
5 | | sursubmefmnd.m |
. . . . . 6
β’ π = (EndoFMndβπ΄) |
6 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
7 | 5, 6 | elefmndbas 18684 |
. . . . 5
β’ (π΄ β π β (π₯ β (Baseβπ) β π₯:π΄βΆπ΄)) |
8 | 4, 7 | syl5ibr 246 |
. . . 4
β’ (π΄ β π β (π₯:π΄β1-1βπ΄ β π₯ β (Baseβπ))) |
9 | 3, 8 | biimtrid 241 |
. . 3
β’ (π΄ β π β (π₯ β {β β£ β:π΄β1-1βπ΄} β π₯ β (Baseβπ))) |
10 | 9 | ssrdv 3951 |
. 2
β’ (π΄ β π β {β β£ β:π΄β1-1βπ΄} β (Baseβπ)) |
11 | 5 | efmndid 18699 |
. . 3
β’ (π΄ β π β ( I βΎ π΄) = (0gβπ)) |
12 | | resiexg 7852 |
. . . 4
β’ (π΄ β π β ( I βΎ π΄) β V) |
13 | | f1oi 6823 |
. . . . 5
β’ ( I
βΎ π΄):π΄β1-1-ontoβπ΄ |
14 | | f1of1 6784 |
. . . . 5
β’ (( I
βΎ π΄):π΄β1-1-ontoβπ΄ β ( I βΎ π΄):π΄β1-1βπ΄) |
15 | 13, 14 | mp1i 13 |
. . . 4
β’ (π΄ β π β ( I βΎ π΄):π΄β1-1βπ΄) |
16 | | f1eq1 6734 |
. . . 4
β’ (β = ( I βΎ π΄) β (β:π΄β1-1βπ΄ β ( I βΎ π΄):π΄β1-1βπ΄)) |
17 | 12, 15, 16 | elabd 3634 |
. . 3
β’ (π΄ β π β ( I βΎ π΄) β {β β£ β:π΄β1-1βπ΄}) |
18 | 11, 17 | eqeltrrd 2839 |
. 2
β’ (π΄ β π β (0gβπ) β {β β£ β:π΄β1-1βπ΄}) |
19 | | vex 3450 |
. . . . . 6
β’ π¦ β V |
20 | | f1eq1 6734 |
. . . . . 6
β’ (β = π¦ β (β:π΄β1-1βπ΄ β π¦:π΄β1-1βπ΄)) |
21 | 19, 20 | elab 3631 |
. . . . 5
β’ (π¦ β {β β£ β:π΄β1-1βπ΄} β π¦:π΄β1-1βπ΄) |
22 | 3, 21 | anbi12i 628 |
. . . 4
β’ ((π₯ β {β β£ β:π΄β1-1βπ΄} β§ π¦ β {β β£ β:π΄β1-1βπ΄}) β (π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄)) |
23 | | f1co 6751 |
. . . . . . 7
β’ ((π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄) β (π₯ β π¦):π΄β1-1βπ΄) |
24 | 23 | adantl 483 |
. . . . . 6
β’ ((π΄ β π β§ (π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄)) β (π₯ β π¦):π΄β1-1βπ΄) |
25 | | f1f 6739 |
. . . . . . . . . . . 12
β’ (π¦:π΄β1-1βπ΄ β π¦:π΄βΆπ΄) |
26 | 4, 25 | anim12i 614 |
. . . . . . . . . . 11
β’ ((π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄) β (π₯:π΄βΆπ΄ β§ π¦:π΄βΆπ΄)) |
27 | 5, 6 | elefmndbas 18684 |
. . . . . . . . . . . 12
β’ (π΄ β π β (π¦ β (Baseβπ) β π¦:π΄βΆπ΄)) |
28 | 7, 27 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π΄ β π β ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯:π΄βΆπ΄ β§ π¦:π΄βΆπ΄))) |
29 | 26, 28 | syl5ibr 246 |
. . . . . . . . . 10
β’ (π΄ β π β ((π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄) β (π₯ β (Baseβπ) β§ π¦ β (Baseβπ)))) |
30 | 29 | imp 408 |
. . . . . . . . 9
β’ ((π΄ β π β§ (π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄)) β (π₯ β (Baseβπ) β§ π¦ β (Baseβπ))) |
31 | | eqid 2737 |
. . . . . . . . . 10
β’
(+gβπ) = (+gβπ) |
32 | 5, 6, 31 | efmndov 18692 |
. . . . . . . . 9
β’ ((π₯ β (Baseβπ) β§ π¦ β (Baseβπ)) β (π₯(+gβπ)π¦) = (π₯ β π¦)) |
33 | 30, 32 | syl 17 |
. . . . . . . 8
β’ ((π΄ β π β§ (π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄)) β (π₯(+gβπ)π¦) = (π₯ β π¦)) |
34 | 33 | eleq1d 2823 |
. . . . . . 7
β’ ((π΄ β π β§ (π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄)) β ((π₯(+gβπ)π¦) β {β β£ β:π΄β1-1βπ΄} β (π₯ β π¦) β {β β£ β:π΄β1-1βπ΄})) |
35 | 1, 19 | coex 7868 |
. . . . . . . 8
β’ (π₯ β π¦) β V |
36 | | f1eq1 6734 |
. . . . . . . 8
β’ (β = (π₯ β π¦) β (β:π΄β1-1βπ΄ β (π₯ β π¦):π΄β1-1βπ΄)) |
37 | 35, 36 | elab 3631 |
. . . . . . 7
β’ ((π₯ β π¦) β {β β£ β:π΄β1-1βπ΄} β (π₯ β π¦):π΄β1-1βπ΄) |
38 | 34, 37 | bitrdi 287 |
. . . . . 6
β’ ((π΄ β π β§ (π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄)) β ((π₯(+gβπ)π¦) β {β β£ β:π΄β1-1βπ΄} β (π₯ β π¦):π΄β1-1βπ΄)) |
39 | 24, 38 | mpbird 257 |
. . . . 5
β’ ((π΄ β π β§ (π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄)) β (π₯(+gβπ)π¦) β {β β£ β:π΄β1-1βπ΄}) |
40 | 39 | ex 414 |
. . . 4
β’ (π΄ β π β ((π₯:π΄β1-1βπ΄ β§ π¦:π΄β1-1βπ΄) β (π₯(+gβπ)π¦) β {β β£ β:π΄β1-1βπ΄})) |
41 | 22, 40 | biimtrid 241 |
. . 3
β’ (π΄ β π β ((π₯ β {β β£ β:π΄β1-1βπ΄} β§ π¦ β {β β£ β:π΄β1-1βπ΄}) β (π₯(+gβπ)π¦) β {β β£ β:π΄β1-1βπ΄})) |
42 | 41 | ralrimivv 3196 |
. 2
β’ (π΄ β π β βπ₯ β {β β£ β:π΄β1-1βπ΄}βπ¦ β {β β£ β:π΄β1-1βπ΄} (π₯(+gβπ)π¦) β {β β£ β:π΄β1-1βπ΄}) |
43 | 5 | efmndmnd 18700 |
. . 3
β’ (π΄ β π β π β Mnd) |
44 | | eqid 2737 |
. . . 4
β’
(0gβπ) = (0gβπ) |
45 | 6, 44, 31 | issubm 18615 |
. . 3
β’ (π β Mnd β ({β β£ β:π΄β1-1βπ΄} β (SubMndβπ) β ({β β£ β:π΄β1-1βπ΄} β (Baseβπ) β§ (0gβπ) β {β β£ β:π΄β1-1βπ΄} β§ βπ₯ β {β β£ β:π΄β1-1βπ΄}βπ¦ β {β β£ β:π΄β1-1βπ΄} (π₯(+gβπ)π¦) β {β β£ β:π΄β1-1βπ΄}))) |
46 | 43, 45 | syl 17 |
. 2
β’ (π΄ β π β ({β β£ β:π΄β1-1βπ΄} β (SubMndβπ) β ({β β£ β:π΄β1-1βπ΄} β (Baseβπ) β§ (0gβπ) β {β β£ β:π΄β1-1βπ΄} β§ βπ₯ β {β β£ β:π΄β1-1βπ΄}βπ¦ β {β β£ β:π΄β1-1βπ΄} (π₯(+gβπ)π¦) β {β β£ β:π΄β1-1βπ΄}))) |
47 | 10, 18, 42, 46 | mpbir3and 1343 |
1
β’ (π΄ β π β {β β£ β:π΄β1-1βπ΄} β (SubMndβπ)) |