Step | Hyp | Ref
| Expression |
1 | | omex 9580 |
. . . 4
β’ Ο
β V |
2 | | limom 7819 |
. . . 4
β’ Lim
Ο |
3 | | r1lim 9709 |
. . . 4
β’ ((Ο
β V β§ Lim Ο) β (π
1βΟ) =
βͺ π β Ο
(π
1βπ)) |
4 | 1, 2, 3 | mp2an 691 |
. . 3
β’
(π
1βΟ) = βͺ π β Ο
(π
1βπ) |
5 | | r1fnon 9704 |
. . . 4
β’
π
1 Fn On |
6 | | fnfun 6603 |
. . . 4
β’
(π
1 Fn On β Fun
π
1) |
7 | | funiunfv 7196 |
. . . 4
β’ (Fun
π
1 β βͺ π β Ο
(π
1βπ) = βͺ
(π
1 β Ο)) |
8 | 5, 6, 7 | mp2b 10 |
. . 3
β’ βͺ π β Ο
(π
1βπ) = βͺ
(π
1 β Ο) |
9 | 4, 8 | eqtri 2765 |
. 2
β’
(π
1βΟ) = βͺ
(π
1 β Ο) |
10 | | iuneq1 4971 |
. . . . . . 7
β’ (π = π β βͺ
π β π ({π} Γ π« π) = βͺ π β π ({π} Γ π« π)) |
11 | | sneq 4597 |
. . . . . . . . 9
β’ (π = π β {π} = {π}) |
12 | | pweq 4575 |
. . . . . . . . 9
β’ (π = π β π« π = π« π) |
13 | 11, 12 | xpeq12d 5665 |
. . . . . . . 8
β’ (π = π β ({π} Γ π« π) = ({π} Γ π« π)) |
14 | 13 | cbviunv 5001 |
. . . . . . 7
β’ βͺ π β π ({π} Γ π« π) = βͺ π β π ({π} Γ π« π) |
15 | 10, 14 | eqtrdi 2793 |
. . . . . 6
β’ (π = π β βͺ
π β π ({π} Γ π« π) = βͺ π β π ({π} Γ π« π)) |
16 | 15 | fveq2d 6847 |
. . . . 5
β’ (π = π β (cardββͺ π β π ({π} Γ π« π)) = (cardββͺ π β π ({π} Γ π« π))) |
17 | 16 | cbvmptv 5219 |
. . . 4
β’ (π β (π« Ο β©
Fin) β¦ (cardββͺ π β π ({π} Γ π« π))) = (π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π))) |
18 | | dmeq 5860 |
. . . . . . . 8
β’ (π = π β dom π = dom π) |
19 | 18 | pweqd 4578 |
. . . . . . 7
β’ (π = π β π« dom π = π« dom π) |
20 | | imaeq1 6009 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
21 | 20 | fveq2d 6847 |
. . . . . . 7
β’ (π = π β ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)) = ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π))) |
22 | 19, 21 | mpteq12dv 5197 |
. . . . . 6
β’ (π = π β (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π))) = (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)))) |
23 | | imaeq2 6010 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
24 | 23 | fveq2d 6847 |
. . . . . . 7
β’ (π = π β ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)) = ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π))) |
25 | 24 | cbvmptv 5219 |
. . . . . 6
β’ (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π))) = (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π))) |
26 | 22, 25 | eqtrdi 2793 |
. . . . 5
β’ (π = π β (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π))) = (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)))) |
27 | 26 | cbvmptv 5219 |
. . . 4
β’ (π β V β¦ (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)))) = (π β V β¦ (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)))) |
28 | | eqid 2737 |
. . . 4
β’ βͺ (rec((π β V β¦ (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)))), β
) β Ο) = βͺ (rec((π β V β¦ (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)))), β
) β
Ο) |
29 | 17, 27, 28 | ackbij2 10180 |
. . 3
β’ βͺ (rec((π β V β¦ (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)))), β
) β Ο):βͺ (π
1 β Ο)β1-1-ontoβΟ |
30 | | fvex 6856 |
. . . . 5
β’
(π
1βΟ) β V |
31 | 9, 30 | eqeltrri 2835 |
. . . 4
β’ βͺ (π
1 β Ο) β
V |
32 | 31 | f1oen 8914 |
. . 3
β’ (βͺ (rec((π β V β¦ (π β π« dom π β¦ ((π β (π« Ο β© Fin) β¦
(cardββͺ π β π ({π} Γ π« π)))β(π β π)))), β
) β Ο):βͺ (π
1 β Ο)β1-1-ontoβΟ β βͺ
(π
1 β Ο) β Ο) |
33 | 29, 32 | ax-mp 5 |
. 2
β’ βͺ (π
1 β Ο) β
Ο |
34 | 9, 33 | eqbrtri 5127 |
1
β’
(π
1βΟ) β Ο |