Step | Hyp | Ref
| Expression |
1 | | elee 28407 |
. 2
β’ (π β β β ((π β (1...π) β¦ (π΄πΉπ΅)) β (πΌβπ) β (π β (1...π) β¦ (π΄πΉπ΅)):(1...π)βΆβ)) |
2 | | ovex 7444 |
. . . . 5
β’ (π΄πΉπ΅) β V |
3 | | eqid 2732 |
. . . . 5
β’ (π β (1...π) β¦ (π΄πΉπ΅)) = (π β (1...π) β¦ (π΄πΉπ΅)) |
4 | 2, 3 | fnmpti 6693 |
. . . 4
β’ (π β (1...π) β¦ (π΄πΉπ΅)) Fn (1...π) |
5 | | df-f 6547 |
. . . 4
β’ ((π β (1...π) β¦ (π΄πΉπ΅)):(1...π)βΆβ β ((π β (1...π) β¦ (π΄πΉπ΅)) Fn (1...π) β§ ran (π β (1...π) β¦ (π΄πΉπ΅)) β β)) |
6 | 4, 5 | mpbiran 707 |
. . 3
β’ ((π β (1...π) β¦ (π΄πΉπ΅)):(1...π)βΆβ β ran (π β (1...π) β¦ (π΄πΉπ΅)) β β) |
7 | 3 | rnmpt 5954 |
. . . . 5
β’ ran
(π β (1...π) β¦ (π΄πΉπ΅)) = {π β£ βπ β (1...π)π = (π΄πΉπ΅)} |
8 | 7 | sseq1i 4010 |
. . . 4
β’ (ran
(π β (1...π) β¦ (π΄πΉπ΅)) β β β {π β£ βπ β (1...π)π = (π΄πΉπ΅)} β β) |
9 | | abss 4057 |
. . . . 5
β’ ({π β£ βπ β (1...π)π = (π΄πΉπ΅)} β β β βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
10 | | nfre1 3282 |
. . . . . . . . 9
β’
β²πβπ β (1...π)π = (π΄πΉπ΅) |
11 | | nfv 1917 |
. . . . . . . . 9
β’
β²π π β β |
12 | 10, 11 | nfim 1899 |
. . . . . . . 8
β’
β²π(βπ β (1...π)π = (π΄πΉπ΅) β π β β) |
13 | 12 | nfal 2316 |
. . . . . . 7
β’
β²πβπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β) |
14 | | r19.23v 3182 |
. . . . . . . . 9
β’
(βπ β
(1...π)(π = (π΄πΉπ΅) β π β β) β (βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
15 | 14 | albii 1821 |
. . . . . . . 8
β’
(βπβπ β (1...π)(π = (π΄πΉπ΅) β π β β) β βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
16 | | ralcom4 3283 |
. . . . . . . . 9
β’
(βπ β
(1...π)βπ(π = (π΄πΉπ΅) β π β β) β βπβπ β (1...π)(π = (π΄πΉπ΅) β π β β)) |
17 | | rsp 3244 |
. . . . . . . . . 10
β’
(βπ β
(1...π)βπ(π = (π΄πΉπ΅) β π β β) β (π β (1...π) β βπ(π = (π΄πΉπ΅) β π β β))) |
18 | 2 | clel2 3649 |
. . . . . . . . . 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 3254 |
. . . . . 6
β’
(βπ(βπ β (1...π)π = (π΄πΉπ΅) β π β β) β βπ β (1...π)(π΄πΉπ΅) β β) |
23 | | nfra1 3281 |
. . . . . . . 8
β’
β²πβπ β (1...π)(π΄πΉπ΅) β β |
24 | | rsp 3244 |
. . . . . . . . 9
β’
(βπ β
(1...π)(π΄πΉπ΅) β β β (π β (1...π) β (π΄πΉπ΅) β β)) |
25 | | eleq1a 2828 |
. . . . . . . . 9
β’ ((π΄πΉπ΅) β β β (π = (π΄πΉπ΅) β π β β)) |
26 | 24, 25 | syl6 35 |
. . . . . . . 8
β’
(βπ β
(1...π)(π΄πΉπ΅) β β β (π β (1...π) β (π = (π΄πΉπ΅) β π β β))) |
27 | 23, 11, 26 | rexlimd 3263 |
. . . . . . 7
β’
(βπ β
(1...π)(π΄πΉπ΅) β β β (βπ β (1...π)π = (π΄πΉπ΅) β π β β)) |
28 | 27 | alrimiv 1930 |
. . . . . 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...π)(π΄πΉπ΅) β β)) |