Step | Hyp | Ref
| Expression |
1 | | elee 28419 |
. 2
β’ (π β β β ((π β (1...π) β¦ (π΄πΉπ΅)) β (πΌβπ) β (π β (1...π) β¦ (π΄πΉπ΅)):(1...π)βΆβ)) |
2 | | ovex 7444 |
. . . . 5
β’ (π΄πΉπ΅) β V |
3 | | eqid 2730 |
. . . . 5
β’ (π β (1...π) β¦ (π΄πΉπ΅)) = (π β (1...π) β¦ (π΄πΉπ΅)) |
4 | 2, 3 | fnmpti 6692 |
. . . 4
β’ (π β (1...π) β¦ (π΄πΉπ΅)) Fn (1...π) |
5 | | df-f 6546 |
. . . 4
β’ ((π β (1...π) β¦ (π΄πΉπ΅)):(1...π)βΆβ β ((π β (1...π) β¦ (π΄πΉπ΅)) Fn (1...π) β§ ran (π β (1...π) β¦ (π΄πΉπ΅)) β β)) |
6 | 4, 5 | mpbiran 705 |
. . 3
β’ ((π β (1...π) β¦ (π΄πΉπ΅)):(1...π)βΆβ β ran (π β (1...π) β¦ (π΄πΉπ΅)) β β) |
7 | 3 | rnmpt 5953 |
. . . . 5
β’ ran
(π β (1...π) β¦ (π΄πΉπ΅)) = {π β£ βπ β (1...π)π = (π΄πΉπ΅)} |
8 | 7 | sseq1i 4009 |
. . . 4
β’ (ran
(π β (1...π) β¦ (π΄πΉπ΅)) β β β {π β£ βπ β (1...π)π = (π΄πΉπ΅)} β β) |
9 | | abss 4056 |
. . . . 5
β’ ({π β£ βπ β (1...π)π = (π΄πΉπ΅)} β β β βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
10 | | nfre1 3280 |
. . . . . . . . 9
β’
β²πβπ β (1...π)π = (π΄πΉπ΅) |
11 | | nfv 1915 |
. . . . . . . . 9
β’
β²π π β β |
12 | 10, 11 | nfim 1897 |
. . . . . . . 8
β’
β²π(βπ β (1...π)π = (π΄πΉπ΅) β π β β) |
13 | 12 | nfal 2314 |
. . . . . . 7
β’
β²πβπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β) |
14 | | r19.23v 3180 |
. . . . . . . . 9
β’
(βπ β
(1...π)(π = (π΄πΉπ΅) β π β β) β (βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
15 | 14 | albii 1819 |
. . . . . . . 8
β’
(βπβπ β (1...π)(π = (π΄πΉπ΅) β π β β) β βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
16 | | ralcom4 3281 |
. . . . . . . . 9
β’
(βπ β
(1...π)βπ(π = (π΄πΉπ΅) β π β β) β βπβπ β (1...π)(π = (π΄πΉπ΅) β π β β)) |
17 | | rsp 3242 |
. . . . . . . . . 10
β’
(βπ β
(1...π)βπ(π = (π΄πΉπ΅) β π β β) β (π β (1...π) β βπ(π = (π΄πΉπ΅) β π β β))) |
18 | 2 | clel2 3648 |
. . . . . . . . . 10
β’ ((π΄πΉπ΅) β β β βπ(π = (π΄πΉπ΅) β π β β)) |
19 | 17, 18 | imbitrrdi 251 |
. . . . . . . . 9
β’
(βπ β
(1...π)βπ(π = (π΄πΉπ΅) β π β β) β (π β (1...π) β (π΄πΉπ΅) β β)) |
20 | 16, 19 | sylbir 234 |
. . . . . . . 8
β’
(βπβπ β (1...π)(π = (π΄πΉπ΅) β π β β) β (π β (1...π) β (π΄πΉπ΅) β β)) |
21 | 15, 20 | sylbir 234 |
. . . . . . 7
β’
(βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β) β (π β (1...π) β (π΄πΉπ΅) β β)) |
22 | 13, 21 | ralrimi 3252 |
. . . . . 6
β’
(βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β) β βπ β (1...π)(π΄πΉπ΅) β β) |
23 | | nfra1 3279 |
. . . . . . . 8
β’
β²πβπ β (1...π)(π΄πΉπ΅) β β |
24 | | rsp 3242 |
. . . . . . . . 9
β’
(βπ β
(1...π)(π΄πΉπ΅) β β β (π β (1...π) β (π΄πΉπ΅) β β)) |
25 | | eleq1a 2826 |
. . . . . . . . 9
β’ ((π΄πΉπ΅) β β β (π = (π΄πΉπ΅) β π β β)) |
26 | 24, 25 | syl6 35 |
. . . . . . . 8
β’
(βπ β
(1...π)(π΄πΉπ΅) β β β (π β (1...π) β (π = (π΄πΉπ΅) β π β β))) |
27 | 23, 11, 26 | rexlimd 3261 |
. . . . . . 7
β’
(βπ β
(1...π)(π΄πΉπ΅) β β β (βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
28 | 27 | alrimiv 1928 |
. . . . . 6
β’
(βπ β
(1...π)(π΄πΉπ΅) β β β βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
29 | 22, 28 | impbii 208 |
. . . . 5
β’
(βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β) β βπ β (1...π)(π΄πΉπ΅) β β) |
30 | 9, 29 | bitri 274 |
. . . 4
β’ ({π β£ βπ β (1...π)π = (π΄πΉπ΅)} β β β βπ β (1...π)(π΄πΉπ΅) β β) |
31 | 8, 30 | bitri 274 |
. . 3
β’ (ran
(π β (1...π) β¦ (π΄πΉπ΅)) β β β βπ β (1...π)(π΄πΉπ΅) β β) |
32 | 6, 31 | bitri 274 |
. 2
β’ ((π β (1...π) β¦ (π΄πΉπ΅)):(1...π)βΆβ β βπ β (1...π)(π΄πΉπ΅) β β) |
33 | 1, 32 | bitrdi 286 |
1
β’ (π β β β ((π β (1...π) β¦ (π΄πΉπ΅)) β (πΌβπ) β βπ β (1...π)(π΄πΉπ΅) β β)) |