Step | Hyp | Ref
| Expression |
1 | | oveq1 7368 |
. . 3
β’ (π = π β (ππΉπ ) = (ππΉπ )) |
2 | | 2fveq3 6851 |
. . 3
β’ (π = π β (π»β(cardβπ)) = (π»β(cardβπ))) |
3 | 1, 2 | eqeq12d 2749 |
. 2
β’ (π = π β ((ππΉπ ) = (π»β(cardβπ)) β (ππΉπ ) = (π»β(cardβπ)))) |
4 | | oveq2 7369 |
. . 3
β’ (π = π
β (ππΉπ ) = (ππΉπ
)) |
5 | 4 | eqeq1d 2735 |
. 2
β’ (π = π
β ((ππΉπ ) = (π»β(cardβπ)) β (ππΉπ
) = (π»β(cardβπ)))) |
6 | | nfcv 2904 |
. . 3
β’
β²π₯π |
7 | | nfcv 2904 |
. . 3
β’
β²ππ |
8 | | nfcv 2904 |
. . 3
β’
β²ππ |
9 | | pwfseqlem4.f |
. . . . . 6
β’ πΉ = (π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
10 | | nfmpo1 7441 |
. . . . . 6
β’
β²π₯(π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
11 | 9, 10 | nfcxfr 2902 |
. . . . 5
β’
β²π₯πΉ |
12 | | nfcv 2904 |
. . . . 5
β’
β²π₯π |
13 | 6, 11, 12 | nfov 7391 |
. . . 4
β’
β²π₯(ππΉπ) |
14 | 13 | nfeq1 2919 |
. . 3
β’
β²π₯(ππΉπ) = (π»β(cardβπ)) |
15 | | nfmpo2 7442 |
. . . . . 6
β’
β²π(π₯ β V, π β V β¦ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
16 | 9, 15 | nfcxfr 2902 |
. . . . 5
β’
β²ππΉ |
17 | 7, 16, 8 | nfov 7391 |
. . . 4
β’
β²π(ππΉπ ) |
18 | 17 | nfeq1 2919 |
. . 3
β’
β²π(ππΉπ ) = (π»β(cardβπ)) |
19 | | oveq1 7368 |
. . . 4
β’ (π₯ = π β (π₯πΉπ) = (ππΉπ)) |
20 | | 2fveq3 6851 |
. . . 4
β’ (π₯ = π β (π»β(cardβπ₯)) = (π»β(cardβπ))) |
21 | 19, 20 | eqeq12d 2749 |
. . 3
β’ (π₯ = π β ((π₯πΉπ) = (π»β(cardβπ₯)) β (ππΉπ) = (π»β(cardβπ)))) |
22 | | oveq2 7369 |
. . . 4
β’ (π = π β (ππΉπ) = (ππΉπ )) |
23 | 22 | eqeq1d 2735 |
. . 3
β’ (π = π β ((ππΉπ) = (π»β(cardβπ)) β (ππΉπ ) = (π»β(cardβπ)))) |
24 | | vex 3451 |
. . . . . 6
β’ π₯ β V |
25 | | vex 3451 |
. . . . . 6
β’ π β V |
26 | | fvex 6859 |
. . . . . . 7
β’ (π»β(cardβπ₯)) β V |
27 | | fvex 6859 |
. . . . . . 7
β’ (π·ββ© {π§
β Ο β£ Β¬ (π·βπ§) β π₯}) β V |
28 | 26, 27 | ifex 4540 |
. . . . . 6
β’ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) β V |
29 | 9 | ovmpt4g 7506 |
. . . . . 6
β’ ((π₯ β V β§ π β V β§ if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) β V) β (π₯πΉπ) = if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯}))) |
30 | 24, 25, 28, 29 | mp3an 1462 |
. . . . 5
β’ (π₯πΉπ) = if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) |
31 | | iftrue 4496 |
. . . . 5
β’ (π₯ β Fin β if(π₯ β Fin, (π»β(cardβπ₯)), (π·ββ© {π§ β Ο β£ Β¬
(π·βπ§) β π₯})) = (π»β(cardβπ₯))) |
32 | 30, 31 | eqtrid 2785 |
. . . 4
β’ (π₯ β Fin β (π₯πΉπ) = (π»β(cardβπ₯))) |
33 | 32 | adantr 482 |
. . 3
β’ ((π₯ β Fin β§ π β π) β (π₯πΉπ) = (π»β(cardβπ₯))) |
34 | 6, 7, 8, 14, 18, 21, 23, 33 | vtocl2gaf 3538 |
. 2
β’ ((π β Fin β§ π β π) β (ππΉπ ) = (π»β(cardβπ))) |
35 | 3, 5, 34 | vtocl2ga 3537 |
1
β’ ((π β Fin β§ π
β π) β (ππΉπ
) = (π»β(cardβπ))) |