Step | Hyp | Ref
| Expression |
1 | | elpw2g 5343 |
. . . . . . 7
β’ (π΅ β π β (πΆ β π« π΅ β πΆ β π΅)) |
2 | 1 | biimprd 247 |
. . . . . 6
β’ (π΅ β π β (πΆ β π΅ β πΆ β π« π΅)) |
3 | 2 | ralimdv 3167 |
. . . . 5
β’ (π΅ β π β (βπ¦ β πΌ πΆ β π΅ β βπ¦ β πΌ πΆ β π« π΅)) |
4 | 3 | imp 405 |
. . . 4
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β βπ¦ β πΌ πΆ β π« π΅) |
5 | | eqid 2730 |
. . . . 5
β’ (π¦ β πΌ β¦ πΆ) = (π¦ β πΌ β¦ πΆ) |
6 | 5 | fmpt 7110 |
. . . 4
β’
(βπ¦ β
πΌ πΆ β π« π΅ β (π¦ β πΌ β¦ πΆ):πΌβΆπ« π΅) |
7 | 4, 6 | sylib 217 |
. . 3
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (π¦ β πΌ β¦ πΆ):πΌβΆπ« π΅) |
8 | | elrfirn 41735 |
. . 3
β’ ((π΅ β π β§ (π¦ β πΌ β¦ πΆ):πΌβΆπ« π΅) β (π΄ β (fiβ({π΅} βͺ ran (π¦ β πΌ β¦ πΆ))) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)))) |
9 | 7, 8 | syldan 589 |
. 2
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (π΄ β (fiβ({π΅} βͺ ran (π¦ β πΌ β¦ πΆ))) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)))) |
10 | | inss1 4227 |
. . . . . 6
β’
(π« πΌ β©
Fin) β π« πΌ |
11 | 10 | sseli 3977 |
. . . . 5
β’ (π£ β (π« πΌ β© Fin) β π£ β π« πΌ) |
12 | 11 | elpwid 4610 |
. . . 4
β’ (π£ β (π« πΌ β© Fin) β π£ β πΌ) |
13 | | nffvmpt1 6901 |
. . . . . . . 8
β’
β²π¦((π¦ β πΌ β¦ πΆ)βπ§) |
14 | | nfcv 2901 |
. . . . . . . 8
β’
β²π§((π¦ β πΌ β¦ πΆ)βπ¦) |
15 | | fveq2 6890 |
. . . . . . . 8
β’ (π§ = π¦ β ((π¦ β πΌ β¦ πΆ)βπ§) = ((π¦ β πΌ β¦ πΆ)βπ¦)) |
16 | 13, 14, 15 | cbviin 5039 |
. . . . . . 7
β’ β© π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§) = β© π¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) |
17 | | simplr 765 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β π¦ β πΌ) |
18 | | simpll 763 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β π΅ β π) |
19 | | simpr 483 |
. . . . . . . . . . . . . 14
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β πΆ β π΅) |
20 | 18, 19 | ssexd 5323 |
. . . . . . . . . . . . 13
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β πΆ β V) |
21 | 5 | fvmpt2 7008 |
. . . . . . . . . . . . 13
β’ ((π¦ β πΌ β§ πΆ β V) β ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ) |
22 | 17, 20, 21 | syl2anc 582 |
. . . . . . . . . . . 12
β’ (((π΅ β π β§ π¦ β πΌ) β§ πΆ β π΅) β ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ) |
23 | 22 | ex 411 |
. . . . . . . . . . 11
β’ ((π΅ β π β§ π¦ β πΌ) β (πΆ β π΅ β ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ)) |
24 | 23 | ralimdva 3165 |
. . . . . . . . . 10
β’ (π΅ β π β (βπ¦ β πΌ πΆ β π΅ β βπ¦ β πΌ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ)) |
25 | 24 | imp 405 |
. . . . . . . . 9
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β βπ¦ β πΌ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ) |
26 | | ssralv 4049 |
. . . . . . . . 9
β’ (π£ β πΌ β (βπ¦ β πΌ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ β βπ¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ)) |
27 | 25, 26 | mpan9 505 |
. . . . . . . 8
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β βπ¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ) |
28 | | iineq2 5016 |
. . . . . . . 8
β’
(βπ¦ β
π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = πΆ β β©
π¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = β© π¦ β π£ πΆ) |
29 | 27, 28 | syl 17 |
. . . . . . 7
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β β©
π¦ β π£ ((π¦ β πΌ β¦ πΆ)βπ¦) = β© π¦ β π£ πΆ) |
30 | 16, 29 | eqtrid 2782 |
. . . . . 6
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§) = β© π¦ β π£ πΆ) |
31 | 30 | ineq2d 4211 |
. . . . 5
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)) = (π΅ β© β©
π¦ β π£ πΆ)) |
32 | 31 | eqeq2d 2741 |
. . . 4
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β πΌ) β (π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)) β π΄ = (π΅ β© β©
π¦ β π£ πΆ))) |
33 | 12, 32 | sylan2 591 |
. . 3
β’ (((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β§ π£ β (π« πΌ β© Fin)) β (π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)) β π΄ = (π΅ β© β©
π¦ β π£ πΆ))) |
34 | 33 | rexbidva 3174 |
. 2
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π§ β π£ ((π¦ β πΌ β¦ πΆ)βπ§)) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π¦ β π£ πΆ))) |
35 | 9, 34 | bitrd 278 |
1
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (π΄ β (fiβ({π΅} βͺ ran (π¦ β πΌ β¦ πΆ))) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β©
π¦ β π£ πΆ))) |