Step | Hyp | Ref
| Expression |
1 | | acsmapd.4 |
. . . 4
β’ (π β π β (πβπ)) |
2 | | fvex 6859 |
. . . . 5
β’ (πβπ) β V |
3 | 2 | ssex 5282 |
. . . 4
β’ (π β (πβπ) β π β V) |
4 | 1, 3 | syl 17 |
. . 3
β’ (π β π β V) |
5 | 1 | sseld 3947 |
. . . . 5
β’ (π β (π₯ β π β π₯ β (πβπ))) |
6 | | acsmapd.1 |
. . . . . 6
β’ (π β π΄ β (ACSβπ)) |
7 | | acsmapd.2 |
. . . . . 6
β’ π = (mrClsβπ΄) |
8 | | acsmapd.3 |
. . . . . 6
β’ (π β π β π) |
9 | 6, 7, 8 | acsficl2d 18449 |
. . . . 5
β’ (π β (π₯ β (πβπ) β βπ¦ β (π« π β© Fin)π₯ β (πβπ¦))) |
10 | 5, 9 | sylibd 238 |
. . . 4
β’ (π β (π₯ β π β βπ¦ β (π« π β© Fin)π₯ β (πβπ¦))) |
11 | 10 | ralrimiv 3139 |
. . 3
β’ (π β βπ₯ β π βπ¦ β (π« π β© Fin)π₯ β (πβπ¦)) |
12 | | fveq2 6846 |
. . . . 5
β’ (π¦ = (πβπ₯) β (πβπ¦) = (πβ(πβπ₯))) |
13 | 12 | eleq2d 2820 |
. . . 4
β’ (π¦ = (πβπ₯) β (π₯ β (πβπ¦) β π₯ β (πβ(πβπ₯)))) |
14 | 13 | ac6sg 10432 |
. . 3
β’ (π β V β (βπ₯ β π βπ¦ β (π« π β© Fin)π₯ β (πβπ¦) β βπ(π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯))))) |
15 | 4, 11, 14 | sylc 65 |
. 2
β’ (π β βπ(π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) |
16 | | simprl 770 |
. . . . 5
β’ ((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β π:πβΆ(π« π β© Fin)) |
17 | | nfv 1918 |
. . . . . . . 8
β’
β²π₯π |
18 | | nfv 1918 |
. . . . . . . . 9
β’
β²π₯ π:πβΆ(π« π β© Fin) |
19 | | nfra1 3266 |
. . . . . . . . 9
β’
β²π₯βπ₯ β π π₯ β (πβ(πβπ₯)) |
20 | 18, 19 | nfan 1903 |
. . . . . . . 8
β’
β²π₯(π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯))) |
21 | 17, 20 | nfan 1903 |
. . . . . . 7
β’
β²π₯(π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) |
22 | 6 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β π΄ β (ACSβπ)) |
23 | 22 | acsmred 17544 |
. . . . . . . . . 10
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β π΄ β (Mooreβπ)) |
24 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β π:πβΆ(π« π β© Fin)) |
25 | 24 | ffnd 6673 |
. . . . . . . . . . . . 13
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β π Fn π) |
26 | | fnfvelrn 7035 |
. . . . . . . . . . . . 13
β’ ((π Fn π β§ π₯ β π) β (πβπ₯) β ran π) |
27 | 25, 26 | sylancom 589 |
. . . . . . . . . . . 12
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β (πβπ₯) β ran π) |
28 | 27 | snssd 4773 |
. . . . . . . . . . 11
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β {(πβπ₯)} β ran π) |
29 | 28 | unissd 4879 |
. . . . . . . . . 10
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β βͺ
{(πβπ₯)} β βͺ ran π) |
30 | | frn 6679 |
. . . . . . . . . . . . . 14
β’ (π:πβΆ(π« π β© Fin) β ran π β (π« π β© Fin)) |
31 | 30 | unissd 4879 |
. . . . . . . . . . . . 13
β’ (π:πβΆ(π« π β© Fin) β βͺ ran π β βͺ
(π« π β©
Fin)) |
32 | | unifpw 9305 |
. . . . . . . . . . . . 13
β’ βͺ (π« π β© Fin) = π |
33 | 31, 32 | sseqtrdi 3998 |
. . . . . . . . . . . 12
β’ (π:πβΆ(π« π β© Fin) β βͺ ran π β π) |
34 | 24, 33 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β βͺ ran
π β π) |
35 | 8 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β π β π) |
36 | 34, 35 | sstrd 3958 |
. . . . . . . . . 10
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β βͺ ran
π β π) |
37 | 23, 7, 29, 36 | mrcssd 17512 |
. . . . . . . . 9
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β (πββͺ {(πβπ₯)}) β (πββͺ ran
π)) |
38 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β βπ₯ β π π₯ β (πβ(πβπ₯))) |
39 | 38 | r19.21bi 3233 |
. . . . . . . . . 10
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β π₯ β (πβ(πβπ₯))) |
40 | | fvex 6859 |
. . . . . . . . . . . 12
β’ (πβπ₯) β V |
41 | 40 | unisn 4891 |
. . . . . . . . . . 11
β’ βͺ {(πβπ₯)} = (πβπ₯) |
42 | 41 | fveq2i 6849 |
. . . . . . . . . 10
β’ (πββͺ {(πβπ₯)}) = (πβ(πβπ₯)) |
43 | 39, 42 | eleqtrrdi 2845 |
. . . . . . . . 9
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β π₯ β (πββͺ {(πβπ₯)})) |
44 | 37, 43 | sseldd 3949 |
. . . . . . . 8
β’ (((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β§ π₯ β π) β π₯ β (πββͺ ran
π)) |
45 | 44 | ex 414 |
. . . . . . 7
β’ ((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β (π₯ β π β π₯ β (πββͺ ran
π))) |
46 | 21, 45 | alrimi 2207 |
. . . . . 6
β’ ((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β βπ₯(π₯ β π β π₯ β (πββͺ ran
π))) |
47 | | dfss2 3934 |
. . . . . 6
β’ (π β (πββͺ ran
π) β βπ₯(π₯ β π β π₯ β (πββͺ ran
π))) |
48 | 46, 47 | sylibr 233 |
. . . . 5
β’ ((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β π β (πββͺ ran
π)) |
49 | 16, 48 | jca 513 |
. . . 4
β’ ((π β§ (π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯)))) β (π:πβΆ(π« π β© Fin) β§ π β (πββͺ ran
π))) |
50 | 49 | ex 414 |
. . 3
β’ (π β ((π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯))) β (π:πβΆ(π« π β© Fin) β§ π β (πββͺ ran
π)))) |
51 | 50 | eximdv 1921 |
. 2
β’ (π β (βπ(π:πβΆ(π« π β© Fin) β§ βπ₯ β π π₯ β (πβ(πβπ₯))) β βπ(π:πβΆ(π« π β© Fin) β§ π β (πββͺ ran
π)))) |
52 | 15, 51 | mpd 15 |
1
β’ (π β βπ(π:πβΆ(π« π β© Fin) β§ π β (πββͺ ran
π))) |