Step | Hyp | Ref
| Expression |
1 | | ffn 5365 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β πΉ Fn π΄) |
2 | | dffn3 5376 |
. . . 4
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
3 | 1, 2 | sylib 122 |
. . 3
β’ (πΉ:π΄βΆπ΅ β πΉ:π΄βΆran πΉ) |
4 | | f2ndf 6226 |
. . 3
β’ (πΉ:π΄βΆran πΉ β (2nd βΎ πΉ):πΉβΆran πΉ) |
5 | 3, 4 | syl 14 |
. 2
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβΆran πΉ) |
6 | 2, 4 | sylbi 121 |
. . . . 5
β’ (πΉ Fn π΄ β (2nd βΎ πΉ):πΉβΆran πΉ) |
7 | 1, 6 | syl 14 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβΆran πΉ) |
8 | | frn 5374 |
. . . 4
β’
((2nd βΎ πΉ):πΉβΆran πΉ β ran (2nd βΎ πΉ) β ran πΉ) |
9 | 7, 8 | syl 14 |
. . 3
β’ (πΉ:π΄βΆπ΅ β ran (2nd βΎ πΉ) β ran πΉ) |
10 | | elrn2g 4817 |
. . . . . 6
β’ (π¦ β ran πΉ β (π¦ β ran πΉ β βπ₯β¨π₯, π¦β© β πΉ)) |
11 | 10 | ibi 176 |
. . . . 5
β’ (π¦ β ran πΉ β βπ₯β¨π₯, π¦β© β πΉ) |
12 | | fvres 5539 |
. . . . . . . . . 10
β’
(β¨π₯, π¦β© β πΉ β ((2nd βΎ πΉ)ββ¨π₯, π¦β©) = (2nd ββ¨π₯, π¦β©)) |
13 | 12 | adantl 277 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ β¨π₯, π¦β© β πΉ) β ((2nd βΎ πΉ)ββ¨π₯, π¦β©) = (2nd ββ¨π₯, π¦β©)) |
14 | | vex 2740 |
. . . . . . . . . 10
β’ π₯ β V |
15 | | vex 2740 |
. . . . . . . . . 10
β’ π¦ β V |
16 | 14, 15 | op2nd 6147 |
. . . . . . . . 9
β’
(2nd ββ¨π₯, π¦β©) = π¦ |
17 | 13, 16 | eqtr2di 2227 |
. . . . . . . 8
β’ ((πΉ:π΄βΆπ΅ β§ β¨π₯, π¦β© β πΉ) β π¦ = ((2nd βΎ πΉ)ββ¨π₯, π¦β©)) |
18 | | f2ndf 6226 |
. . . . . . . . . 10
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβΆπ΅) |
19 | | ffn 5365 |
. . . . . . . . . 10
β’
((2nd βΎ πΉ):πΉβΆπ΅ β (2nd βΎ πΉ) Fn πΉ) |
20 | 18, 19 | syl 14 |
. . . . . . . . 9
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ) Fn πΉ) |
21 | | fnfvelrn 5648 |
. . . . . . . . 9
β’
(((2nd βΎ πΉ) Fn πΉ β§ β¨π₯, π¦β© β πΉ) β ((2nd βΎ πΉ)ββ¨π₯, π¦β©) β ran (2nd βΎ
πΉ)) |
22 | 20, 21 | sylan 283 |
. . . . . . . 8
β’ ((πΉ:π΄βΆπ΅ β§ β¨π₯, π¦β© β πΉ) β ((2nd βΎ πΉ)ββ¨π₯, π¦β©) β ran (2nd βΎ
πΉ)) |
23 | 17, 22 | eqeltrd 2254 |
. . . . . . 7
β’ ((πΉ:π΄βΆπ΅ β§ β¨π₯, π¦β© β πΉ) β π¦ β ran (2nd βΎ πΉ)) |
24 | 23 | ex 115 |
. . . . . 6
β’ (πΉ:π΄βΆπ΅ β (β¨π₯, π¦β© β πΉ β π¦ β ran (2nd βΎ πΉ))) |
25 | 24 | exlimdv 1819 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β (βπ₯β¨π₯, π¦β© β πΉ β π¦ β ran (2nd βΎ πΉ))) |
26 | 11, 25 | syl5 32 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (π¦ β ran πΉ β π¦ β ran (2nd βΎ πΉ))) |
27 | 26 | ssrdv 3161 |
. . 3
β’ (πΉ:π΄βΆπ΅ β ran πΉ β ran (2nd βΎ πΉ)) |
28 | 9, 27 | eqssd 3172 |
. 2
β’ (πΉ:π΄βΆπ΅ β ran (2nd βΎ πΉ) = ran πΉ) |
29 | | dffo2 5442 |
. 2
β’
((2nd βΎ πΉ):πΉβontoβran πΉ β ((2nd βΎ πΉ):πΉβΆran πΉ β§ ran (2nd βΎ πΉ) = ran πΉ)) |
30 | 5, 28, 29 | sylanbrc 417 |
1
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβontoβran πΉ) |