Step | Hyp | Ref
| Expression |
1 | | smfpimcc.z |
. . . . . . 7
β’ π =
(β€β₯βπ) |
2 | 1 | uzct 44052 |
. . . . . 6
β’ π βΌ
Ο |
3 | 2 | a1i 11 |
. . . . 5
β’ (π β π βΌ Ο) |
4 | | mptct 10535 |
. . . . 5
β’ (π βΌ Ο β (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) βΌ Ο) |
5 | | rnct 10522 |
. . . . 5
β’ ((π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) βΌ Ο β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) βΌ Ο) |
6 | 3, 4, 5 | 3syl 18 |
. . . 4
β’ (π β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) βΌ Ο) |
7 | | vex 3478 |
. . . . . . . 8
β’ π¦ β V |
8 | | eqid 2732 |
. . . . . . . . 9
β’ (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) = (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) |
9 | 8 | elrnmpt 5955 |
. . . . . . . 8
β’ (π¦ β V β (π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) β βπ β π π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) |
10 | 7, 9 | ax-mp 5 |
. . . . . . 7
β’ (π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) β βπ β π π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) |
11 | 10 | biimpi 215 |
. . . . . 6
β’ (π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) β βπ β π π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) |
12 | 11 | adantl 482 |
. . . . 5
β’ ((π β§ π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β βπ β π π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) |
13 | | simp3 1138 |
. . . . . . . . 9
β’ ((π β§ π β π β§ π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) β π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) |
14 | | smfpimcc.s |
. . . . . . . . . . . . . 14
β’ (π β π β SAlg) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β SAlg) |
16 | | smfpimcc.f |
. . . . . . . . . . . . . 14
β’ (π β πΉ:πβΆ(SMblFnβπ)) |
17 | 16 | ffvelcdmda 7086 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (πΉβπ) β (SMblFnβπ)) |
18 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ dom
(πΉβπ) = dom (πΉβπ) |
19 | | smfpimcc.j |
. . . . . . . . . . . . 13
β’ π½ = (topGenβran
(,)) |
20 | | smfpimcc.b |
. . . . . . . . . . . . 13
β’ π΅ = (SalGenβπ½) |
21 | | smfpimcc.a |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π΅) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π΄ β π΅) |
23 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ (β‘(πΉβπ) β π΄) = (β‘(πΉβπ) β π΄) |
24 | 15, 17, 18, 19, 20, 22, 23 | smfpimbor1 45815 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (β‘(πΉβπ) β π΄) β (π βΎt dom (πΉβπ))) |
25 | | fvex 6904 |
. . . . . . . . . . . . . . . 16
β’ (πΉβπ) β V |
26 | 25 | dmex 7904 |
. . . . . . . . . . . . . . 15
β’ dom
(πΉβπ) β V |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β dom (πΉβπ) β V) |
28 | | elrest 17377 |
. . . . . . . . . . . . . 14
β’ ((π β SAlg β§ dom (πΉβπ) β V) β ((β‘(πΉβπ) β π΄) β (π βΎt dom (πΉβπ)) β βπ β π (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ)))) |
29 | 14, 27, 28 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (π β ((β‘(πΉβπ) β π΄) β (π βΎt dom (πΉβπ)) β βπ β π (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ)))) |
30 | 29 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β ((β‘(πΉβπ) β π΄) β (π βΎt dom (πΉβπ)) β βπ β π (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ)))) |
31 | 24, 30 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β βπ β π (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))) |
32 | | rabn0 4385 |
. . . . . . . . . . 11
β’ ({π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))} β β
β βπ β π (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))) |
33 | 31, 32 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ π β π) β {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))} β β
) |
34 | 33 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π β§ π β π β§ π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) β {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))} β β
) |
35 | 13, 34 | eqnetrd 3008 |
. . . . . . . 8
β’ ((π β§ π β π β§ π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) β π¦ β β
) |
36 | 35 | 3exp 1119 |
. . . . . . 7
β’ (π β (π β π β (π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))} β π¦ β β
))) |
37 | 36 | rexlimdv 3153 |
. . . . . 6
β’ (π β (βπ β π π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))} β π¦ β β
)) |
38 | 37 | adantr 481 |
. . . . 5
β’ ((π β§ π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β (βπ β π π¦ = {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))} β π¦ β β
)) |
39 | 12, 38 | mpd 15 |
. . . 4
β’ ((π β§ π¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β π¦ β β
) |
40 | 6, 39 | axccd2 44228 |
. . 3
β’ (π β βπβπ¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦) |
41 | | nfv 1917 |
. . . . . . 7
β’
β²ππ |
42 | | nfmpt1 5256 |
. . . . . . . . 9
β’
β²π(π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) |
43 | 42 | nfrn 5951 |
. . . . . . . 8
β’
β²πran
(π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))}) |
44 | | nfv 1917 |
. . . . . . . 8
β’
β²π(πβπ¦) β π¦ |
45 | 43, 44 | nfralw 3308 |
. . . . . . 7
β’
β²πβπ¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦ |
46 | 41, 45 | nfan 1902 |
. . . . . 6
β’
β²π(π β§ βπ¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦) |
47 | 1 | fvexi 6905 |
. . . . . 6
β’ π β V |
48 | 14 | adantr 481 |
. . . . . 6
β’ ((π β§ βπ¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦) β π β SAlg) |
49 | | fveq2 6891 |
. . . . . . . . 9
β’ (π¦ = π€ β (πβπ¦) = (πβπ€)) |
50 | | id 22 |
. . . . . . . . 9
β’ (π¦ = π€ β π¦ = π€) |
51 | 49, 50 | eleq12d 2827 |
. . . . . . . 8
β’ (π¦ = π€ β ((πβπ¦) β π¦ β (πβπ€) β π€)) |
52 | 51 | rspccva 3611 |
. . . . . . 7
β’
((βπ¦ β
ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦ β§ π€ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β (πβπ€) β π€) |
53 | 52 | adantll 712 |
. . . . . 6
β’ (((π β§ βπ¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦) β§ π€ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) β (πβπ€) β π€) |
54 | | eqid 2732 |
. . . . . 6
β’ (π β π β¦ (πβ{π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) = (π β π β¦ (πβ{π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})) |
55 | 46, 47, 48, 53, 54 | smfpimcclem 45822 |
. . . . 5
β’ ((π β§ βπ¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦) β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) |
56 | 55 | ex 413 |
. . . 4
β’ (π β (βπ¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦ β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ))))) |
57 | 56 | exlimdv 1936 |
. . 3
β’ (π β (βπβπ¦ β ran (π β π β¦ {π β π β£ (β‘(πΉβπ) β π΄) = (π β© dom (πΉβπ))})(πβπ¦) β π¦ β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ))))) |
58 | 40, 57 | mpd 15 |
. 2
β’ (π β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) |
59 | | smfpimcc.1 |
. . . . . . . . 9
β’
β²ππΉ |
60 | | nfcv 2903 |
. . . . . . . . 9
β’
β²ππ |
61 | 59, 60 | nffv 6901 |
. . . . . . . 8
β’
β²π(πΉβπ) |
62 | 61 | nfcnv 5878 |
. . . . . . 7
β’
β²πβ‘(πΉβπ) |
63 | | nfcv 2903 |
. . . . . . 7
β’
β²ππ΄ |
64 | 62, 63 | nfima 6067 |
. . . . . 6
β’
β²π(β‘(πΉβπ) β π΄) |
65 | | nfcv 2903 |
. . . . . . 7
β’
β²π(ββπ) |
66 | 61 | nfdm 5950 |
. . . . . . 7
β’
β²πdom
(πΉβπ) |
67 | 65, 66 | nfin 4216 |
. . . . . 6
β’
β²π((ββπ) β© dom (πΉβπ)) |
68 | 64, 67 | nfeq 2916 |
. . . . 5
β’
β²π(β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)) |
69 | | nfv 1917 |
. . . . 5
β’
β²π(β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)) |
70 | | fveq2 6891 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
71 | 70 | cnveqd 5875 |
. . . . . . 7
β’ (π = π β β‘(πΉβπ) = β‘(πΉβπ)) |
72 | 71 | imaeq1d 6058 |
. . . . . 6
β’ (π = π β (β‘(πΉβπ) β π΄) = (β‘(πΉβπ) β π΄)) |
73 | | fveq2 6891 |
. . . . . . 7
β’ (π = π β (ββπ) = (ββπ)) |
74 | 70 | dmeqd 5905 |
. . . . . . 7
β’ (π = π β dom (πΉβπ) = dom (πΉβπ)) |
75 | 73, 74 | ineq12d 4213 |
. . . . . 6
β’ (π = π β ((ββπ) β© dom (πΉβπ)) = ((ββπ) β© dom (πΉβπ))) |
76 | 72, 75 | eqeq12d 2748 |
. . . . 5
β’ (π = π β ((β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)) β (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) |
77 | 68, 69, 76 | cbvralw 3303 |
. . . 4
β’
(βπ β
π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)) β βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ))) |
78 | 77 | anbi2i 623 |
. . 3
β’ ((β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ))) β (β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) |
79 | 78 | exbii 1850 |
. 2
β’
(ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ))) β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) |
80 | 58, 79 | sylib 217 |
1
β’ (π β ββ(β:πβΆπ β§ βπ β π (β‘(πΉβπ) β π΄) = ((ββπ) β© dom (πΉβπ)))) |