Step | Hyp | Ref
| Expression |
1 | | fsn2.1 |
. . . . . 6
β’ π΄ β V |
2 | 1 | snid 4664 |
. . . . 5
β’ π΄ β {π΄} |
3 | | ffvelcdm 7083 |
. . . . 5
β’ ((πΉ:{π΄}βΆπ΅ β§ π΄ β {π΄}) β (πΉβπ΄) β π΅) |
4 | 2, 3 | mpan2 689 |
. . . 4
β’ (πΉ:{π΄}βΆπ΅ β (πΉβπ΄) β π΅) |
5 | | ffn 6717 |
. . . . 5
β’ (πΉ:{π΄}βΆπ΅ β πΉ Fn {π΄}) |
6 | | dffn3 6730 |
. . . . . . 7
β’ (πΉ Fn {π΄} β πΉ:{π΄}βΆran πΉ) |
7 | 6 | biimpi 215 |
. . . . . 6
β’ (πΉ Fn {π΄} β πΉ:{π΄}βΆran πΉ) |
8 | | imadmrn 6069 |
. . . . . . . . 9
β’ (πΉ β dom πΉ) = ran πΉ |
9 | | fndm 6652 |
. . . . . . . . . 10
β’ (πΉ Fn {π΄} β dom πΉ = {π΄}) |
10 | 9 | imaeq2d 6059 |
. . . . . . . . 9
β’ (πΉ Fn {π΄} β (πΉ β dom πΉ) = (πΉ β {π΄})) |
11 | 8, 10 | eqtr3id 2786 |
. . . . . . . 8
β’ (πΉ Fn {π΄} β ran πΉ = (πΉ β {π΄})) |
12 | | fnsnfv 6970 |
. . . . . . . . 9
β’ ((πΉ Fn {π΄} β§ π΄ β {π΄}) β {(πΉβπ΄)} = (πΉ β {π΄})) |
13 | 2, 12 | mpan2 689 |
. . . . . . . 8
β’ (πΉ Fn {π΄} β {(πΉβπ΄)} = (πΉ β {π΄})) |
14 | 11, 13 | eqtr4d 2775 |
. . . . . . 7
β’ (πΉ Fn {π΄} β ran πΉ = {(πΉβπ΄)}) |
15 | 14 | feq3d 6704 |
. . . . . 6
β’ (πΉ Fn {π΄} β (πΉ:{π΄}βΆran πΉ β πΉ:{π΄}βΆ{(πΉβπ΄)})) |
16 | 7, 15 | mpbid 231 |
. . . . 5
β’ (πΉ Fn {π΄} β πΉ:{π΄}βΆ{(πΉβπ΄)}) |
17 | 5, 16 | syl 17 |
. . . 4
β’ (πΉ:{π΄}βΆπ΅ β πΉ:{π΄}βΆ{(πΉβπ΄)}) |
18 | 4, 17 | jca 512 |
. . 3
β’ (πΉ:{π΄}βΆπ΅ β ((πΉβπ΄) β π΅ β§ πΉ:{π΄}βΆ{(πΉβπ΄)})) |
19 | | snssi 4811 |
. . . 4
β’ ((πΉβπ΄) β π΅ β {(πΉβπ΄)} β π΅) |
20 | | fss 6734 |
. . . . 5
β’ ((πΉ:{π΄}βΆ{(πΉβπ΄)} β§ {(πΉβπ΄)} β π΅) β πΉ:{π΄}βΆπ΅) |
21 | 20 | ancoms 459 |
. . . 4
β’ (({(πΉβπ΄)} β π΅ β§ πΉ:{π΄}βΆ{(πΉβπ΄)}) β πΉ:{π΄}βΆπ΅) |
22 | 19, 21 | sylan 580 |
. . 3
β’ (((πΉβπ΄) β π΅ β§ πΉ:{π΄}βΆ{(πΉβπ΄)}) β πΉ:{π΄}βΆπ΅) |
23 | 18, 22 | impbii 208 |
. 2
β’ (πΉ:{π΄}βΆπ΅ β ((πΉβπ΄) β π΅ β§ πΉ:{π΄}βΆ{(πΉβπ΄)})) |
24 | | fvex 6904 |
. . . 4
β’ (πΉβπ΄) β V |
25 | 1, 24 | fsn 7135 |
. . 3
β’ (πΉ:{π΄}βΆ{(πΉβπ΄)} β πΉ = {β¨π΄, (πΉβπ΄)β©}) |
26 | 25 | anbi2i 623 |
. 2
β’ (((πΉβπ΄) β π΅ β§ πΉ:{π΄}βΆ{(πΉβπ΄)}) β ((πΉβπ΄) β π΅ β§ πΉ = {β¨π΄, (πΉβπ΄)β©})) |
27 | 23, 26 | bitri 274 |
1
β’ (πΉ:{π΄}βΆπ΅ β ((πΉβπ΄) β π΅ β§ πΉ = {β¨π΄, (πΉβπ΄)β©})) |