Step | Hyp | Ref
| Expression |
1 | | frn 6679 |
. . 3
β’ (πΉ:πΌβΆπ« π΅ β ran πΉ β π« π΅) |
2 | | elrfi 41064 |
. . 3
β’ ((π΅ β π β§ ran πΉ β π« π΅) β (π΄ β (fiβ({π΅} βͺ ran πΉ)) β βπ€ β (π« ran πΉ β© Fin)π΄ = (π΅ β© β© π€))) |
3 | 1, 2 | sylan2 594 |
. 2
β’ ((π΅ β π β§ πΉ:πΌβΆπ« π΅) β (π΄ β (fiβ({π΅} βͺ ran πΉ)) β βπ€ β (π« ran πΉ β© Fin)π΄ = (π΅ β© β© π€))) |
4 | | imassrn 6028 |
. . . . . 6
β’ (πΉ β π£) β ran πΉ |
5 | | pwexg 5337 |
. . . . . . . 8
β’ (π΅ β π β π« π΅ β V) |
6 | | ssexg 5284 |
. . . . . . . 8
β’ ((ran
πΉ β π« π΅ β§ π« π΅ β V) β ran πΉ β V) |
7 | 1, 5, 6 | syl2anr 598 |
. . . . . . 7
β’ ((π΅ β π β§ πΉ:πΌβΆπ« π΅) β ran πΉ β V) |
8 | | elpw2g 5305 |
. . . . . . 7
β’ (ran
πΉ β V β ((πΉ β π£) β π« ran πΉ β (πΉ β π£) β ran πΉ)) |
9 | 7, 8 | syl 17 |
. . . . . 6
β’ ((π΅ β π β§ πΉ:πΌβΆπ« π΅) β ((πΉ β π£) β π« ran πΉ β (πΉ β π£) β ran πΉ)) |
10 | 4, 9 | mpbiri 258 |
. . . . 5
β’ ((π΅ β π β§ πΉ:πΌβΆπ« π΅) β (πΉ β π£) β π« ran πΉ) |
11 | 10 | adantr 482 |
. . . 4
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β (πΉ β π£) β π« ran πΉ) |
12 | | ffun 6675 |
. . . . . 6
β’ (πΉ:πΌβΆπ« π΅ β Fun πΉ) |
13 | 12 | ad2antlr 726 |
. . . . 5
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β Fun πΉ) |
14 | | inss2 4193 |
. . . . . . 7
β’
(π« πΌ β©
Fin) β Fin |
15 | 14 | sseli 3944 |
. . . . . 6
β’ (π£ β (π« πΌ β© Fin) β π£ β Fin) |
16 | 15 | adantl 483 |
. . . . 5
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β π£ β Fin) |
17 | | imafi 9125 |
. . . . 5
β’ ((Fun
πΉ β§ π£ β Fin) β (πΉ β π£) β Fin) |
18 | 13, 16, 17 | syl2anc 585 |
. . . 4
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β (πΉ β π£) β Fin) |
19 | 11, 18 | elind 4158 |
. . 3
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β (πΉ β π£) β (π« ran πΉ β© Fin)) |
20 | | ffn 6672 |
. . . . . 6
β’ (πΉ:πΌβΆπ« π΅ β πΉ Fn πΌ) |
21 | 20 | ad2antlr 726 |
. . . . 5
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π€ β (π« ran πΉ β© Fin)) β πΉ Fn πΌ) |
22 | | inss1 4192 |
. . . . . . . 8
β’
(π« ran πΉ
β© Fin) β π« ran πΉ |
23 | 22 | sseli 3944 |
. . . . . . 7
β’ (π€ β (π« ran πΉ β© Fin) β π€ β π« ran πΉ) |
24 | 23 | elpwid 4573 |
. . . . . 6
β’ (π€ β (π« ran πΉ β© Fin) β π€ β ran πΉ) |
25 | 24 | adantl 483 |
. . . . 5
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π€ β (π« ran πΉ β© Fin)) β π€ β ran πΉ) |
26 | | inss2 4193 |
. . . . . . 7
β’
(π« ran πΉ
β© Fin) β Fin |
27 | 26 | sseli 3944 |
. . . . . 6
β’ (π€ β (π« ran πΉ β© Fin) β π€ β Fin) |
28 | 27 | adantl 483 |
. . . . 5
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π€ β (π« ran πΉ β© Fin)) β π€ β Fin) |
29 | | fipreima 9308 |
. . . . 5
β’ ((πΉ Fn πΌ β§ π€ β ran πΉ β§ π€ β Fin) β βπ£ β (π« πΌ β© Fin)(πΉ β π£) = π€) |
30 | 21, 25, 28, 29 | syl3anc 1372 |
. . . 4
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π€ β (π« ran πΉ β© Fin)) β βπ£ β (π« πΌ β© Fin)(πΉ β π£) = π€) |
31 | | eqcom 2740 |
. . . . 5
β’ ((πΉ β π£) = π€ β π€ = (πΉ β π£)) |
32 | 31 | rexbii 3094 |
. . . 4
β’
(βπ£ β
(π« πΌ β©
Fin)(πΉ β π£) = π€ β βπ£ β (π« πΌ β© Fin)π€ = (πΉ β π£)) |
33 | 30, 32 | sylib 217 |
. . 3
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π€ β (π« ran πΉ β© Fin)) β βπ£ β (π« πΌ β© Fin)π€ = (πΉ β π£)) |
34 | | inteq 4914 |
. . . . . 6
β’ (π€ = (πΉ β π£) β β© π€ = β©
(πΉ β π£)) |
35 | 34 | ineq2d 4176 |
. . . . 5
β’ (π€ = (πΉ β π£) β (π΅ β© β© π€) = (π΅ β© β© (πΉ β π£))) |
36 | 35 | eqeq2d 2744 |
. . . 4
β’ (π€ = (πΉ β π£) β (π΄ = (π΅ β© β© π€) β π΄ = (π΅ β© β© (πΉ β π£)))) |
37 | 36 | adantl 483 |
. . 3
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π€ = (πΉ β π£)) β (π΄ = (π΅ β© β© π€) β π΄ = (π΅ β© β© (πΉ β π£)))) |
38 | 19, 33, 37 | rexxfrd 5368 |
. 2
β’ ((π΅ β π β§ πΉ:πΌβΆπ« π΅) β (βπ€ β (π« ran πΉ β© Fin)π΄ = (π΅ β© β© π€) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β© (πΉ β π£)))) |
39 | 20 | ad2antlr 726 |
. . . . . . 7
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β πΉ Fn πΌ) |
40 | | inss1 4192 |
. . . . . . . . . 10
β’
(π« πΌ β©
Fin) β π« πΌ |
41 | 40 | sseli 3944 |
. . . . . . . . 9
β’ (π£ β (π« πΌ β© Fin) β π£ β π« πΌ) |
42 | 41 | elpwid 4573 |
. . . . . . . 8
β’ (π£ β (π« πΌ β© Fin) β π£ β πΌ) |
43 | 42 | adantl 483 |
. . . . . . 7
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β π£ β πΌ) |
44 | | imaiinfv 41063 |
. . . . . . 7
β’ ((πΉ Fn πΌ β§ π£ β πΌ) β β©
π¦ β π£ (πΉβπ¦) = β© (πΉ β π£)) |
45 | 39, 43, 44 | syl2anc 585 |
. . . . . 6
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β β© π¦ β π£ (πΉβπ¦) = β© (πΉ β π£)) |
46 | 45 | eqcomd 2739 |
. . . . 5
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β β© (πΉ
β π£) = β© π¦ β π£ (πΉβπ¦)) |
47 | 46 | ineq2d 4176 |
. . . 4
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β (π΅ β© β© (πΉ β π£)) = (π΅ β© β©
π¦ β π£ (πΉβπ¦))) |
48 | 47 | eqeq2d 2744 |
. . 3
β’ (((π΅ β π β§ πΉ:πΌβΆπ« π΅) β§ π£ β (π« πΌ β© Fin)) β (π΄ = (π΅ β© β© (πΉ β π£)) β π΄ = (π΅ β© β©
π¦ β π£ (πΉβπ¦)))) |
49 | 48 | rexbidva 3170 |
. 2
β’ ((π΅ β π β§ πΉ:πΌβΆπ« π΅) β (βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β© (πΉ β π£)) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π¦ β π£ (πΉβπ¦)))) |
50 | 3, 38, 49 | 3bitrd 305 |
1
β’ ((π΅ β π β§ πΉ:πΌβΆπ« π΅) β (π΄ β (fiβ({π΅} βͺ ran πΉ)) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π¦ β π£ (πΉβπ¦)))) |