Step | Hyp | Ref
| Expression |
1 | | elpw2g 5305 |
. . . . . . 7
β’ (π΅ β π β (πΆ β π« π΅ β πΆ β π΅)) |
2 | 1 | biimprd 248 |
. . . . . 6
β’ (π΅ β π β (πΆ β π΅ β πΆ β π« π΅)) |
3 | 2 | ralimdv 3163 |
. . . . 5
β’ (π΅ β π β (βπ¦ β πΌ πΆ β π΅ β βπ¦ β πΌ πΆ β π« π΅)) |
4 | 3 | imp 408 |
. . . 4
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β βπ¦ β πΌ πΆ β π« π΅) |
5 | | eqid 2733 |
. . . . 5
β’ (π¦ β πΌ β¦ πΆ) = (π¦ β πΌ β¦ πΆ) |
6 | 5 | fmpt 7062 |
. . . 4
β’
(βπ¦ β
πΌ πΆ β π« π΅ β (π¦ β πΌ β¦ πΆ):πΌβΆπ« π΅) |
7 | 4, 6 | sylib 217 |
. . 3
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (π¦ β πΌ β¦ πΆ):πΌβΆπ« π΅) |
8 | | elrfirn 41065 |
. . 3
β’ ((π΅ β π β§ (π¦ β πΌ β¦ πΆ):πΌβΆπ« π΅) β (π΄ β (fiβ({π΅} βͺ ran (π¦ β πΌ β¦ πΆ))) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)))) |
9 | 7, 8 | syldan 592 |
. 2
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (π΄ β (fiβ({π΅} βͺ ran (π¦ β πΌ β¦ πΆ))) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)))) |
10 | | inss1 4192 |
. . . . . 6
β’
(π« πΌ β©
Fin) β π« πΌ |
11 | 10 | sseli 3944 |
. . . . 5
β’ (π£ β (π« πΌ β© Fin) β π£ β π« πΌ) |
12 | 11 | elpwid 4573 |
. . . 4
β’ (π£ β (π« πΌ β© Fin) β π£ β πΌ) |
13 | | nffvmpt1 6857 |
. . . . . . . 8
β’
β²π¦((π¦ β πΌ β¦ πΆ)βπ§) |
14 | | nfcv 2904 |
. . . . . . . 8
β’
β²π§((π¦ β πΌ β¦ πΆ)βπ¦) |
15 | | fveq2 6846 |
. . . . . . . 8
β’ (π§ = π¦ β ((π¦ β πΌ β¦ πΆ)βπ§) = ((π¦ β πΌ β¦ πΆ)βπ¦)) |
16 | 13, 14, 15 | cbviin 5001 |
. . . . . . 7
β’ β© π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§) = β© π¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) |
17 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β π¦ β πΌ) |
18 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β π΅ β π) |
19 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β πΆ β π΅) |
20 | 18, 19 | ssexd 5285 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β πΆ β V) |
21 | 5 | fvmpt2 6963 |
. . . . . . . . . . . . 13
β’ ((π¦ β πΌ β§ πΆ β V) β ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ) |
22 | 17, 20, 21 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ) |
23 | 22 | ex 414 |
. . . . . . . . . . 11
β’ ((π΅ β π β§ π¦ β πΌ) β (πΆ β π΅ β ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ)) |
24 | 23 | ralimdva 3161 |
. . . . . . . . . 10
β’ (π΅ β π β (βπ¦ β πΌ πΆ β π΅ β βπ¦ β πΌ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ)) |
25 | 24 | imp 408 |
. . . . . . . . 9
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β βπ¦ β πΌ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ) |
26 | | ssralv 4014 |
. . . . . . . . 9
β’ (π£ β πΌ β (βπ¦ β πΌ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ β βπ¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ)) |
27 | 25, 26 | mpan9 508 |
. . . . . . . 8
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β βπ¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ) |
28 | | iineq2 4978 |
. . . . . . . 8
β’
(βπ¦ β
π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ β β©
π¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = β© π¦ β π£ πΆ) |
29 | 27, 28 | syl 17 |
. . . . . . 7
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β β©
π¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = β© π¦ β π£ πΆ) |
30 | 16, 29 | eqtrid 2785 |
. . . . . 6
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§) = β© π¦ β π£ πΆ) |
31 | 30 | ineq2d 4176 |
. . . . 5
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)) = (π΅ β© β©
π¦ β π£ πΆ)) |
32 | 31 | eqeq2d 2744 |
. . . 4
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β (π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)) β π΄ = (π΅ β© β©
π¦ β π£ πΆ))) |
33 | 12, 32 | sylan2 594 |
. . 3
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β (π« πΌ β© Fin)) β (π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)) β π΄ = (π΅ β© β©
π¦ β π£ πΆ))) |
34 | 33 | rexbidva 3170 |
. 2
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π¦ β π£ πΆ))) |
35 | 9, 34 | bitrd 279 |
1
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (π΄ β (fiβ({π΅} βͺ ran (π¦ β πΌ β¦ πΆ))) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π¦ β π£ πΆ))) |