Step | Hyp | Ref
| Expression |
1 | | focdmex 7893 |
. . . 4
β’ (π΄ β π β (πΉ:π΄βontoβπ΅ β π΅ β V)) |
2 | 1 | imp 408 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βontoβπ΅) β π΅ β V) |
3 | | foelrn 7061 |
. . . . . 6
β’ ((πΉ:π΄βontoβπ΅ β§ π¦ β π΅) β βπ§ β π΄ π¦ = (πΉβπ§)) |
4 | | fofn 6763 |
. . . . . . . . . 10
β’ (πΉ:π΄βontoβπ΅ β πΉ Fn π΄) |
5 | | eqcom 2744 |
. . . . . . . . . . 11
β’ ((πΉβπ§) = π¦ β π¦ = (πΉβπ§)) |
6 | | fniniseg 7015 |
. . . . . . . . . . . . 13
β’ (πΉ Fn π΄ β (π§ β (β‘πΉ β {π¦}) β (π§ β π΄ β§ (πΉβπ§) = π¦))) |
7 | 6 | biimpar 479 |
. . . . . . . . . . . 12
β’ ((πΉ Fn π΄ β§ (π§ β π΄ β§ (πΉβπ§) = π¦)) β π§ β (β‘πΉ β {π¦})) |
8 | 7 | anassrs 469 |
. . . . . . . . . . 11
β’ (((πΉ Fn π΄ β§ π§ β π΄) β§ (πΉβπ§) = π¦) β π§ β (β‘πΉ β {π¦})) |
9 | 5, 8 | sylan2br 596 |
. . . . . . . . . 10
β’ (((πΉ Fn π΄ β§ π§ β π΄) β§ π¦ = (πΉβπ§)) β π§ β (β‘πΉ β {π¦})) |
10 | 4, 9 | sylanl1 679 |
. . . . . . . . 9
β’ (((πΉ:π΄βontoβπ΅ β§ π§ β π΄) β§ π¦ = (πΉβπ§)) β π§ β (β‘πΉ β {π¦})) |
11 | 10 | ex 414 |
. . . . . . . 8
β’ ((πΉ:π΄βontoβπ΅ β§ π§ β π΄) β (π¦ = (πΉβπ§) β π§ β (β‘πΉ β {π¦}))) |
12 | 11 | reximdva 3166 |
. . . . . . 7
β’ (πΉ:π΄βontoβπ΅ β (βπ§ β π΄ π¦ = (πΉβπ§) β βπ§ β π΄ π§ β (β‘πΉ β {π¦}))) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((πΉ:π΄βontoβπ΅ β§ π¦ β π΅) β (βπ§ β π΄ π¦ = (πΉβπ§) β βπ§ β π΄ π§ β (β‘πΉ β {π¦}))) |
14 | 3, 13 | mpd 15 |
. . . . 5
β’ ((πΉ:π΄βontoβπ΅ β§ π¦ β π΅) β βπ§ β π΄ π§ β (β‘πΉ β {π¦})) |
15 | 14 | adantll 713 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ π¦ β π΅) β βπ§ β π΄ π§ β (β‘πΉ β {π¦})) |
16 | 15 | ralrimiva 3144 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βontoβπ΅) β βπ¦ β π΅ βπ§ β π΄ π§ β (β‘πΉ β {π¦})) |
17 | | eleq1 2826 |
. . . 4
β’ (π§ = (πβπ¦) β (π§ β (β‘πΉ β {π¦}) β (πβπ¦) β (β‘πΉ β {π¦}))) |
18 | 17 | ac6sg 10431 |
. . 3
β’ (π΅ β V β (βπ¦ β π΅ βπ§ β π΄ π§ β (β‘πΉ β {π¦}) β βπ(π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦})))) |
19 | 2, 16, 18 | sylc 65 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βontoβπ΅) β βπ(π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) |
20 | | frn 6680 |
. . . . 5
β’ (π:π΅βΆπ΄ β ran π β π΄) |
21 | 20 | ad2antrl 727 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β ran π β π΄) |
22 | | vex 3452 |
. . . . . 6
β’ π β V |
23 | 22 | rnex 7854 |
. . . . 5
β’ ran π β V |
24 | 23 | elpw 4569 |
. . . 4
β’ (ran
π β π« π΄ β ran π β π΄) |
25 | 21, 24 | sylibr 233 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β ran π β π« π΄) |
26 | | fof 6761 |
. . . . . 6
β’ (πΉ:π΄βontoβπ΅ β πΉ:π΄βΆπ΅) |
27 | 26 | ad2antlr 726 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β πΉ:π΄βΆπ΅) |
28 | 27, 21 | fssresd 6714 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β (πΉ βΎ ran π):ran πβΆπ΅) |
29 | | ffn 6673 |
. . . . . 6
β’ (π:π΅βΆπ΄ β π Fn π΅) |
30 | 29 | ad2antrl 727 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β π Fn π΅) |
31 | | dffn3 6686 |
. . . . 5
β’ (π Fn π΅ β π:π΅βΆran π) |
32 | 30, 31 | sylib 217 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β π:π΅βΆran π) |
33 | | fvres 6866 |
. . . . . . . 8
β’ (π§ β ran π β ((πΉ βΎ ran π)βπ§) = (πΉβπ§)) |
34 | 33 | adantl 483 |
. . . . . . 7
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β ((πΉ βΎ ran π)βπ§) = (πΉβπ§)) |
35 | 34 | fveq2d 6851 |
. . . . . 6
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β (πβ((πΉ βΎ ran π)βπ§)) = (πβ(πΉβπ§))) |
36 | | nfv 1918 |
. . . . . . . . 9
β’
β²π¦(π΄ β π β§ πΉ:π΄βontoβπ΅) |
37 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π¦ π:π΅βΆπ΄ |
38 | | nfra1 3270 |
. . . . . . . . . 10
β’
β²π¦βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}) |
39 | 37, 38 | nfan 1903 |
. . . . . . . . 9
β’
β²π¦(π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦})) |
40 | 36, 39 | nfan 1903 |
. . . . . . . 8
β’
β²π¦((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) |
41 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦ π§ β ran π |
42 | 40, 41 | nfan 1903 |
. . . . . . 7
β’
β²π¦(((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) |
43 | | simpr 486 |
. . . . . . . . . . 11
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β (πβπ¦) = π§) |
44 | 43 | fveq2d 6851 |
. . . . . . . . . 10
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β (πΉβ(πβπ¦)) = (πΉβπ§)) |
45 | 4 | ad5antlr 734 |
. . . . . . . . . . 11
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β πΉ Fn π΄) |
46 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦})) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦})) |
48 | | simplr 768 |
. . . . . . . . . . . 12
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β π¦ β π΅) |
49 | | rspa 3234 |
. . . . . . . . . . . 12
β’
((βπ¦ β
π΅ (πβπ¦) β (β‘πΉ β {π¦}) β§ π¦ β π΅) β (πβπ¦) β (β‘πΉ β {π¦})) |
50 | 47, 48, 49 | syl2anc 585 |
. . . . . . . . . . 11
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β (πβπ¦) β (β‘πΉ β {π¦})) |
51 | | fniniseg 7015 |
. . . . . . . . . . . 12
β’ (πΉ Fn π΄ β ((πβπ¦) β (β‘πΉ β {π¦}) β ((πβπ¦) β π΄ β§ (πΉβ(πβπ¦)) = π¦))) |
52 | 51 | simplbda 501 |
. . . . . . . . . . 11
β’ ((πΉ Fn π΄ β§ (πβπ¦) β (β‘πΉ β {π¦})) β (πΉβ(πβπ¦)) = π¦) |
53 | 45, 50, 52 | syl2anc 585 |
. . . . . . . . . 10
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β (πΉβ(πβπ¦)) = π¦) |
54 | 44, 53 | eqtr3d 2779 |
. . . . . . . . 9
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β (πΉβπ§) = π¦) |
55 | 54 | fveq2d 6851 |
. . . . . . . 8
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β (πβ(πΉβπ§)) = (πβπ¦)) |
56 | 55, 43 | eqtrd 2777 |
. . . . . . 7
β’
((((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β§ π¦ β π΅) β§ (πβπ¦) = π§) β (πβ(πΉβπ§)) = π§) |
57 | | fvelrnb 6908 |
. . . . . . . . 9
β’ (π Fn π΅ β (π§ β ran π β βπ¦ β π΅ (πβπ¦) = π§)) |
58 | 57 | biimpa 478 |
. . . . . . . 8
β’ ((π Fn π΅ β§ π§ β ran π) β βπ¦ β π΅ (πβπ¦) = π§) |
59 | 30, 58 | sylan 581 |
. . . . . . 7
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β βπ¦ β π΅ (πβπ¦) = π§) |
60 | 42, 56, 59 | r19.29af 3254 |
. . . . . 6
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β (πβ(πΉβπ§)) = π§) |
61 | 35, 60 | eqtrd 2777 |
. . . . 5
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π§ β ran π) β (πβ((πΉ βΎ ran π)βπ§)) = π§) |
62 | 61 | ralrimiva 3144 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β βπ§ β ran π(πβ((πΉ βΎ ran π)βπ§)) = π§) |
63 | 32 | ffvelcdmda 7040 |
. . . . . . . 8
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π¦ β π΅) β (πβπ¦) β ran π) |
64 | | fvres 6866 |
. . . . . . . 8
β’ ((πβπ¦) β ran π β ((πΉ βΎ ran π)β(πβπ¦)) = (πΉβ(πβπ¦))) |
65 | 63, 64 | syl 17 |
. . . . . . 7
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π¦ β π΅) β ((πΉ βΎ ran π)β(πβπ¦)) = (πΉβ(πβπ¦))) |
66 | 4 | ad3antlr 730 |
. . . . . . . 8
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π¦ β π΅) β πΉ Fn π΄) |
67 | | simplrr 777 |
. . . . . . . . 9
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π¦ β π΅) β βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦})) |
68 | | simpr 486 |
. . . . . . . . 9
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π¦ β π΅) β π¦ β π΅) |
69 | 67, 68, 49 | syl2anc 585 |
. . . . . . . 8
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π¦ β π΅) β (πβπ¦) β (β‘πΉ β {π¦})) |
70 | 66, 69, 52 | syl2anc 585 |
. . . . . . 7
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π¦ β π΅) β (πΉβ(πβπ¦)) = π¦) |
71 | 65, 70 | eqtrd 2777 |
. . . . . 6
β’ ((((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β§ π¦ β π΅) β ((πΉ βΎ ran π)β(πβπ¦)) = π¦) |
72 | 71 | ex 414 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β (π¦ β π΅ β ((πΉ βΎ ran π)β(πβπ¦)) = π¦)) |
73 | 40, 72 | ralrimi 3243 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β βπ¦ β π΅ ((πΉ βΎ ran π)β(πβπ¦)) = π¦) |
74 | 28, 32, 62, 73 | 2fvidf1od 7249 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β (πΉ βΎ ran π):ran πβ1-1-ontoβπ΅) |
75 | | reseq2 5937 |
. . . . 5
β’ (π₯ = ran π β (πΉ βΎ π₯) = (πΉ βΎ ran π)) |
76 | | id 22 |
. . . . 5
β’ (π₯ = ran π β π₯ = ran π) |
77 | | eqidd 2738 |
. . . . 5
β’ (π₯ = ran π β π΅ = π΅) |
78 | 75, 76, 77 | f1oeq123d 6783 |
. . . 4
β’ (π₯ = ran π β ((πΉ βΎ π₯):π₯β1-1-ontoβπ΅ β (πΉ βΎ ran π):ran πβ1-1-ontoβπ΅)) |
79 | 78 | rspcev 3584 |
. . 3
β’ ((ran
π β π« π΄ β§ (πΉ βΎ ran π):ran πβ1-1-ontoβπ΅) β βπ₯ β π« π΄(πΉ βΎ π₯):π₯β1-1-ontoβπ΅) |
80 | 25, 74, 79 | syl2anc 585 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βontoβπ΅) β§ (π:π΅βΆπ΄ β§ βπ¦ β π΅ (πβπ¦) β (β‘πΉ β {π¦}))) β βπ₯ β π« π΄(πΉ βΎ π₯):π₯β1-1-ontoβπ΅) |
81 | 19, 80 | exlimddv 1939 |
1
β’ ((π΄ β π β§ πΉ:π΄βontoβπ΅) β βπ₯ β π« π΄(πΉ βΎ π₯):π₯β1-1-ontoβπ΅) |