Step | Hyp | Ref
| Expression |
1 | | fprodcl2lem.5 |
. . . 4
β’ (π β π΄ β β
) |
2 | 1 | a1d 25 |
. . 3
β’ (π β (Β¬ βπ β π΄ π΅ β π β π΄ β β
)) |
3 | 2 | necon4bd 2964 |
. 2
β’ (π β (π΄ = β
β βπ β π΄ π΅ β π)) |
4 | | prodfc 15835 |
. . . . . . 7
β’
βπ β
π΄ ((π β π΄ β¦ π΅)βπ) = βπ β π΄ π΅ |
5 | | fveq2 6847 |
. . . . . . . 8
β’ (π = (πβπ₯) β ((π β π΄ β¦ π΅)βπ) = ((π β π΄ β¦ π΅)β(πβπ₯))) |
6 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
β) |
7 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))β1-1-ontoβπ΄) |
8 | | fprodcllem.1 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
9 | 8 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π β β) |
10 | | fprodcllem.4 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΄) β π΅ β π) |
11 | 9, 10 | sseldd 3950 |
. . . . . . . . . . 11
β’ ((π β§ π β π΄) β π΅ β β) |
12 | 11 | fmpttd 7068 |
. . . . . . . . . 10
β’ (π β (π β π΄ β¦ π΅):π΄βΆβ) |
13 | 12 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
14 | 13 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π β π΄) β ((π β π΄ β¦ π΅)βπ) β β) |
15 | | f1of 6789 |
. . . . . . . . . 10
β’ (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β π:(1...(β―βπ΄))βΆπ΄) |
16 | 15 | ad2antll 728 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β π:(1...(β―βπ΄))βΆπ΄) |
17 | | fvco3 6945 |
. . . . . . . . 9
β’ ((π:(1...(β―βπ΄))βΆπ΄ β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ₯) = ((π β π΄ β¦ π΅)β(πβπ₯))) |
18 | 16, 17 | sylan 581 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ₯) = ((π β π΄ β¦ π΅)β(πβπ₯))) |
19 | 5, 6, 7, 14, 18 | fprod 15831 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ ((π β π΄ β¦ π΅)βπ) = (seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
20 | 4, 19 | eqtr3id 2791 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ π΅ = (seq1( Β· , ((π β π΄ β¦ π΅) β π))β(β―βπ΄))) |
21 | | nnuz 12813 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
22 | 6, 21 | eleqtrdi 2848 |
. . . . . . 7
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (β―βπ΄) β
(β€β₯β1)) |
23 | 10 | fmpttd 7068 |
. . . . . . . . 9
β’ (π β (π β π΄ β¦ π΅):π΄βΆπ) |
24 | | fco 6697 |
. . . . . . . . 9
β’ (((π β π΄ β¦ π΅):π΄βΆπ β§ π:(1...(β―βπ΄))βΆπ΄) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆπ) |
25 | 23, 16, 24 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β ((π β π΄ β¦ π΅) β π):(1...(β―βπ΄))βΆπ) |
26 | 25 | ffvelcdmda 7040 |
. . . . . . 7
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ π₯ β (1...(β―βπ΄))) β (((π β π΄ β¦ π΅) β π)βπ₯) β π) |
27 | | fprodcllem.2 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) |
28 | 27 | adantlr 714 |
. . . . . . 7
β’ (((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) |
29 | 22, 26, 28 | seqcl 13935 |
. . . . . 6
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β (seq1( Β· ,
((π β π΄ β¦ π΅) β π))β(β―βπ΄)) β π) |
30 | 20, 29 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ ((β―βπ΄) β β β§ π:(1...(β―βπ΄))β1-1-ontoβπ΄)) β βπ β π΄ π΅ β π) |
31 | 30 | expr 458 |
. . . 4
β’ ((π β§ (β―βπ΄) β β) β (π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ π΅ β π)) |
32 | 31 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―βπ΄) β β) β
(βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄ β βπ β π΄ π΅ β π)) |
33 | 32 | expimpd 455 |
. 2
β’ (π β (((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄) β βπ β π΄ π΅ β π)) |
34 | | fprodcllem.3 |
. . 3
β’ (π β π΄ β Fin) |
35 | | fz1f1o 15602 |
. . 3
β’ (π΄ β Fin β (π΄ = β
β¨
((β―βπ΄) β
β β§ βπ
π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
36 | 34, 35 | syl 17 |
. 2
β’ (π β (π΄ = β
β¨ ((β―βπ΄) β β β§
βπ π:(1...(β―βπ΄))β1-1-ontoβπ΄))) |
37 | 3, 33, 36 | mpjaod 859 |
1
β’ (π β βπ β π΄ π΅ β π) |