Step | Hyp | Ref
| Expression |
1 | | fin23lem.a |
. . . . . . . 8
β’ π = seqΟ((π β Ο, π’ β V β¦ if(((π‘βπ) β© π’) = β
, π’, ((π‘βπ) β© π’))), βͺ ran π‘) |
2 | | fin23lem17.f |
. . . . . . . 8
β’ πΉ = {π β£ βπ β (π« π βm Ο)(βπ₯ β Ο (πβsuc π₯) β (πβπ₯) β β© ran
π β ran π)} |
3 | | fin23lem.b |
. . . . . . . 8
β’ π = {π£ β Ο β£ β© ran π β (π‘βπ£)} |
4 | | fin23lem.c |
. . . . . . . 8
β’ π = (π€ β Ο β¦ (β©π₯ β π (π₯ β© π) β π€)) |
5 | | fin23lem.d |
. . . . . . . 8
β’ π
= (π€ β Ο β¦ (β©π₯ β (Ο β π)(π₯ β© (Ο β π)) β π€)) |
6 | | fin23lem.e |
. . . . . . . 8
β’ π = if(π β Fin, (π‘ β π
), ((π§ β π β¦ ((π‘βπ§) β β© ran
π)) β π)) |
7 | 1, 2, 3, 4, 5, 6 | fin23lem28 10283 |
. . . . . . 7
β’ (π‘:Οβ1-1βV β π:Οβ1-1βV) |
8 | 7 | ad2antrl 727 |
. . . . . 6
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β π:Οβ1-1βV) |
9 | | simprl 770 |
. . . . . . 7
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β π‘:Οβ1-1βV) |
10 | | simpl 484 |
. . . . . . 7
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β πΊ β πΉ) |
11 | | simprr 772 |
. . . . . . 7
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β βͺ ran
π‘ β πΊ) |
12 | 1, 2, 3, 4, 5, 6 | fin23lem31 10286 |
. . . . . . 7
β’ ((π‘:Οβ1-1βV β§ πΊ β πΉ β§ βͺ ran
π‘ β πΊ) β βͺ ran
π β βͺ ran π‘) |
13 | 9, 10, 11, 12 | syl3anc 1372 |
. . . . . 6
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β βͺ ran
π β βͺ ran π‘) |
14 | | f1fn 6744 |
. . . . . . . . . . . 12
β’ (π‘:Οβ1-1βV β π‘ Fn Ο) |
15 | | dffn3 6686 |
. . . . . . . . . . . 12
β’ (π‘ Fn Ο β π‘:ΟβΆran π‘) |
16 | 14, 15 | sylib 217 |
. . . . . . . . . . 11
β’ (π‘:Οβ1-1βV β π‘:ΟβΆran π‘) |
17 | 16 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β π‘:ΟβΆran π‘) |
18 | | sspwuni 5065 |
. . . . . . . . . . . 12
β’ (ran
π‘ β π« πΊ β βͺ ran π‘ β πΊ) |
19 | 18 | biimpri 227 |
. . . . . . . . . . 11
β’ (βͺ ran π‘ β πΊ β ran π‘ β π« πΊ) |
20 | 19 | ad2antll 728 |
. . . . . . . . . 10
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β ran π‘ β π« πΊ) |
21 | 17, 20 | fssd 6691 |
. . . . . . . . 9
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β π‘:ΟβΆπ« πΊ) |
22 | | pwexg 5338 |
. . . . . . . . . . 11
β’ (πΊ β πΉ β π« πΊ β V) |
23 | 22 | adantr 482 |
. . . . . . . . . 10
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β π« πΊ β V) |
24 | | vex 3452 |
. . . . . . . . . . . 12
β’ π‘ β V |
25 | | f1f 6743 |
. . . . . . . . . . . 12
β’ (π‘:Οβ1-1βV β π‘:ΟβΆV) |
26 | | dmfex 7849 |
. . . . . . . . . . . 12
β’ ((π‘ β V β§ π‘:ΟβΆV) β
Ο β V) |
27 | 24, 25, 26 | sylancr 588 |
. . . . . . . . . . 11
β’ (π‘:Οβ1-1βV β Ο β V) |
28 | 27 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β Ο β V) |
29 | 23, 28 | elmapd 8786 |
. . . . . . . . 9
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β (π‘ β (π« πΊ βm Ο) β π‘:ΟβΆπ« πΊ)) |
30 | 21, 29 | mpbird 257 |
. . . . . . . 8
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β π‘ β (π« πΊ βm
Ο)) |
31 | | f1f 6743 |
. . . . . . . . . 10
β’ (π:Οβ1-1βV β π:ΟβΆV) |
32 | 8, 31 | syl 17 |
. . . . . . . . 9
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β π:ΟβΆV) |
33 | 32, 28 | fexd 7182 |
. . . . . . . 8
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β π β V) |
34 | | eqid 2737 |
. . . . . . . . 9
β’ (π‘ β (π« πΊ βm Ο)
β¦ π) = (π‘ β (π« πΊ βm Ο)
β¦ π) |
35 | 34 | fvmpt2 6964 |
. . . . . . . 8
β’ ((π‘ β (π« πΊ βm Ο)
β§ π β V) β
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) = π) |
36 | 30, 33, 35 | syl2anc 585 |
. . . . . . 7
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β ((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘) = π) |
37 | | f1eq1 6738 |
. . . . . . . 8
β’ (((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) = π β (((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β π:Οβ1-1βV)) |
38 | | rneq 5896 |
. . . . . . . . . 10
β’ (((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) = π β ran ((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘) = ran π) |
39 | 38 | unieqd 4884 |
. . . . . . . . 9
β’ (((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) = π β βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) = βͺ
ran π) |
40 | 39 | psseq1d 4057 |
. . . . . . . 8
β’ (((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) = π β (βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘ β βͺ ran
π β βͺ ran π‘)) |
41 | 37, 40 | anbi12d 632 |
. . . . . . 7
β’ (((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) = π β ((((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘) β (π:Οβ1-1βV β§ βͺ ran π β βͺ ran π‘))) |
42 | 36, 41 | syl 17 |
. . . . . 6
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β ((((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘) β (π:Οβ1-1βV β§ βͺ ran π β βͺ ran π‘))) |
43 | 8, 13, 42 | mpbir2and 712 |
. . . . 5
β’ ((πΊ β πΉ β§ (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ)) β (((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘)) |
44 | 43 | ex 414 |
. . . 4
β’ (πΊ β πΉ β ((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β (((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘))) |
45 | 44 | alrimiv 1931 |
. . 3
β’ (πΊ β πΉ β βπ‘((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β (((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘))) |
46 | | ovex 7395 |
. . . . 5
β’
(π« πΊ
βm Ο) β V |
47 | 46 | mptex 7178 |
. . . 4
β’ (π‘ β (π« πΊ βm Ο)
β¦ π) β
V |
48 | | nfmpt1 5218 |
. . . . . 6
β’
β²π‘(π‘ β (π« πΊ βm Ο) β¦ π) |
49 | 48 | nfeq2 2925 |
. . . . 5
β’
β²π‘ π = (π‘ β (π« πΊ βm Ο) β¦ π) |
50 | | fveq1 6846 |
. . . . . . . 8
β’ (π = (π‘ β (π« πΊ βm Ο) β¦ π) β (πβπ‘) = ((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘)) |
51 | | f1eq1 6738 |
. . . . . . . 8
β’ ((πβπ‘) = ((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘) β ((πβπ‘):Οβ1-1βV β ((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV)) |
52 | 50, 51 | syl 17 |
. . . . . . 7
β’ (π = (π‘ β (π« πΊ βm Ο) β¦ π) β ((πβπ‘):Οβ1-1βV β ((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV)) |
53 | 50 | rneqd 5898 |
. . . . . . . . 9
β’ (π = (π‘ β (π« πΊ βm Ο) β¦ π) β ran (πβπ‘) = ran ((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘)) |
54 | 53 | unieqd 4884 |
. . . . . . . 8
β’ (π = (π‘ β (π« πΊ βm Ο) β¦ π) β βͺ ran (πβπ‘) = βͺ ran ((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘)) |
55 | 54 | psseq1d 4057 |
. . . . . . 7
β’ (π = (π‘ β (π« πΊ βm Ο) β¦ π) β (βͺ ran (πβπ‘) β βͺ ran
π‘ β βͺ ran ((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘) β βͺ ran
π‘)) |
56 | 52, 55 | anbi12d 632 |
. . . . . 6
β’ (π = (π‘ β (π« πΊ βm Ο) β¦ π) β (((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘) β (((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘))) |
57 | 56 | imbi2d 341 |
. . . . 5
β’ (π = (π‘ β (π« πΊ βm Ο) β¦ π) β (((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β ((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘)) β ((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β (((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘)))) |
58 | 49, 57 | albid 2216 |
. . . 4
β’ (π = (π‘ β (π« πΊ βm Ο) β¦ π) β (βπ‘((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β ((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘)) β βπ‘((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β (((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘)))) |
59 | 47, 58 | spcev 3568 |
. . 3
β’
(βπ‘((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β (((π‘ β (π« πΊ βm Ο) β¦ π)βπ‘):Οβ1-1βV β§ βͺ ran
((π‘ β (π« πΊ βm Ο)
β¦ π)βπ‘) β βͺ ran π‘)) β βπβπ‘((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β ((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘))) |
60 | 45, 59 | syl 17 |
. 2
β’ (πΊ β πΉ β βπβπ‘((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β ((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘))) |
61 | | f1eq1 6738 |
. . . . . 6
β’ (π = π‘ β (π:Οβ1-1βV β π‘:Οβ1-1βV)) |
62 | | rneq 5896 |
. . . . . . . 8
β’ (π = π‘ β ran π = ran π‘) |
63 | 62 | unieqd 4884 |
. . . . . . 7
β’ (π = π‘ β βͺ ran
π = βͺ ran π‘) |
64 | 63 | sseq1d 3980 |
. . . . . 6
β’ (π = π‘ β (βͺ ran
π β πΊ β βͺ ran
π‘ β πΊ)) |
65 | 61, 64 | anbi12d 632 |
. . . . 5
β’ (π = π‘ β ((π:Οβ1-1βV β§ βͺ ran π β πΊ) β (π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ))) |
66 | | fveq2 6847 |
. . . . . . 7
β’ (π = π‘ β (πβπ) = (πβπ‘)) |
67 | | f1eq1 6738 |
. . . . . . 7
β’ ((πβπ) = (πβπ‘) β ((πβπ):Οβ1-1βV β (πβπ‘):Οβ1-1βV)) |
68 | 66, 67 | syl 17 |
. . . . . 6
β’ (π = π‘ β ((πβπ):Οβ1-1βV β (πβπ‘):Οβ1-1βV)) |
69 | 66 | rneqd 5898 |
. . . . . . . 8
β’ (π = π‘ β ran (πβπ) = ran (πβπ‘)) |
70 | 69 | unieqd 4884 |
. . . . . . 7
β’ (π = π‘ β βͺ ran
(πβπ) = βͺ ran (πβπ‘)) |
71 | 70, 63 | psseq12d 4059 |
. . . . . 6
β’ (π = π‘ β (βͺ ran
(πβπ) β βͺ ran
π β βͺ ran (πβπ‘) β βͺ ran
π‘)) |
72 | 68, 71 | anbi12d 632 |
. . . . 5
β’ (π = π‘ β (((πβπ):Οβ1-1βV β§ βͺ ran (πβπ) β βͺ ran
π) β ((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘))) |
73 | 65, 72 | imbi12d 345 |
. . . 4
β’ (π = π‘ β (((π:Οβ1-1βV β§ βͺ ran π β πΊ) β ((πβπ):Οβ1-1βV β§ βͺ ran (πβπ) β βͺ ran
π)) β ((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β ((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘)))) |
74 | 73 | cbvalvw 2040 |
. . 3
β’
(βπ((π:Οβ1-1βV β§ βͺ ran π β πΊ) β ((πβπ):Οβ1-1βV β§ βͺ ran (πβπ) β βͺ ran
π)) β βπ‘((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β ((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘))) |
75 | 74 | exbii 1851 |
. 2
β’
(βπβπ((π:Οβ1-1βV β§ βͺ ran π β πΊ) β ((πβπ):Οβ1-1βV β§ βͺ ran (πβπ) β βͺ ran
π)) β βπβπ‘((π‘:Οβ1-1βV β§ βͺ ran π‘ β πΊ) β ((πβπ‘):Οβ1-1βV β§ βͺ ran (πβπ‘) β βͺ ran
π‘))) |
76 | 60, 75 | sylibr 233 |
1
β’ (πΊ β πΉ β βπβπ((π:Οβ1-1βV β§ βͺ ran π β πΊ) β ((πβπ):Οβ1-1βV β§ βͺ ran (πβπ) β βͺ ran
π))) |