Step | Hyp | Ref
| Expression |
1 | | fsumiunle.1 |
. . . 4
β’ (π β π΄ β Fin) |
2 | | fsumiunle.2 |
. . . 4
β’ ((π β§ π₯ β π΄) β π΅ β Fin) |
3 | 1, 2 | aciunf1 31632 |
. . 3
β’ (π β βπ(π:βͺ π₯ β π΄ π΅β1-1ββͺ π₯ β π΄ ({π₯} Γ π΅) β§ βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π)) |
4 | | f1f1orn 6799 |
. . . . . 6
β’ (π:βͺ π₯ β π΄ π΅β1-1ββͺ π₯ β π΄ ({π₯} Γ π΅) β π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π) |
5 | 4 | anim1i 616 |
. . . . 5
β’ ((π:βͺ π₯ β π΄ π΅β1-1ββͺ π₯ β π΄ ({π₯} Γ π΅) β§ βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π) β (π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π)) |
6 | | f1f 6742 |
. . . . . . 7
β’ (π:βͺ π₯ β π΄ π΅β1-1ββͺ π₯ β π΄ ({π₯} Γ π΅) β π:βͺ π₯ β π΄ π΅βΆβͺ
π₯ β π΄ ({π₯} Γ π΅)) |
7 | 6 | frnd 6680 |
. . . . . 6
β’ (π:βͺ π₯ β π΄ π΅β1-1ββͺ π₯ β π΄ ({π₯} Γ π΅) β ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅)) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((π:βͺ π₯ β π΄ π΅β1-1ββͺ π₯ β π΄ ({π₯} Γ π΅) β§ βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π) β ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅)) |
9 | 5, 8 | jca 513 |
. . . 4
β’ ((π:βͺ π₯ β π΄ π΅β1-1ββͺ π₯ β π΄ ({π₯} Γ π΅) β§ βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π) β ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) |
10 | 9 | eximi 1838 |
. . 3
β’
(βπ(π:βͺ π₯ β π΄ π΅β1-1ββͺ π₯ β π΄ ({π₯} Γ π΅) β§ βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π) β βπ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) |
11 | 3, 10 | syl 17 |
. 2
β’ (π β βπ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) |
12 | | csbeq1a 3873 |
. . . . . . 7
β’ (π = π¦ β πΆ = β¦π¦ / πβ¦πΆ) |
13 | | nfcv 2904 |
. . . . . . 7
β’
β²π¦βͺ π₯ β π΄ π΅ |
14 | | nfcv 2904 |
. . . . . . 7
β’
β²πβͺ π₯ β π΄ π΅ |
15 | | nfcv 2904 |
. . . . . . 7
β’
β²π¦πΆ |
16 | | nfcsb1v 3884 |
. . . . . . 7
β’
β²πβ¦π¦ / πβ¦πΆ |
17 | 12, 13, 14, 15, 16 | cbvsum 15588 |
. . . . . 6
β’
Ξ£π β
βͺ π₯ β π΄ π΅πΆ = Ξ£π¦ β βͺ
π₯ β π΄ π΅β¦π¦ / πβ¦πΆ |
18 | | csbeq1 3862 |
. . . . . . 7
β’ (π¦ = (2nd βπ§) β β¦π¦ / πβ¦πΆ = β¦(2nd
βπ§) / πβ¦πΆ) |
19 | | snfi 8994 |
. . . . . . . . . . . 12
β’ {π₯} β Fin |
20 | | xpfi 9267 |
. . . . . . . . . . . 12
β’ (({π₯} β Fin β§ π΅ β Fin) β ({π₯} Γ π΅) β Fin) |
21 | 19, 2, 20 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β ({π₯} Γ π΅) β Fin) |
22 | 21 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (π β βπ₯ β π΄ ({π₯} Γ π΅) β Fin) |
23 | | iunfi 9290 |
. . . . . . . . . 10
β’ ((π΄ β Fin β§ βπ₯ β π΄ ({π₯} Γ π΅) β Fin) β βͺ π₯ β π΄ ({π₯} Γ π΅) β Fin) |
24 | 1, 22, 23 | syl2anc 585 |
. . . . . . . . 9
β’ (π β βͺ π₯ β π΄ ({π₯} Γ π΅) β Fin) |
25 | 24 | adantr 482 |
. . . . . . . 8
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β βͺ π₯ β π΄ ({π₯} Γ π΅) β Fin) |
26 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅)) |
27 | 25, 26 | ssfid 9217 |
. . . . . . 7
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β ran π β Fin) |
28 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ ran π β βͺ π₯ β π΄ ({π₯} Γ π΅))) β π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π) |
29 | | f1ocnv 6800 |
. . . . . . . . 9
β’ (π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β β‘π:ran πβ1-1-ontoββͺ π₯ β π΄ π΅) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ ran π β βͺ π₯ β π΄ ({π₯} Γ π΅))) β β‘π:ran πβ1-1-ontoββͺ π₯ β π΄ π΅) |
31 | 30 | adantrlr 722 |
. . . . . . 7
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β β‘π:ran πβ1-1-ontoββͺ π₯ β π΄ π΅) |
32 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π₯π |
33 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯π |
34 | | nfiu1 4992 |
. . . . . . . . . . . . 13
β’
β²π₯βͺ π₯ β π΄ π΅ |
35 | 33 | nfrn 5911 |
. . . . . . . . . . . . 13
β’
β²π₯ran
π |
36 | 33, 34, 35 | nff1o 6786 |
. . . . . . . . . . . 12
β’
β²π₯ π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π |
37 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π₯(2nd β(πβπ)) = π |
38 | 34, 37 | nfralw 3293 |
. . . . . . . . . . . 12
β’
β²π₯βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π |
39 | 36, 38 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π₯(π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) |
40 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π₯ran
π |
41 | | nfiu1 4992 |
. . . . . . . . . . . 12
β’
β²π₯βͺ π₯ β π΄ ({π₯} Γ π΅) |
42 | 40, 41 | nfss 3940 |
. . . . . . . . . . 11
β’
β²π₯ran π β βͺ π₯ β π΄ ({π₯} Γ π΅) |
43 | 39, 42 | nfan 1903 |
. . . . . . . . . 10
β’
β²π₯((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅)) |
44 | 32, 43 | nfan 1903 |
. . . . . . . . 9
β’
β²π₯(π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) |
45 | | nfv 1918 |
. . . . . . . . 9
β’
β²π₯ π§ β ran π |
46 | 44, 45 | nfan 1903 |
. . . . . . . 8
β’
β²π₯((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) |
47 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β (πβπ) = π§) |
48 | 47 | fveq2d 6850 |
. . . . . . . . . . 11
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β (2nd β(πβπ)) = (2nd βπ§)) |
49 | | simplr 768 |
. . . . . . . . . . . 12
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β π β βͺ
π₯ β π΄ π΅) |
50 | | simp-4r 783 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) |
51 | 50 | simpld 496 |
. . . . . . . . . . . . . 14
β’
(((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β (π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π)) |
52 | 51 | simprd 497 |
. . . . . . . . . . . . 13
β’
(((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π) |
53 | 52 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π) |
54 | | 2fveq3 6851 |
. . . . . . . . . . . . . 14
β’ (π = π β (2nd β(πβπ)) = (2nd β(πβπ))) |
55 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = π β π = π) |
56 | 54, 55 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (π = π β ((2nd β(πβπ)) = π β (2nd β(πβπ)) = π)) |
57 | 56 | rspcva 3581 |
. . . . . . . . . . . 12
β’ ((π β βͺ π₯ β π΄ π΅ β§ βπ β βͺ
π₯ β π΄ π΅(2nd β(πβπ)) = π) β (2nd β(πβπ)) = π) |
58 | 49, 53, 57 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β (2nd β(πβπ)) = π) |
59 | 48, 58 | eqtr3d 2775 |
. . . . . . . . . 10
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β (2nd βπ§) = π) |
60 | 51 | simpld 496 |
. . . . . . . . . . . 12
β’
(((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π) |
61 | 60 | ad2antrr 725 |
. . . . . . . . . . 11
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π) |
62 | | f1ocnvfv1 7226 |
. . . . . . . . . . 11
β’ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ π β βͺ
π₯ β π΄ π΅) β (β‘πβ(πβπ)) = π) |
63 | 61, 49, 62 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β (β‘πβ(πβπ)) = π) |
64 | 47 | fveq2d 6850 |
. . . . . . . . . 10
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β (β‘πβ(πβπ)) = (β‘πβπ§)) |
65 | 59, 63, 64 | 3eqtr2rd 2780 |
. . . . . . . . 9
β’
(((((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β§ π β βͺ
π₯ β π΄ π΅) β§ (πβπ) = π§) β (β‘πβπ§) = (2nd βπ§)) |
66 | | f1ofn 6789 |
. . . . . . . . . . 11
β’ (π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β π Fn βͺ π₯ β π΄ π΅) |
67 | 60, 66 | syl 17 |
. . . . . . . . . 10
β’
(((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β π Fn βͺ π₯ β π΄ π΅) |
68 | | simpllr 775 |
. . . . . . . . . 10
β’
(((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β π§ β ran π) |
69 | | fvelrnb 6907 |
. . . . . . . . . . 11
β’ (π Fn βͺ π₯ β π΄ π΅ β (π§ β ran π β βπ β βͺ
π₯ β π΄ π΅(πβπ) = π§)) |
70 | 69 | biimpa 478 |
. . . . . . . . . 10
β’ ((π Fn βͺ π₯ β π΄ π΅ β§ π§ β ran π) β βπ β βͺ
π₯ β π΄ π΅(πβπ) = π§) |
71 | 67, 68, 70 | syl2anc 585 |
. . . . . . . . 9
β’
(((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β βπ β βͺ
π₯ β π΄ π΅(πβπ) = π§) |
72 | 65, 71 | r19.29a 3156 |
. . . . . . . 8
β’
(((((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β (β‘πβπ§) = (2nd βπ§)) |
73 | 26 | sselda 3948 |
. . . . . . . . 9
β’ (((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) |
74 | | eliun 4962 |
. . . . . . . . 9
β’ (π§ β βͺ π₯ β π΄ ({π₯} Γ π΅) β βπ₯ β π΄ π§ β ({π₯} Γ π΅)) |
75 | 73, 74 | sylib 217 |
. . . . . . . 8
β’ (((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β βπ₯ β π΄ π§ β ({π₯} Γ π΅)) |
76 | 46, 72, 75 | r19.29af 3250 |
. . . . . . 7
β’ (((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β ran π) β (β‘πβπ§) = (2nd βπ§)) |
77 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π β§ π¦ β βͺ
π₯ β π΄ π΅) |
78 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²πβ |
79 | 16, 78 | nfel 2918 |
. . . . . . . . . 10
β’
β²πβ¦π¦ / πβ¦πΆ β β |
80 | 77, 79 | nfim 1900 |
. . . . . . . . 9
β’
β²π((π β§ π¦ β βͺ
π₯ β π΄ π΅) β β¦π¦ / πβ¦πΆ β β) |
81 | | eleq1w 2817 |
. . . . . . . . . . 11
β’ (π = π¦ β (π β βͺ
π₯ β π΄ π΅ β π¦ β βͺ
π₯ β π΄ π΅)) |
82 | 81 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = π¦ β ((π β§ π β βͺ
π₯ β π΄ π΅) β (π β§ π¦ β βͺ
π₯ β π΄ π΅))) |
83 | 12 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = π¦ β (πΆ β β β β¦π¦ / πβ¦πΆ β β)) |
84 | 82, 83 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π¦ β (((π β§ π β βͺ
π₯ β π΄ π΅) β πΆ β β) β ((π β§ π¦ β βͺ
π₯ β π΄ π΅) β β¦π¦ / πβ¦πΆ β β))) |
85 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π₯π |
86 | 85, 34 | nfel 2918 |
. . . . . . . . . . 11
β’
β²π₯ π β βͺ π₯ β π΄ π΅ |
87 | 32, 86 | nfan 1903 |
. . . . . . . . . 10
β’
β²π₯(π β§ π β βͺ
π₯ β π΄ π΅) |
88 | | fsumiunle.3 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π΄) β§ π β π΅) β πΆ β β) |
89 | 88 | adantllr 718 |
. . . . . . . . . . 11
β’ ((((π β§ π β βͺ
π₯ β π΄ π΅) β§ π₯ β π΄) β§ π β π΅) β πΆ β β) |
90 | 89 | recnd 11191 |
. . . . . . . . . 10
β’ ((((π β§ π β βͺ
π₯ β π΄ π΅) β§ π₯ β π΄) β§ π β π΅) β πΆ β β) |
91 | | eliun 4962 |
. . . . . . . . . . . 12
β’ (π β βͺ π₯ β π΄ π΅ β βπ₯ β π΄ π β π΅) |
92 | 91 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β βͺ π₯ β π΄ π΅ β βπ₯ β π΄ π β π΅) |
93 | 92 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β βͺ
π₯ β π΄ π΅) β βπ₯ β π΄ π β π΅) |
94 | 87, 90, 93 | r19.29af 3250 |
. . . . . . . . 9
β’ ((π β§ π β βͺ
π₯ β π΄ π΅) β πΆ β β) |
95 | 80, 84, 94 | chvarfv 2234 |
. . . . . . . 8
β’ ((π β§ π¦ β βͺ
π₯ β π΄ π΅) β β¦π¦ / πβ¦πΆ β β) |
96 | 95 | adantlr 714 |
. . . . . . 7
β’ (((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π¦ β βͺ
π₯ β π΄ π΅) β β¦π¦ / πβ¦πΆ β β) |
97 | 18, 27, 31, 76, 96 | fsumf1o 15616 |
. . . . . 6
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β Ξ£π¦ β βͺ
π₯ β π΄ π΅β¦π¦ / πβ¦πΆ = Ξ£π§ β ran πβ¦(2nd βπ§) / πβ¦πΆ) |
98 | 17, 97 | eqtrid 2785 |
. . . . 5
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β Ξ£π β βͺ
π₯ β π΄ π΅πΆ = Ξ£π§ β ran πβ¦(2nd βπ§) / πβ¦πΆ) |
99 | 98 | eqcomd 2739 |
. . . 4
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β Ξ£π§ β ran πβ¦(2nd βπ§) / πβ¦πΆ = Ξ£π β βͺ
π₯ β π΄ π΅πΆ) |
100 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π₯π§ |
101 | 100, 41 | nfel 2918 |
. . . . . . . 8
β’
β²π₯ π§ β βͺ π₯ β π΄ ({π₯} Γ π΅) |
102 | 32, 101 | nfan 1903 |
. . . . . . 7
β’
β²π₯(π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) |
103 | | xp2nd 7958 |
. . . . . . . . 9
β’ (π§ β ({π₯} Γ π΅) β (2nd βπ§) β π΅) |
104 | 103 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β (2nd βπ§) β π΅) |
105 | 88 | ralrimiva 3140 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β βπ β π΅ πΆ β β) |
106 | 105 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β βπ β π΅ πΆ β β) |
107 | 106 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β βπ β π΅ πΆ β β) |
108 | | nfcsb1v 3884 |
. . . . . . . . . . 11
β’
β²πβ¦(2nd βπ§) / πβ¦πΆ |
109 | 108 | nfel1 2920 |
. . . . . . . . . 10
β’
β²πβ¦(2nd βπ§) / πβ¦πΆ β β |
110 | | csbeq1a 3873 |
. . . . . . . . . . 11
β’ (π = (2nd βπ§) β πΆ = β¦(2nd
βπ§) / πβ¦πΆ) |
111 | 110 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = (2nd βπ§) β (πΆ β β β
β¦(2nd βπ§) / πβ¦πΆ β β)) |
112 | 109, 111 | rspc 3571 |
. . . . . . . . 9
β’
((2nd βπ§) β π΅ β (βπ β π΅ πΆ β β β
β¦(2nd βπ§) / πβ¦πΆ β β)) |
113 | 112 | imp 408 |
. . . . . . . 8
β’
(((2nd βπ§) β π΅ β§ βπ β π΅ πΆ β β) β
β¦(2nd βπ§) / πβ¦πΆ β β) |
114 | 104, 107,
113 | syl2anc 585 |
. . . . . . 7
β’ ((((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β β¦(2nd
βπ§) / πβ¦πΆ β β) |
115 | 74 | biimpi 215 |
. . . . . . . 8
β’ (π§ β βͺ π₯ β π΄ ({π₯} Γ π΅) β βπ₯ β π΄ π§ β ({π₯} Γ π΅)) |
116 | 115 | adantl 483 |
. . . . . . 7
β’ ((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β βπ₯ β π΄ π§ β ({π₯} Γ π΅)) |
117 | 102, 114,
116 | r19.29af 3250 |
. . . . . 6
β’ ((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β β¦(2nd
βπ§) / πβ¦πΆ β β) |
118 | 117 | adantlr 714 |
. . . . 5
β’ (((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β β¦(2nd
βπ§) / πβ¦πΆ β β) |
119 | | xp1st 7957 |
. . . . . . . . . . 11
β’ (π§ β ({π₯} Γ π΅) β (1st βπ§) β {π₯}) |
120 | | elsni 4607 |
. . . . . . . . . . 11
β’
((1st βπ§) β {π₯} β (1st βπ§) = π₯) |
121 | 119, 120 | syl 17 |
. . . . . . . . . 10
β’ (π§ β ({π₯} Γ π΅) β (1st βπ§) = π₯) |
122 | 121, 103 | jca 513 |
. . . . . . . . 9
β’ (π§ β ({π₯} Γ π΅) β ((1st βπ§) = π₯ β§ (2nd βπ§) β π΅)) |
123 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β§ ((1st βπ§) = π₯ β§ (2nd βπ§) β π΅)) β π) |
124 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β§ ((1st βπ§) = π₯ β§ (2nd βπ§) β π΅)) β π₯ β π΄) |
125 | | fsumiunle.4 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π΄) β§ π β π΅) β 0 β€ πΆ) |
126 | 125 | ralrimiva 3140 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β βπ β π΅ 0 β€ πΆ) |
127 | 123, 124,
126 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β§ ((1st βπ§) = π₯ β§ (2nd βπ§) β π΅)) β βπ β π΅ 0 β€ πΆ) |
128 | 122, 127 | sylan2 594 |
. . . . . . . 8
β’ ((((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β βπ β π΅ 0 β€ πΆ) |
129 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π0 |
130 | | nfcv 2904 |
. . . . . . . . . . 11
β’
β²π
β€ |
131 | 129, 130,
108 | nfbr 5156 |
. . . . . . . . . 10
β’
β²π0 β€
β¦(2nd βπ§) / πβ¦πΆ |
132 | 110 | breq2d 5121 |
. . . . . . . . . 10
β’ (π = (2nd βπ§) β (0 β€ πΆ β 0 β€
β¦(2nd βπ§) / πβ¦πΆ)) |
133 | 131, 132 | rspc 3571 |
. . . . . . . . 9
β’
((2nd βπ§) β π΅ β (βπ β π΅ 0 β€ πΆ β 0 β€
β¦(2nd βπ§) / πβ¦πΆ)) |
134 | 133 | imp 408 |
. . . . . . . 8
β’
(((2nd βπ§) β π΅ β§ βπ β π΅ 0 β€ πΆ) β 0 β€
β¦(2nd βπ§) / πβ¦πΆ) |
135 | 104, 128,
134 | syl2anc 585 |
. . . . . . 7
β’ ((((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β§ π₯ β π΄) β§ π§ β ({π₯} Γ π΅)) β 0 β€
β¦(2nd βπ§) / πβ¦πΆ) |
136 | 102, 135,
116 | r19.29af 3250 |
. . . . . 6
β’ ((π β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β 0 β€
β¦(2nd βπ§) / πβ¦πΆ) |
137 | 136 | adantlr 714 |
. . . . 5
β’ (((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β§ π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)) β 0 β€
β¦(2nd βπ§) / πβ¦πΆ) |
138 | 25, 118, 137, 26 | fsumless 15689 |
. . . 4
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β Ξ£π§ β ran πβ¦(2nd βπ§) / πβ¦πΆ β€ Ξ£π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
139 | 99, 138 | eqbrtrrd 5133 |
. . 3
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β Ξ£π β βͺ
π₯ β π΄ π΅πΆ β€ Ξ£π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
140 | | nfcv 2904 |
. . . . . . . 8
β’
β²π¦π΅ |
141 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππ΅ |
142 | 12, 140, 141, 15, 16 | cbvsum 15588 |
. . . . . . 7
β’
Ξ£π β
π΅ πΆ = Ξ£π¦ β π΅ β¦π¦ / πβ¦πΆ |
143 | 142 | a1i 11 |
. . . . . 6
β’ (π β Ξ£π β π΅ πΆ = Ξ£π¦ β π΅ β¦π¦ / πβ¦πΆ) |
144 | 143 | sumeq2sdv 15597 |
. . . . 5
β’ (π β Ξ£π₯ β π΄ Ξ£π β π΅ πΆ = Ξ£π₯ β π΄ Ξ£π¦ β π΅ β¦π¦ / πβ¦πΆ) |
145 | | vex 3451 |
. . . . . . . . . 10
β’ π₯ β V |
146 | | vex 3451 |
. . . . . . . . . 10
β’ π¦ β V |
147 | 145, 146 | op2ndd 7936 |
. . . . . . . . 9
β’ (π§ = β¨π₯, π¦β© β (2nd βπ§) = π¦) |
148 | 147 | eqcomd 2739 |
. . . . . . . 8
β’ (π§ = β¨π₯, π¦β© β π¦ = (2nd βπ§)) |
149 | 148 | csbeq1d 3863 |
. . . . . . 7
β’ (π§ = β¨π₯, π¦β© β β¦π¦ / πβ¦πΆ = β¦(2nd
βπ§) / πβ¦πΆ) |
150 | 149 | eqcomd 2739 |
. . . . . 6
β’ (π§ = β¨π₯, π¦β© β β¦(2nd
βπ§) / πβ¦πΆ = β¦π¦ / πβ¦πΆ) |
151 | | nfv 1918 |
. . . . . . . . 9
β’
β²π((π β§ π₯ β π΄) β§ π¦ β π΅) |
152 | 16 | nfel1 2920 |
. . . . . . . . 9
β’
β²πβ¦π¦ / πβ¦πΆ β β |
153 | 151, 152 | nfim 1900 |
. . . . . . . 8
β’
β²π(((π β§ π₯ β π΄) β§ π¦ β π΅) β β¦π¦ / πβ¦πΆ β β) |
154 | | eleq1w 2817 |
. . . . . . . . . 10
β’ (π = π¦ β (π β π΅ β π¦ β π΅)) |
155 | 154 | anbi2d 630 |
. . . . . . . . 9
β’ (π = π¦ β (((π β§ π₯ β π΄) β§ π β π΅) β ((π β§ π₯ β π΄) β§ π¦ β π΅))) |
156 | 155, 83 | imbi12d 345 |
. . . . . . . 8
β’ (π = π¦ β ((((π β§ π₯ β π΄) β§ π β π΅) β πΆ β β) β (((π β§ π₯ β π΄) β§ π¦ β π΅) β β¦π¦ / πβ¦πΆ β β))) |
157 | 88 | recnd 11191 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β π΅) β πΆ β β) |
158 | 153, 156,
157 | chvarfv 2234 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π¦ β π΅) β β¦π¦ / πβ¦πΆ β β) |
159 | 158 | anasss 468 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β§ π¦ β π΅)) β β¦π¦ / πβ¦πΆ β β) |
160 | 150, 1, 2, 159 | fsum2d 15664 |
. . . . 5
β’ (π β Ξ£π₯ β π΄ Ξ£π¦ β π΅ β¦π¦ / πβ¦πΆ = Ξ£π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
161 | 144, 160 | eqtrd 2773 |
. . . 4
β’ (π β Ξ£π₯ β π΄ Ξ£π β π΅ πΆ = Ξ£π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
162 | 161 | adantr 482 |
. . 3
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β Ξ£π₯ β π΄ Ξ£π β π΅ πΆ = Ξ£π§ β βͺ
π₯ β π΄ ({π₯} Γ π΅)β¦(2nd βπ§) / πβ¦πΆ) |
163 | 139, 162 | breqtrrd 5137 |
. 2
β’ ((π β§ ((π:βͺ π₯ β π΄ π΅β1-1-ontoβran
π β§ βπ β βͺ π₯ β π΄ π΅(2nd β(πβπ)) = π) β§ ran π β βͺ
π₯ β π΄ ({π₯} Γ π΅))) β Ξ£π β βͺ
π₯ β π΄ π΅πΆ β€ Ξ£π₯ β π΄ Ξ£π β π΅ πΆ) |
164 | 11, 163 | exlimddv 1939 |
1
β’ (π β Ξ£π β βͺ
π₯ β π΄ π΅πΆ β€ Ξ£π₯ β π΄ Ξ£π β π΅ πΆ) |