Step | Hyp | Ref
| Expression |
1 | | fnfvelrn 7036 |
. . . . . 6
β’ ((πΉ Fn π΄ β§ π β π΄) β (πΉβπ) β ran πΉ) |
2 | 1 | ex 414 |
. . . . 5
β’ (πΉ Fn π΄ β (π β π΄ β (πΉβπ) β ran πΉ)) |
3 | 2 | adantr 482 |
. . . 4
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π β π΄ β (πΉβπ) β ran πΉ)) |
4 | | fnrnfv 6907 |
. . . . . . . . . 10
β’ (πΉ Fn π΄ β ran πΉ = {π¦ β£ βπ β π΄ π¦ = (πΉβπ)}) |
5 | 4 | eqabd 2881 |
. . . . . . . . 9
β’ (πΉ Fn π΄ β (π¦ β ran πΉ β βπ β π΄ π¦ = (πΉβπ))) |
6 | 5 | adantr 482 |
. . . . . . . 8
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π¦ β ran πΉ β βπ β π΄ π¦ = (πΉβπ))) |
7 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π πΉ Fn π΄ |
8 | | nfra1 3270 |
. . . . . . . . . 10
β’
β²πβπ β π΄ ((πΉβπ) β© π΄) = {π} |
9 | 7, 8 | nfan 1903 |
. . . . . . . . 9
β’
β²π(πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) |
10 | | nfv 1918 |
. . . . . . . . 9
β’
β²πβπ β π΄ (π β π¦ β π¦ = (πΉβπ)) |
11 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (πΉβπ) β (π β π¦ β π β (πΉβπ))) |
12 | | elin 3931 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((πΉβπ) β© π΄) β (π β (πΉβπ) β§ π β π΄)) |
13 | 12 | rbaib 540 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β (π β ((πΉβπ) β© π΄) β π β (πΉβπ))) |
14 | 13 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β (π β ((πΉβπ) β© π΄) β π β (πΉβπ))) |
15 | | rsp 3233 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ β
π΄ ((πΉβπ) β© π΄) = {π} β (π β π΄ β ((πΉβπ) β© π΄) = {π})) |
16 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΉβπ) β© π΄) = {π} β (π β ((πΉβπ) β© π΄) β π β {π})) |
17 | | velsn 4607 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β {π} β π = π) |
18 | | equcom 2022 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β π = π) |
19 | 17, 18 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β {π} β π = π) |
20 | 16, 19 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΉβπ) β© π΄) = {π} β (π β ((πΉβπ) β© π΄) β π = π)) |
21 | 15, 20 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ β
π΄ ((πΉβπ) β© π΄) = {π} β (π β π΄ β (π β ((πΉβπ) β© π΄) β π = π))) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π β π΄ β (π β ((πΉβπ) β© π΄) β π = π))) |
23 | 22 | adantrd 493 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β ((π β π΄ β§ π β π΄) β (π β ((πΉβπ) β© π΄) β π = π))) |
24 | 23 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β (π β ((πΉβπ) β© π΄) β π = π)) |
25 | 14, 24 | bitr3d 281 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β (π β (πΉβπ) β π = π)) |
26 | 11, 25 | sylan9bbr 512 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β§ π¦ = (πΉβπ)) β (π β π¦ β π = π)) |
27 | 26 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β (π¦ = (πΉβπ) β (π β π¦ β π = π))) |
28 | 27 | anass1rs 654 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ π β π΄) β§ π β π΄) β (π¦ = (πΉβπ) β (π β π¦ β π = π))) |
29 | 28 | impr 456 |
. . . . . . . . . . . . . 14
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ π β π΄) β§ (π β π΄ β§ π¦ = (πΉβπ))) β (π β π¦ β π = π)) |
30 | 29 | an32s 651 |
. . . . . . . . . . . . 13
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π¦ = (πΉβπ))) β§ π β π΄) β (π β π¦ β π = π)) |
31 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = (πΉβπ) β (π¦ = (πΉβπ) β (πΉβπ) = (πΉβπ))) |
32 | | dffn3 6686 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΉ Fn π΄ β πΉ:π΄βΆran πΉ) |
33 | | fvineqsnf1 35910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ:π΄βΆran πΉ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β πΉ:π΄β1-1βran πΉ) |
34 | 32, 33 | sylanb 582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β πΉ:π΄β1-1βran πΉ) |
35 | | dff13 7207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πΉ:π΄β1-1βran πΉ β (πΉ:π΄βΆran πΉ β§ βπ β π΄ βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π))) |
36 | 34, 35 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (πΉ:π΄βΆran πΉ β§ βπ β π΄ βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π))) |
37 | 36 | simprd 497 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β βπ β π΄ βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π)) |
38 | | rsp 3233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ β
π΄ βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π) β (π β π΄ β βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π))) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π β π΄ β βπ β π΄ ((πΉβπ) = (πΉβπ) β π = π))) |
40 | | rsp 3233 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
π΄ ((πΉβπ) = (πΉβπ) β π = π) β (π β π΄ β ((πΉβπ) = (πΉβπ) β π = π))) |
41 | 39, 40 | syl6 35 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π β π΄ β (π β π΄ β ((πΉβπ) = (πΉβπ) β π = π)))) |
42 | 41 | imp32 420 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β ((πΉβπ) = (πΉβπ) β π = π)) |
43 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΉβπ) = (πΉβπ)) |
44 | 42, 43 | impbid1 224 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β ((πΉβπ) = (πΉβπ) β π = π)) |
45 | 31, 44 | sylan9bbr 512 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β§ π¦ = (πΉβπ)) β (π¦ = (πΉβπ) β π = π)) |
46 | 45 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π β π΄)) β (π¦ = (πΉβπ) β (π¦ = (πΉβπ) β π = π))) |
47 | 46 | anass1rs 654 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ π β π΄) β§ π β π΄) β (π¦ = (πΉβπ) β (π¦ = (πΉβπ) β π = π))) |
48 | 47 | impr 456 |
. . . . . . . . . . . . . 14
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ π β π΄) β§ (π β π΄ β§ π¦ = (πΉβπ))) β (π¦ = (πΉβπ) β π = π)) |
49 | 48 | an32s 651 |
. . . . . . . . . . . . 13
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π¦ = (πΉβπ))) β§ π β π΄) β (π¦ = (πΉβπ) β π = π)) |
50 | 30, 49 | bitr4d 282 |
. . . . . . . . . . . 12
β’ ((((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π¦ = (πΉβπ))) β§ π β π΄) β (π β π¦ β π¦ = (πΉβπ))) |
51 | 50 | ex 414 |
. . . . . . . . . . 11
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π¦ = (πΉβπ))) β (π β π΄ β (π β π¦ β π¦ = (πΉβπ)))) |
52 | 51 | ralrimiv 3143 |
. . . . . . . . . 10
β’ (((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β§ (π β π΄ β§ π¦ = (πΉβπ))) β βπ β π΄ (π β π¦ β π¦ = (πΉβπ))) |
53 | 52 | exp32 422 |
. . . . . . . . 9
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π β π΄ β (π¦ = (πΉβπ) β βπ β π΄ (π β π¦ β π¦ = (πΉβπ))))) |
54 | 9, 10, 53 | rexlimd 3252 |
. . . . . . . 8
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (βπ β π΄ π¦ = (πΉβπ) β βπ β π΄ (π β π¦ β π¦ = (πΉβπ)))) |
55 | 6, 54 | sylbid 239 |
. . . . . . 7
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π¦ β ran πΉ β βπ β π΄ (π β π¦ β π¦ = (πΉβπ)))) |
56 | | rsp 3233 |
. . . . . . 7
β’
(βπ β
π΄ (π β π¦ β π¦ = (πΉβπ)) β (π β π΄ β (π β π¦ β π¦ = (πΉβπ)))) |
57 | 55, 56 | syl6 35 |
. . . . . 6
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π¦ β ran πΉ β (π β π΄ β (π β π¦ β π¦ = (πΉβπ))))) |
58 | 57 | com23 86 |
. . . . 5
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π β π΄ β (π¦ β ran πΉ β (π β π¦ β π¦ = (πΉβπ))))) |
59 | 58 | ralrimdv 3150 |
. . . 4
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π β π΄ β βπ¦ β ran πΉ(π β π¦ β π¦ = (πΉβπ)))) |
60 | | reu6i 3691 |
. . . . 5
β’ (((πΉβπ) β ran πΉ β§ βπ¦ β ran πΉ(π β π¦ β π¦ = (πΉβπ))) β β!π¦ β ran πΉ π β π¦) |
61 | 60 | ex 414 |
. . . 4
β’ ((πΉβπ) β ran πΉ β (βπ¦ β ran πΉ(π β π¦ β π¦ = (πΉβπ)) β β!π¦ β ran πΉ π β π¦)) |
62 | 3, 59, 61 | syl6c 70 |
. . 3
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β (π β π΄ β β!π¦ β ran πΉ π β π¦)) |
63 | 62 | ralrimiv 3143 |
. 2
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β βπ β π΄ β!π¦ β ran πΉ π β π¦) |
64 | | nfv 1918 |
. . . 4
β’
β²π₯ π = π |
65 | | nfv 1918 |
. . . 4
β’
β²π¦ π = π |
66 | | nfvd 1919 |
. . . 4
β’ (π = π β β²π¦ π β π₯) |
67 | | nfvd 1919 |
. . . 4
β’ (π = π β β²π₯ π β π¦) |
68 | | eleq12 2828 |
. . . . 5
β’ ((π = π β§ π₯ = π¦) β (π β π₯ β π β π¦)) |
69 | 68 | ex 414 |
. . . 4
β’ (π = π β (π₯ = π¦ β (π β π₯ β π β π¦))) |
70 | 64, 65, 66, 67, 69 | cbvreud 35873 |
. . 3
β’ (π = π β (β!π₯ β ran πΉ π β π₯ β β!π¦ β ran πΉ π β π¦)) |
71 | 70 | cbvralvw 3228 |
. 2
β’
(βπ β
π΄ β!π₯ β ran πΉ π β π₯ β βπ β π΄ β!π¦ β ran πΉ π β π¦) |
72 | 63, 71 | sylibr 233 |
1
β’ ((πΉ Fn π΄ β§ βπ β π΄ ((πΉβπ) β© π΄) = {π}) β βπ β π΄ β!π₯ β ran πΉ π β π₯) |