Step | Hyp | Ref
| Expression |
1 | | fprodss.1 |
. . 3
β’ (π β π΄ β π΅) |
2 | | sseq2 3971 |
. . . . 5
β’ (π΅ = β
β (π΄ β π΅ β π΄ β β
)) |
3 | | ss0 4359 |
. . . . 5
β’ (π΄ β β
β π΄ = β
) |
4 | 2, 3 | syl6bi 253 |
. . . 4
β’ (π΅ = β
β (π΄ β π΅ β π΄ = β
)) |
5 | | prodeq1 15797 |
. . . . . 6
β’ (π΄ = β
β βπ β π΄ πΆ = βπ β β
πΆ) |
6 | | prodeq1 15797 |
. . . . . . 7
β’ (π΅ = β
β βπ β π΅ πΆ = βπ β β
πΆ) |
7 | 6 | eqcomd 2739 |
. . . . . 6
β’ (π΅ = β
β βπ β β
πΆ = βπ β π΅ πΆ) |
8 | 5, 7 | sylan9eq 2793 |
. . . . 5
β’ ((π΄ = β
β§ π΅ = β
) β βπ β π΄ πΆ = βπ β π΅ πΆ) |
9 | 8 | expcom 415 |
. . . 4
β’ (π΅ = β
β (π΄ = β
β βπ β π΄ πΆ = βπ β π΅ πΆ)) |
10 | 4, 9 | syld 47 |
. . 3
β’ (π΅ = β
β (π΄ β π΅ β βπ β π΄ πΆ = βπ β π΅ πΆ)) |
11 | 1, 10 | syl5com 31 |
. 2
β’ (π β (π΅ = β
β βπ β π΄ πΆ = βπ β π΅ πΆ)) |
12 | | cnvimass 6034 |
. . . . . . . . 9
β’ (β‘π β π΄) β dom π |
13 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))β1-1-ontoβπ΅) |
14 | | f1of 6785 |
. . . . . . . . . 10
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))βΆπ΅) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))βΆπ΅) |
16 | 12, 15 | fssdm 6689 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β‘π β π΄) β (1...(β―βπ΅))) |
17 | | f1ofn 6786 |
. . . . . . . . . . . 12
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π Fn (1...(β―βπ΅))) |
18 | | elpreima 7009 |
. . . . . . . . . . . 12
β’ (π Fn (1...(β―βπ΅)) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
19 | 13, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
20 | 15 | ffvelcdmda 7036 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (1...(β―βπ΅))) β (πβπ) β π΅) |
21 | 20 | ex 414 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (1...(β―βπ΅)) β (πβπ) β π΅)) |
22 | 21 | adantrd 493 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β ((π β (1...(β―βπ΅)) β§ (πβπ) β π΄) β (πβπ) β π΅)) |
23 | 19, 22 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄) β (πβπ) β π΅)) |
24 | 23 | imp 408 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β (πβπ) β π΅) |
25 | | fprodss.2 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β πΆ β β) |
26 | 25 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β (π β π΄ β πΆ β β)) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (π β π΄ β πΆ β β)) |
28 | | eldif 3921 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β π΄) β (π β π΅ β§ Β¬ π β π΄)) |
29 | | fprodss.3 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΅ β π΄)) β πΆ = 1) |
30 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
31 | 29, 30 | eqeltrdi 2842 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π΅ β π΄)) β πΆ β β) |
32 | 28, 31 | sylan2br 596 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β πΆ β β) |
33 | 32 | expr 458 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β (Β¬ π β π΄ β πΆ β β)) |
34 | 27, 33 | pm2.61d 179 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β πΆ β β) |
35 | 34 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΅) β πΆ β β) |
36 | 35 | fmpttd 7064 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β π΅ β¦ πΆ):π΅βΆβ) |
37 | 36 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ (πβπ) β π΅) β ((π β π΅ β¦ πΆ)β(πβπ)) β β) |
38 | 24, 37 | syldan 592 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β ((π β π΅ β¦ πΆ)β(πβπ)) β β) |
39 | | eqid 2733 |
. . . . . . . . 9
β’
(β€β₯β1) =
(β€β₯β1) |
40 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β―βπ΅) β
β) |
41 | | nnuz 12811 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
42 | 40, 41 | eleqtrdi 2844 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β―βπ΅) β
(β€β₯β1)) |
43 | | ssidd 3968 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β
(1...(β―βπ΅))
β (1...(β―βπ΅))) |
44 | 39, 42, 43 | fprodntriv 15830 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ β
(β€β₯β1)βπ¦(π¦ β 0 β§ seqπ( Β· , (π β (β€β₯β1)
β¦ if(π β
(1...(β―βπ΅)),
((π β π΅ β¦ πΆ)β(πβπ)), 1))) β π¦)) |
45 | | eldifi 4087 |
. . . . . . . . . . . 12
β’ (π β
((1...(β―βπ΅))
β (β‘π β π΄)) β π β (1...(β―βπ΅))) |
46 | 45, 20 | sylan2 594 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (πβπ) β π΅) |
47 | | eldifn 4088 |
. . . . . . . . . . . . 13
β’ (π β
((1...(β―βπ΅))
β (β‘π β π΄)) β Β¬ π β (β‘π β π΄)) |
48 | 47 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β Β¬ π β (β‘π β π΄)) |
49 | 45 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β π β (1...(β―βπ΅))) |
50 | 19 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (β‘π β π΄) β (π β (1...(β―βπ΅)) β§ (πβπ) β π΄))) |
51 | 49, 50 | mpbirand 706 |
. . . . . . . . . . . 12
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (β‘π β π΄) β (πβπ) β π΄)) |
52 | 48, 51 | mtbid 324 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β Β¬ (πβπ) β π΄) |
53 | 46, 52 | eldifd 3922 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (πβπ) β (π΅ β π΄)) |
54 | | difss 4092 |
. . . . . . . . . . . . 13
β’ (π΅ β π΄) β π΅ |
55 | | resmpt 5992 |
. . . . . . . . . . . . 13
β’ ((π΅ β π΄) β π΅ β ((π β π΅ β¦ πΆ) βΎ (π΅ β π΄)) = (π β (π΅ β π΄) β¦ πΆ)) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π β π΅ β¦ πΆ) βΎ (π΅ β π΄)) = (π β (π΅ β π΄) β¦ πΆ) |
57 | 56 | fveq1i 6844 |
. . . . . . . . . . 11
β’ (((π β π΅ β¦ πΆ) βΎ (π΅ β π΄))β(πβπ)) = ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) |
58 | | fvres 6862 |
. . . . . . . . . . 11
β’ ((πβπ) β (π΅ β π΄) β (((π β π΅ β¦ πΆ) βΎ (π΅ β π΄))β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
59 | 57, 58 | eqtr3id 2787 |
. . . . . . . . . 10
β’ ((πβπ) β (π΅ β π΄) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
60 | 53, 59 | syl 17 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = ((π β π΅ β¦ πΆ)β(πβπ))) |
61 | | 1ex 11156 |
. . . . . . . . . . . . . . 15
β’ 1 β
V |
62 | 61 | elsn2 4626 |
. . . . . . . . . . . . . 14
β’ (πΆ β {1} β πΆ = 1) |
63 | 29, 62 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΅ β π΄)) β πΆ β {1}) |
64 | 63 | fmpttd 7064 |
. . . . . . . . . . . 12
β’ (π β (π β (π΅ β π΄) β¦ πΆ):(π΅ β π΄)βΆ{1}) |
65 | 64 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β (π β (π΅ β π΄) β¦ πΆ):(π΅ β π΄)βΆ{1}) |
66 | 65, 53 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) β {1}) |
67 | | elsni 4604 |
. . . . . . . . . 10
β’ (((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) β {1} β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = 1) |
68 | 66, 67 | syl 17 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β (π΅ β π΄) β¦ πΆ)β(πβπ)) = 1) |
69 | 60, 68 | eqtr3d 2775 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β ((1...(β―βπ΅)) β (β‘π β π΄))) β ((π β π΅ β¦ πΆ)β(πβπ)) = 1) |
70 | | fzssuz 13488 |
. . . . . . . . 9
β’
(1...(β―βπ΅)) β
(β€β₯β1) |
71 | 70 | a1i 11 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β
(1...(β―βπ΅))
β (β€β₯β1)) |
72 | 16, 38, 44, 69, 71 | prodss 15835 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ)) = βπ β (1...(β―βπ΅))((π β π΅ β¦ πΆ)β(πβπ))) |
73 | 1 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π΄ β π΅) |
74 | 73 | resmptd 5995 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β ((π β π΅ β¦ πΆ) βΎ π΄) = (π β π΄ β¦ πΆ)) |
75 | 74 | fveq1d 6845 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (((π β π΅ β¦ πΆ) βΎ π΄)βπ) = ((π β π΄ β¦ πΆ)βπ)) |
76 | | fvres 6862 |
. . . . . . . . . 10
β’ (π β π΄ β (((π β π΅ β¦ πΆ) βΎ π΄)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
77 | 75, 76 | sylan9req 2794 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
78 | 77 | prodeq2dv 15811 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΄ ((π β π΅ β¦ πΆ)βπ)) |
79 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = (πβπ) β ((π β π΅ β¦ πΆ)βπ) = ((π β π΅ β¦ πΆ)β(πβπ))) |
80 | | fzfid 13884 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β
(1...(β―βπ΅))
β Fin) |
81 | 80, 15 | fisuppfi 9317 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (β‘π β π΄) β Fin) |
82 | | f1of1 6784 |
. . . . . . . . . . . 12
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))β1-1βπ΅) |
83 | 13, 82 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))β1-1βπ΅) |
84 | | f1ores 6799 |
. . . . . . . . . . 11
β’ ((π:(1...(β―βπ΅))β1-1βπ΅ β§ (β‘π β π΄) β (1...(β―βπ΅))) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄))) |
85 | 83, 16, 84 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄))) |
86 | | f1ofo 6792 |
. . . . . . . . . . . . 13
β’ (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β π:(1...(β―βπ΅))βontoβπ΅) |
87 | 13, 86 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β π:(1...(β―βπ΅))βontoβπ΅) |
88 | | foimacnv 6802 |
. . . . . . . . . . . 12
β’ ((π:(1...(β―βπ΅))βontoβπ΅ β§ π΄ β π΅) β (π β (β‘π β π΄)) = π΄) |
89 | 87, 73, 88 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π β (β‘π β π΄)) = π΄) |
90 | 89 | f1oeq3d 6782 |
. . . . . . . . . 10
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β ((π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβ(π β (β‘π β π΄)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβπ΄)) |
91 | 85, 90 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β (π βΎ (β‘π β π΄)):(β‘π β π΄)β1-1-ontoβπ΄) |
92 | | fvres 6862 |
. . . . . . . . . 10
β’ (π β (β‘π β π΄) β ((π βΎ (β‘π β π΄))βπ) = (πβπ)) |
93 | 92 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (β‘π β π΄)) β ((π βΎ (β‘π β π΄))βπ) = (πβπ)) |
94 | 73 | sselda 3945 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β π β π΅) |
95 | 36 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΅) β ((π β π΅ β¦ πΆ)βπ) β β) |
96 | 94, 95 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β π΄) β ((π β π΅ β¦ πΆ)βπ) β β) |
97 | 79, 81, 91, 93, 96 | fprodf1o 15834 |
. . . . . . . 8
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ β π΄ ((π β π΅ β¦ πΆ)βπ) = βπ β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ))) |
98 | 78, 97 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β (β‘π β π΄)((π β π΅ β¦ πΆ)β(πβπ))) |
99 | | eqidd 2734 |
. . . . . . . 8
β’ (((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β§ π β (1...(β―βπ΅))) β (πβπ) = (πβπ)) |
100 | 79, 80, 13, 99, 95 | fprodf1o 15834 |
. . . . . . 7
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ β π΅ ((π β π΅ β¦ πΆ)βπ) = βπ β (1...(β―βπ΅))((π β π΅ β¦ πΆ)β(πβπ))) |
101 | 72, 98, 100 | 3eqtr4d 2783 |
. . . . . 6
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ β π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΅ ((π β π΅ β¦ πΆ)βπ)) |
102 | | prodfc 15833 |
. . . . . 6
β’
βπ β
π΄ ((π β π΄ β¦ πΆ)βπ) = βπ β π΄ πΆ |
103 | | prodfc 15833 |
. . . . . 6
β’
βπ β
π΅ ((π β π΅ β¦ πΆ)βπ) = βπ β π΅ πΆ |
104 | 101, 102,
103 | 3eqtr3g 2796 |
. . . . 5
β’ ((π β§ ((β―βπ΅) β β β§ π:(1...(β―βπ΅))β1-1-ontoβπ΅)) β βπ β π΄ πΆ = βπ β π΅ πΆ) |
105 | 104 | expr 458 |
. . . 4
β’ ((π β§ (β―βπ΅) β β) β (π:(1...(β―βπ΅))β1-1-ontoβπ΅ β βπ β π΄ πΆ = βπ β π΅ πΆ)) |
106 | 105 | exlimdv 1937 |
. . 3
β’ ((π β§ (β―βπ΅) β β) β
(βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅ β βπ β π΄ πΆ = βπ β π΅ πΆ)) |
107 | 106 | expimpd 455 |
. 2
β’ (π β (((β―βπ΅) β β β§
βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅) β βπ β π΄ πΆ = βπ β π΅ πΆ)) |
108 | | fprodss.4 |
. . 3
β’ (π β π΅ β Fin) |
109 | | fz1f1o 15600 |
. . 3
β’ (π΅ β Fin β (π΅ = β
β¨
((β―βπ΅) β
β β§ βπ
π:(1...(β―βπ΅))β1-1-ontoβπ΅))) |
110 | 108, 109 | syl 17 |
. 2
β’ (π β (π΅ = β
β¨ ((β―βπ΅) β β β§
βπ π:(1...(β―βπ΅))β1-1-ontoβπ΅))) |
111 | 11, 107, 110 | mpjaod 859 |
1
β’ (π β βπ β π΄ πΆ = βπ β π΅ πΆ) |