Step | Hyp | Ref
| Expression |
1 | | ffrn 6732 |
. . 3
β’ (πΉ:π΄βΆπ΅ β πΉ:π΄βΆran πΉ) |
2 | | f2ndf 8106 |
. . 3
β’ (πΉ:π΄βΆran πΉ β (2nd βΎ πΉ):πΉβΆran πΉ) |
3 | 1, 2 | syl 17 |
. 2
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβΆran πΉ) |
4 | | ffn 6718 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β πΉ Fn π΄) |
5 | | dffn3 6731 |
. . . . . 6
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
6 | 5, 2 | sylbi 216 |
. . . . 5
β’ (πΉ Fn π΄ β (2nd βΎ πΉ):πΉβΆran πΉ) |
7 | 4, 6 | syl 17 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβΆran πΉ) |
8 | 7 | frnd 6726 |
. . 3
β’ (πΉ:π΄βΆπ΅ β ran (2nd βΎ πΉ) β ran πΉ) |
9 | | elrn2g 5891 |
. . . . . 6
β’ (π¦ β ran πΉ β (π¦ β ran πΉ β βπ₯β¨π₯, π¦β© β πΉ)) |
10 | 9 | ibi 267 |
. . . . 5
β’ (π¦ β ran πΉ β βπ₯β¨π₯, π¦β© β πΉ) |
11 | | fvres 6911 |
. . . . . . . . . 10
β’
(β¨π₯, π¦β© β πΉ β ((2nd βΎ πΉ)ββ¨π₯, π¦β©) = (2nd ββ¨π₯, π¦β©)) |
12 | 11 | adantl 483 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆπ΅ β§ β¨π₯, π¦β© β πΉ) β ((2nd βΎ πΉ)ββ¨π₯, π¦β©) = (2nd ββ¨π₯, π¦β©)) |
13 | | vex 3479 |
. . . . . . . . . 10
β’ π₯ β V |
14 | | vex 3479 |
. . . . . . . . . 10
β’ π¦ β V |
15 | 13, 14 | op2nd 7984 |
. . . . . . . . 9
β’
(2nd ββ¨π₯, π¦β©) = π¦ |
16 | 12, 15 | eqtr2di 2790 |
. . . . . . . 8
β’ ((πΉ:π΄βΆπ΅ β§ β¨π₯, π¦β© β πΉ) β π¦ = ((2nd βΎ πΉ)ββ¨π₯, π¦β©)) |
17 | | f2ndf 8106 |
. . . . . . . . . 10
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβΆπ΅) |
18 | 17 | ffnd 6719 |
. . . . . . . . 9
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ) Fn πΉ) |
19 | | fnfvelrn 7083 |
. . . . . . . . 9
β’
(((2nd βΎ πΉ) Fn πΉ β§ β¨π₯, π¦β© β πΉ) β ((2nd βΎ πΉ)ββ¨π₯, π¦β©) β ran (2nd βΎ
πΉ)) |
20 | 18, 19 | sylan 581 |
. . . . . . . 8
β’ ((πΉ:π΄βΆπ΅ β§ β¨π₯, π¦β© β πΉ) β ((2nd βΎ πΉ)ββ¨π₯, π¦β©) β ran (2nd βΎ
πΉ)) |
21 | 16, 20 | eqeltrd 2834 |
. . . . . . 7
β’ ((πΉ:π΄βΆπ΅ β§ β¨π₯, π¦β© β πΉ) β π¦ β ran (2nd βΎ πΉ)) |
22 | 21 | ex 414 |
. . . . . 6
β’ (πΉ:π΄βΆπ΅ β (β¨π₯, π¦β© β πΉ β π¦ β ran (2nd βΎ πΉ))) |
23 | 22 | exlimdv 1937 |
. . . . 5
β’ (πΉ:π΄βΆπ΅ β (βπ₯β¨π₯, π¦β© β πΉ β π¦ β ran (2nd βΎ πΉ))) |
24 | 10, 23 | syl5 34 |
. . . 4
β’ (πΉ:π΄βΆπ΅ β (π¦ β ran πΉ β π¦ β ran (2nd βΎ πΉ))) |
25 | 24 | ssrdv 3989 |
. . 3
β’ (πΉ:π΄βΆπ΅ β ran πΉ β ran (2nd βΎ πΉ)) |
26 | 8, 25 | eqssd 4000 |
. 2
β’ (πΉ:π΄βΆπ΅ β ran (2nd βΎ πΉ) = ran πΉ) |
27 | | dffo2 6810 |
. 2
β’
((2nd βΎ πΉ):πΉβontoβran πΉ β ((2nd βΎ πΉ):πΉβΆran πΉ β§ ran (2nd βΎ πΉ) = ran πΉ)) |
28 | 3, 26, 27 | sylanbrc 584 |
1
β’ (πΉ:π΄βΆπ΅ β (2nd βΎ πΉ):πΉβontoβran πΉ) |