Step | Hyp | Ref
| Expression |
1 | | actfunsn.5 |
. . 3
β’ πΉ = (π₯ β π΄ β¦ (π₯ βͺ {β¨πΌ, πβ©})) |
2 | | uneq1 4120 |
. . . 4
β’ (π₯ = π§ β (π₯ βͺ {β¨πΌ, πβ©}) = (π§ βͺ {β¨πΌ, πβ©})) |
3 | 2 | cbvmptv 5222 |
. . 3
β’ (π₯ β π΄ β¦ (π₯ βͺ {β¨πΌ, πβ©})) = (π§ β π΄ β¦ (π§ βͺ {β¨πΌ, πβ©})) |
4 | 1, 3 | eqtri 2761 |
. 2
β’ πΉ = (π§ β π΄ β¦ (π§ βͺ {β¨πΌ, πβ©})) |
5 | | vex 3451 |
. . . 4
β’ π§ β V |
6 | | snex 5392 |
. . . 4
β’
{β¨πΌ, πβ©} β
V |
7 | 5, 6 | unex 7684 |
. . 3
β’ (π§ βͺ {β¨πΌ, πβ©}) β V |
8 | 7 | a1i 11 |
. 2
β’ (((π β§ π β πΆ) β§ π§ β π΄) β (π§ βͺ {β¨πΌ, πβ©}) β V) |
9 | | vex 3451 |
. . . 4
β’ π¦ β V |
10 | 9 | resex 5989 |
. . 3
β’ (π¦ βΎ π΅) β V |
11 | 10 | a1i 11 |
. 2
β’ (((π β§ π β πΆ) β§ π¦ β ran πΉ) β (π¦ βΎ π΅) β V) |
12 | | rspe 3231 |
. . . . . . 7
β’ ((π§ β π΄ β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β βπ§ β π΄ π¦ = (π§ βͺ {β¨πΌ, πβ©})) |
13 | 4, 7 | elrnmpti 5919 |
. . . . . . 7
β’ (π¦ β ran πΉ β βπ§ β π΄ π¦ = (π§ βͺ {β¨πΌ, πβ©})) |
14 | 12, 13 | sylibr 233 |
. . . . . 6
β’ ((π§ β π΄ β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π¦ β ran πΉ) |
15 | 14 | adantll 713 |
. . . . 5
β’ ((((π β§ π β πΆ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π¦ β ran πΉ) |
16 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ π β πΆ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π¦ = (π§ βͺ {β¨πΌ, πβ©})) |
17 | 16 | reseq1d 5940 |
. . . . . 6
β’ ((((π β§ π β πΆ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β (π¦ βΎ π΅) = ((π§ βͺ {β¨πΌ, πβ©}) βΎ π΅)) |
18 | | actfunsn.1 |
. . . . . . . . . 10
β’ ((π β§ π β πΆ) β π΄ β (πΆ βm π΅)) |
19 | 18 | sselda 3948 |
. . . . . . . . 9
β’ (((π β§ π β πΆ) β§ π§ β π΄) β π§ β (πΆ βm π΅)) |
20 | | elmapfn 8809 |
. . . . . . . . 9
β’ (π§ β (πΆ βm π΅) β π§ Fn π΅) |
21 | 19, 20 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β πΆ) β§ π§ β π΄) β π§ Fn π΅) |
22 | | actfunsn.3 |
. . . . . . . . . 10
β’ (π β πΌ β π) |
23 | | fnsng 6557 |
. . . . . . . . . 10
β’ ((πΌ β π β§ π β πΆ) β {β¨πΌ, πβ©} Fn {πΌ}) |
24 | 22, 23 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β {β¨πΌ, πβ©} Fn {πΌ}) |
25 | 24 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β πΆ) β§ π§ β π΄) β {β¨πΌ, πβ©} Fn {πΌ}) |
26 | | actfunsn.4 |
. . . . . . . . . . 11
β’ (π β Β¬ πΌ β π΅) |
27 | | disjsn 4676 |
. . . . . . . . . . 11
β’ ((π΅ β© {πΌ}) = β
β Β¬ πΌ β π΅) |
28 | 26, 27 | sylibr 233 |
. . . . . . . . . 10
β’ (π β (π΅ β© {πΌ}) = β
) |
29 | 28 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β πΆ) β (π΅ β© {πΌ}) = β
) |
30 | 29 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β πΆ) β§ π§ β π΄) β (π΅ β© {πΌ}) = β
) |
31 | | fnunres1 31577 |
. . . . . . . 8
β’ ((π§ Fn π΅ β§ {β¨πΌ, πβ©} Fn {πΌ} β§ (π΅ β© {πΌ}) = β
) β ((π§ βͺ {β¨πΌ, πβ©}) βΎ π΅) = π§) |
32 | 21, 25, 30, 31 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ π§ β π΄) β ((π§ βͺ {β¨πΌ, πβ©}) βΎ π΅) = π§) |
33 | 32 | adantr 482 |
. . . . . 6
β’ ((((π β§ π β πΆ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β ((π§ βͺ {β¨πΌ, πβ©}) βΎ π΅) = π§) |
34 | 17, 33 | eqtr2d 2774 |
. . . . 5
β’ ((((π β§ π β πΆ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π§ = (π¦ βΎ π΅)) |
35 | 15, 34 | jca 513 |
. . . 4
β’ ((((π β§ π β πΆ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β (π¦ β ran πΉ β§ π§ = (π¦ βΎ π΅))) |
36 | 35 | anasss 468 |
. . 3
β’ (((π β§ π β πΆ) β§ (π§ β π΄ β§ π¦ = (π§ βͺ {β¨πΌ, πβ©}))) β (π¦ β ran πΉ β§ π§ = (π¦ βΎ π΅))) |
37 | | simpr 486 |
. . . . . 6
β’ ((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ = (π¦ βΎ π΅)) β π§ = (π¦ βΎ π΅)) |
38 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π¦ = (π§ βͺ {β¨πΌ, πβ©})) |
39 | 38 | reseq1d 5940 |
. . . . . . . . 9
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β (π¦ βΎ π΅) = ((π§ βͺ {β¨πΌ, πβ©}) βΎ π΅)) |
40 | 18 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π΄ β (πΆ βm π΅)) |
41 | | simplr 768 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π§ β π΄) |
42 | 40, 41 | sseldd 3949 |
. . . . . . . . . . . 12
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π§ β (πΆ βm π΅)) |
43 | 42, 20 | syl 17 |
. . . . . . . . . . 11
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π§ Fn π΅) |
44 | 22 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β πΌ β π) |
45 | | simp-4r 783 |
. . . . . . . . . . . 12
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β π β πΆ) |
46 | 44, 45, 23 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β {β¨πΌ, πβ©} Fn {πΌ}) |
47 | 28 | ad4antr 731 |
. . . . . . . . . . 11
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β (π΅ β© {πΌ}) = β
) |
48 | 43, 46, 47, 31 | syl3anc 1372 |
. . . . . . . . . 10
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β ((π§ βͺ {β¨πΌ, πβ©}) βΎ π΅) = π§) |
49 | 48, 41 | eqeltrd 2834 |
. . . . . . . . 9
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β ((π§ βͺ {β¨πΌ, πβ©}) βΎ π΅) β π΄) |
50 | 39, 49 | eqeltrd 2834 |
. . . . . . . 8
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β (π¦ βΎ π΅) β π΄) |
51 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π β πΆ) β§ π¦ β ran πΉ) β π¦ β ran πΉ) |
52 | 51, 13 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π β πΆ) β§ π¦ β ran πΉ) β βπ§ β π΄ π¦ = (π§ βͺ {β¨πΌ, πβ©})) |
53 | 50, 52 | r19.29a 3156 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ π¦ β ran πΉ) β (π¦ βΎ π΅) β π΄) |
54 | 53 | adantr 482 |
. . . . . 6
β’ ((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ = (π¦ βΎ π΅)) β (π¦ βΎ π΅) β π΄) |
55 | 37, 54 | eqeltrd 2834 |
. . . . 5
β’ ((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ = (π¦ βΎ π΅)) β π§ β π΄) |
56 | 37 | uneq1d 4126 |
. . . . . 6
β’ ((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ = (π¦ βΎ π΅)) β (π§ βͺ {β¨πΌ, πβ©}) = ((π¦ βΎ π΅) βͺ {β¨πΌ, πβ©})) |
57 | 39, 48 | eqtrd 2773 |
. . . . . . . . . 10
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β (π¦ βΎ π΅) = π§) |
58 | 57 | uneq1d 4126 |
. . . . . . . . 9
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β ((π¦ βΎ π΅) βͺ {β¨πΌ, πβ©}) = (π§ βͺ {β¨πΌ, πβ©})) |
59 | 58, 38 | eqtr4d 2776 |
. . . . . . . 8
β’
(((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ β π΄) β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β ((π¦ βΎ π΅) βͺ {β¨πΌ, πβ©}) = π¦) |
60 | 59, 52 | r19.29a 3156 |
. . . . . . 7
β’ (((π β§ π β πΆ) β§ π¦ β ran πΉ) β ((π¦ βΎ π΅) βͺ {β¨πΌ, πβ©}) = π¦) |
61 | 60 | adantr 482 |
. . . . . 6
β’ ((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ = (π¦ βΎ π΅)) β ((π¦ βΎ π΅) βͺ {β¨πΌ, πβ©}) = π¦) |
62 | 56, 61 | eqtr2d 2774 |
. . . . 5
β’ ((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ = (π¦ βΎ π΅)) β π¦ = (π§ βͺ {β¨πΌ, πβ©})) |
63 | 55, 62 | jca 513 |
. . . 4
β’ ((((π β§ π β πΆ) β§ π¦ β ran πΉ) β§ π§ = (π¦ βΎ π΅)) β (π§ β π΄ β§ π¦ = (π§ βͺ {β¨πΌ, πβ©}))) |
64 | 63 | anasss 468 |
. . 3
β’ (((π β§ π β πΆ) β§ (π¦ β ran πΉ β§ π§ = (π¦ βΎ π΅))) β (π§ β π΄ β§ π¦ = (π§ βͺ {β¨πΌ, πβ©}))) |
65 | 36, 64 | impbida 800 |
. 2
β’ ((π β§ π β πΆ) β ((π§ β π΄ β§ π¦ = (π§ βͺ {β¨πΌ, πβ©})) β (π¦ β ran πΉ β§ π§ = (π¦ βΎ π΅)))) |
66 | 4, 8, 11, 65 | f1od 7609 |
1
β’ ((π β§ π β πΆ) β πΉ:π΄β1-1-ontoβran
πΉ) |