Step | Hyp | Ref
| Expression |
1 | | fpwrelmapffslem.4 |
. . 3
β’ (π β π
= {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))}) |
2 | | relopabv 5781 |
. . . 4
β’ Rel
{β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))} |
3 | | releq 5736 |
. . . 4
β’ (π
= {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))} β (Rel π
β Rel {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))})) |
4 | 2, 3 | mpbiri 258 |
. . 3
β’ (π
= {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))} β Rel π
) |
5 | | relfi 31573 |
. . 3
β’ (Rel
π
β (π
β Fin β (dom π
β Fin β§ ran π
β Fin))) |
6 | 1, 4, 5 | 3syl 18 |
. 2
β’ (π β (π
β Fin β (dom π
β Fin β§ ran π
β Fin))) |
7 | | rexcom4 3270 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π΄ βπ§(π€ β π§ β§ π§ = (πΉβπ₯)) β βπ§βπ₯ β π΄ (π€ β π§ β§ π§ = (πΉβπ₯))) |
8 | | ancom 462 |
. . . . . . . . . . . . . . . 16
β’ ((π§ = (πΉβπ₯) β§ π€ β π§) β (π€ β π§ β§ π§ = (πΉβπ₯))) |
9 | 8 | exbii 1851 |
. . . . . . . . . . . . . . 15
β’
(βπ§(π§ = (πΉβπ₯) β§ π€ β π§) β βπ§(π€ β π§ β§ π§ = (πΉβπ₯))) |
10 | | fvex 6859 |
. . . . . . . . . . . . . . . 16
β’ (πΉβπ₯) β V |
11 | | eleq2 2823 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (πΉβπ₯) β (π€ β π§ β π€ β (πΉβπ₯))) |
12 | 10, 11 | ceqsexv 3496 |
. . . . . . . . . . . . . . 15
β’
(βπ§(π§ = (πΉβπ₯) β§ π€ β π§) β π€ β (πΉβπ₯)) |
13 | 9, 12 | bitr3i 277 |
. . . . . . . . . . . . . 14
β’
(βπ§(π€ β π§ β§ π§ = (πΉβπ₯)) β π€ β (πΉβπ₯)) |
14 | 13 | rexbii 3094 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π΄ βπ§(π€ β π§ β§ π§ = (πΉβπ₯)) β βπ₯ β π΄ π€ β (πΉβπ₯)) |
15 | | r19.42v 3184 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
π΄ (π€ β π§ β§ π§ = (πΉβπ₯)) β (π€ β π§ β§ βπ₯ β π΄ π§ = (πΉβπ₯))) |
16 | 15 | exbii 1851 |
. . . . . . . . . . . . 13
β’
(βπ§βπ₯ β π΄ (π€ β π§ β§ π§ = (πΉβπ₯)) β βπ§(π€ β π§ β§ βπ₯ β π΄ π§ = (πΉβπ₯))) |
17 | 7, 14, 16 | 3bitr3ri 302 |
. . . . . . . . . . . 12
β’
(βπ§(π€ β π§ β§ βπ₯ β π΄ π§ = (πΉβπ₯)) β βπ₯ β π΄ π€ β (πΉβπ₯)) |
18 | | df-rex 3071 |
. . . . . . . . . . . 12
β’
(βπ₯ β
π΄ π€ β (πΉβπ₯) β βπ₯(π₯ β π΄ β§ π€ β (πΉβπ₯))) |
19 | 17, 18 | bitr2i 276 |
. . . . . . . . . . 11
β’
(βπ₯(π₯ β π΄ β§ π€ β (πΉβπ₯)) β βπ§(π€ β π§ β§ βπ₯ β π΄ π§ = (πΉβπ₯))) |
20 | 19 | a1i 11 |
. . . . . . . . . 10
β’ (π β (βπ₯(π₯ β π΄ β§ π€ β (πΉβπ₯)) β βπ§(π€ β π§ β§ βπ₯ β π΄ π§ = (πΉβπ₯)))) |
21 | | vex 3451 |
. . . . . . . . . . 11
β’ π€ β V |
22 | | eleq1w 2817 |
. . . . . . . . . . . . 13
β’ (π¦ = π€ β (π¦ β (πΉβπ₯) β π€ β (πΉβπ₯))) |
23 | 22 | anbi2d 630 |
. . . . . . . . . . . 12
β’ (π¦ = π€ β ((π₯ β π΄ β§ π¦ β (πΉβπ₯)) β (π₯ β π΄ β§ π€ β (πΉβπ₯)))) |
24 | 23 | exbidv 1925 |
. . . . . . . . . . 11
β’ (π¦ = π€ β (βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯)) β βπ₯(π₯ β π΄ β§ π€ β (πΉβπ₯)))) |
25 | 21, 24 | elab 3634 |
. . . . . . . . . 10
β’ (π€ β {π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))} β βπ₯(π₯ β π΄ β§ π€ β (πΉβπ₯))) |
26 | | eluniab 4884 |
. . . . . . . . . 10
β’ (π€ β βͺ {π§
β£ βπ₯ β
π΄ π§ = (πΉβπ₯)} β βπ§(π€ β π§ β§ βπ₯ β π΄ π§ = (πΉβπ₯))) |
27 | 20, 25, 26 | 3bitr4g 314 |
. . . . . . . . 9
β’ (π β (π€ β {π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))} β π€ β βͺ {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)})) |
28 | 27 | eqrdv 2731 |
. . . . . . . 8
β’ (π β {π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))} = βͺ {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)}) |
29 | 28 | eleq1d 2819 |
. . . . . . 7
β’ (π β ({π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))} β Fin β βͺ {π§
β£ βπ₯ β
π΄ π§ = (πΉβπ₯)} β Fin)) |
30 | 29 | adantr 482 |
. . . . . 6
β’ ((π β§ dom π
β Fin) β ({π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))} β Fin β βͺ {π§
β£ βπ₯ β
π΄ π§ = (πΉβπ₯)} β Fin)) |
31 | | fpwrelmapffslem.3 |
. . . . . . . . . . 11
β’ (π β πΉ:π΄βΆπ« π΅) |
32 | | ffn 6672 |
. . . . . . . . . . 11
β’ (πΉ:π΄βΆπ« π΅ β πΉ Fn π΄) |
33 | | fnrnfv 6906 |
. . . . . . . . . . 11
β’ (πΉ Fn π΄ β ran πΉ = {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)}) |
34 | 31, 32, 33 | 3syl 18 |
. . . . . . . . . 10
β’ (π β ran πΉ = {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)}) |
35 | 34 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ dom π
β Fin) β ran πΉ = {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)}) |
36 | | 0ex 5268 |
. . . . . . . . . . 11
β’ β
β V |
37 | 36 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ dom π
β Fin) β β
β
V) |
38 | | fpwrelmapffslem.1 |
. . . . . . . . . . . 12
β’ π΄ β V |
39 | | fex 7180 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆπ« π΅ β§ π΄ β V) β πΉ β V) |
40 | 31, 38, 39 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β πΉ β V) |
41 | 40 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ dom π
β Fin) β πΉ β V) |
42 | 31 | ffund 6676 |
. . . . . . . . . . 11
β’ (π β Fun πΉ) |
43 | 42 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ dom π
β Fin) β Fun πΉ) |
44 | | opabdm 31583 |
. . . . . . . . . . . . . 14
β’ (π
= {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))} β dom π
= {π₯ β£ βπ¦(π₯ β π΄ β§ π¦ β (πΉβπ₯))}) |
45 | 1, 44 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β dom π
= {π₯ β£ βπ¦(π₯ β π΄ β§ π¦ β (πΉβπ₯))}) |
46 | 38, 39 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:π΄βΆπ« π΅ β πΉ β V) |
47 | | suppimacnv 8109 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β V β§ β
β
V) β (πΉ supp β
)
= (β‘πΉ β (V β
{β
}))) |
48 | 36, 47 | mpan2 690 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β V β (πΉ supp β
) = (β‘πΉ β (V β
{β
}))) |
49 | 31, 46, 48 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΉ supp β
) = (β‘πΉ β (V β
{β
}))) |
50 | 31 | feqmptd 6914 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ = (π₯ β π΄ β¦ (πΉβπ₯))) |
51 | 50 | cnveqd 5835 |
. . . . . . . . . . . . . . . . 17
β’ (π β β‘πΉ = β‘(π₯ β π΄ β¦ (πΉβπ₯))) |
52 | 51 | imaeq1d 6016 |
. . . . . . . . . . . . . . . 16
β’ (π β (β‘πΉ β (V β {β
})) = (β‘(π₯ β π΄ β¦ (πΉβπ₯)) β (V β
{β
}))) |
53 | 49, 52 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ supp β
) = (β‘(π₯ β π΄ β¦ (πΉβπ₯)) β (V β
{β
}))) |
54 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π΄ β¦ (πΉβπ₯)) = (π₯ β π΄ β¦ (πΉβπ₯)) |
55 | 54 | mptpreima 6194 |
. . . . . . . . . . . . . . 15
β’ (β‘(π₯ β π΄ β¦ (πΉβπ₯)) β (V β {β
})) = {π₯ β π΄ β£ (πΉβπ₯) β (V β
{β
})} |
56 | 53, 55 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
β’ (π β (πΉ supp β
) = {π₯ β π΄ β£ (πΉβπ₯) β (V β
{β
})}) |
57 | | suppvalfn 8104 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ Fn π΄ β§ π΄ β V β§ β
β V) β
(πΉ supp β
) = {π₯ β π΄ β£ (πΉβπ₯) β β
}) |
58 | 38, 36, 57 | mp3an23 1454 |
. . . . . . . . . . . . . . . 16
β’ (πΉ Fn π΄ β (πΉ supp β
) = {π₯ β π΄ β£ (πΉβπ₯) β β
}) |
59 | 31, 32, 58 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ supp β
) = {π₯ β π΄ β£ (πΉβπ₯) β β
}) |
60 | | n0 4310 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ₯) β β
β βπ¦ π¦ β (πΉβπ₯)) |
61 | 60 | rabbii 3412 |
. . . . . . . . . . . . . . . 16
β’ {π₯ β π΄ β£ (πΉβπ₯) β β
} = {π₯ β π΄ β£ βπ¦ π¦ β (πΉβπ₯)} |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β {π₯ β π΄ β£ (πΉβπ₯) β β
} = {π₯ β π΄ β£ βπ¦ π¦ β (πΉβπ₯)}) |
63 | 59, 56, 62 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
β’ (π β {π₯ β π΄ β£ (πΉβπ₯) β (V β {β
})} = {π₯ β π΄ β£ βπ¦ π¦ β (πΉβπ₯)}) |
64 | | df-rab 3407 |
. . . . . . . . . . . . . . . 16
β’ {π₯ β π΄ β£ βπ¦ π¦ β (πΉβπ₯)} = {π₯ β£ (π₯ β π΄ β§ βπ¦ π¦ β (πΉβπ₯))} |
65 | | 19.42v 1958 |
. . . . . . . . . . . . . . . . 17
β’
(βπ¦(π₯ β π΄ β§ π¦ β (πΉβπ₯)) β (π₯ β π΄ β§ βπ¦ π¦ β (πΉβπ₯))) |
66 | 65 | abbii 2803 |
. . . . . . . . . . . . . . . 16
β’ {π₯ β£ βπ¦(π₯ β π΄ β§ π¦ β (πΉβπ₯))} = {π₯ β£ (π₯ β π΄ β§ βπ¦ π¦ β (πΉβπ₯))} |
67 | 64, 66 | eqtr4i 2764 |
. . . . . . . . . . . . . . 15
β’ {π₯ β π΄ β£ βπ¦ π¦ β (πΉβπ₯)} = {π₯ β£ βπ¦(π₯ β π΄ β§ π¦ β (πΉβπ₯))} |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β {π₯ β π΄ β£ βπ¦ π¦ β (πΉβπ₯)} = {π₯ β£ βπ¦(π₯ β π΄ β§ π¦ β (πΉβπ₯))}) |
69 | 56, 63, 68 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (π β (πΉ supp β
) = {π₯ β£ βπ¦(π₯ β π΄ β§ π¦ β (πΉβπ₯))}) |
70 | 45, 69 | eqtr4d 2776 |
. . . . . . . . . . . 12
β’ (π β dom π
= (πΉ supp β
)) |
71 | 70 | eleq1d 2819 |
. . . . . . . . . . 11
β’ (π β (dom π
β Fin β (πΉ supp β
) β Fin)) |
72 | 71 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β§ dom π
β Fin) β (πΉ supp β
) β Fin) |
73 | 37, 41, 43, 72 | ffsrn 31700 |
. . . . . . . . 9
β’ ((π β§ dom π
β Fin) β ran πΉ β Fin) |
74 | 35, 73 | eqeltrrd 2835 |
. . . . . . . 8
β’ ((π β§ dom π
β Fin) β {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin) |
75 | | unifi 9291 |
. . . . . . . . 9
β’ (({π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin β§ {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin) β βͺ {π§
β£ βπ₯ β
π΄ π§ = (πΉβπ₯)} β Fin) |
76 | 75 | ex 414 |
. . . . . . . 8
β’ ({π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin β ({π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin β βͺ {π§
β£ βπ₯ β
π΄ π§ = (πΉβπ₯)} β Fin)) |
77 | 74, 76 | syl 17 |
. . . . . . 7
β’ ((π β§ dom π
β Fin) β ({π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin β βͺ {π§
β£ βπ₯ β
π΄ π§ = (πΉβπ₯)} β Fin)) |
78 | | unifi3 31683 |
. . . . . . 7
β’ (βͺ {π§
β£ βπ₯ β
π΄ π§ = (πΉβπ₯)} β Fin β {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin) |
79 | 77, 78 | impbid1 224 |
. . . . . 6
β’ ((π β§ dom π
β Fin) β ({π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin β βͺ {π§
β£ βπ₯ β
π΄ π§ = (πΉβπ₯)} β Fin)) |
80 | 30, 79 | bitr4d 282 |
. . . . 5
β’ ((π β§ dom π
β Fin) β ({π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))} β Fin β {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin)) |
81 | | opabrn 31584 |
. . . . . . . 8
β’ (π
= {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))} β ran π
= {π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))}) |
82 | 1, 81 | syl 17 |
. . . . . . 7
β’ (π β ran π
= {π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))}) |
83 | 82 | eleq1d 2819 |
. . . . . 6
β’ (π β (ran π
β Fin β {π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))} β Fin)) |
84 | 83 | adantr 482 |
. . . . 5
β’ ((π β§ dom π
β Fin) β (ran π
β Fin β {π¦ β£ βπ₯(π₯ β π΄ β§ π¦ β (πΉβπ₯))} β Fin)) |
85 | 35 | sseq1d 3979 |
. . . . 5
β’ ((π β§ dom π
β Fin) β (ran πΉ β Fin β {π§ β£ βπ₯ β π΄ π§ = (πΉβπ₯)} β Fin)) |
86 | 80, 84, 85 | 3bitr4d 311 |
. . . 4
β’ ((π β§ dom π
β Fin) β (ran π
β Fin β ran πΉ β Fin)) |
87 | 86 | pm5.32da 580 |
. . 3
β’ (π β ((dom π
β Fin β§ ran π
β Fin) β (dom π
β Fin β§ ran πΉ β Fin))) |
88 | 71 | anbi1d 631 |
. . 3
β’ (π β ((dom π
β Fin β§ ran πΉ β Fin) β ((πΉ supp β
) β Fin β§ ran πΉ β Fin))) |
89 | 87, 88 | bitrd 279 |
. 2
β’ (π β ((dom π
β Fin β§ ran π
β Fin) β ((πΉ supp β
) β Fin β§ ran πΉ β Fin))) |
90 | | ancom 462 |
. . 3
β’ (((πΉ supp β
) β Fin β§
ran πΉ β Fin) β
(ran πΉ β Fin β§
(πΉ supp β
) β
Fin)) |
91 | 90 | a1i 11 |
. 2
β’ (π β (((πΉ supp β
) β Fin β§ ran πΉ β Fin) β (ran πΉ β Fin β§ (πΉ supp β
) β
Fin))) |
92 | 6, 89, 91 | 3bitrd 305 |
1
β’ (π β (π
β Fin β (ran πΉ β Fin β§ (πΉ supp β
) β
Fin))) |