Step | Hyp | Ref
| Expression |
1 | | dnnumch.f |
. . . . 5
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) |
2 | | dnnumch.a |
. . . . 5
β’ (π β π΄ β π) |
3 | | dnnumch.g |
. . . . 5
β’ (π β βπ¦ β π« π΄(π¦ β β
β (πΊβπ¦) β π¦)) |
4 | 1, 2, 3 | dnnumch3 41403 |
. . . 4
β’ (π β (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1βOn) |
5 | | f1f1orn 6800 |
. . . 4
β’ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1βOn β (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1-ontoβran
(π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1-ontoβran
(π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))) |
7 | | f1f 6743 |
. . . . 5
β’ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1βOn β (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄βΆOn) |
8 | | frn 6680 |
. . . . 5
β’ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄βΆOn β ran (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})) β On) |
9 | 4, 7, 8 | 3syl 18 |
. . . 4
β’ (π β ran (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})) β On) |
10 | | epweon 7714 |
. . . 4
β’ E We
On |
11 | | wess 5625 |
. . . 4
β’ (ran
(π₯ β π΄ β¦ β© (β‘πΉ β {π₯})) β On β ( E We On β E We
ran (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})))) |
12 | 9, 10, 11 | mpisyl 21 |
. . 3
β’ (π β E We ran (π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))) |
13 | | eqid 2737 |
. . . 4
β’
{β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} = {β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} |
14 | 13 | f1owe 7303 |
. . 3
β’ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1-ontoβran
(π₯ β π΄ β¦ β© (β‘πΉ β {π₯})) β ( E We ran (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})) β {β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} We π΄)) |
15 | 6, 12, 14 | sylc 65 |
. 2
β’ (π β {β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} We π΄) |
16 | | fvex 6860 |
. . . . . . . . 9
β’ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) β V |
17 | 16 | epeli 5544 |
. . . . . . . 8
β’ (((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)) |
18 | 1, 2, 3 | dnnumch3lem 41402 |
. . . . . . . . . 10
β’ ((π β§ π£ β π΄) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) = β© (β‘πΉ β {π£})) |
19 | 18 | adantrr 716 |
. . . . . . . . 9
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) = β© (β‘πΉ β {π£})) |
20 | 1, 2, 3 | dnnumch3lem 41402 |
. . . . . . . . . 10
β’ ((π β§ π€ β π΄) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) = β© (β‘πΉ β {π€})) |
21 | 20 | adantrl 715 |
. . . . . . . . 9
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) = β© (β‘πΉ β {π€})) |
22 | 19, 21 | eleq12d 2832 |
. . . . . . . 8
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β (((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) β β© (β‘πΉ β {π£}) β β© (β‘πΉ β {π€}))) |
23 | 17, 22 | bitr2id 284 |
. . . . . . 7
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β (β©
(β‘πΉ β {π£}) β β© (β‘πΉ β {π€}) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€))) |
24 | 23 | pm5.32da 580 |
. . . . . 6
β’ (π β (((π£ β π΄ β§ π€ β π΄) β§ β© (β‘πΉ β {π£}) β β© (β‘πΉ β {π€})) β ((π£ β π΄ β§ π€ β π΄) β§ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)))) |
25 | 24 | opabbidv 5176 |
. . . . 5
β’ (π β {β¨π£, π€β© β£ ((π£ β π΄ β§ π€ β π΄) β§ β© (β‘πΉ β {π£}) β β© (β‘πΉ β {π€}))} = {β¨π£, π€β© β£ ((π£ β π΄ β§ π€ β π΄) β§ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€))}) |
26 | | incom 4166 |
. . . . . 6
β’ (π» β© (π΄ Γ π΄)) = ((π΄ Γ π΄) β© π») |
27 | | df-xp 5644 |
. . . . . . 7
β’ (π΄ Γ π΄) = {β¨π£, π€β© β£ (π£ β π΄ β§ π€ β π΄)} |
28 | | dnwech.h |
. . . . . . 7
β’ π» = {β¨π£, π€β© β£ β©
(β‘πΉ β {π£}) β β© (β‘πΉ β {π€})} |
29 | 27, 28 | ineq12i 4175 |
. . . . . 6
β’ ((π΄ Γ π΄) β© π») = ({β¨π£, π€β© β£ (π£ β π΄ β§ π€ β π΄)} β© {β¨π£, π€β© β£ β©
(β‘πΉ β {π£}) β β© (β‘πΉ β {π€})}) |
30 | | inopab 5790 |
. . . . . 6
β’
({β¨π£, π€β© β£ (π£ β π΄ β§ π€ β π΄)} β© {β¨π£, π€β© β£ β©
(β‘πΉ β {π£}) β β© (β‘πΉ β {π€})}) = {β¨π£, π€β© β£ ((π£ β π΄ β§ π€ β π΄) β§ β© (β‘πΉ β {π£}) β β© (β‘πΉ β {π€}))} |
31 | 26, 29, 30 | 3eqtri 2769 |
. . . . 5
β’ (π» β© (π΄ Γ π΄)) = {β¨π£, π€β© β£ ((π£ β π΄ β§ π€ β π΄) β§ β© (β‘πΉ β {π£}) β β© (β‘πΉ β {π€}))} |
32 | | incom 4166 |
. . . . . 6
β’
({β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} β© (π΄ Γ π΄)) = ((π΄ Γ π΄) β© {β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)}) |
33 | 27 | ineq1i 4173 |
. . . . . 6
β’ ((π΄ Γ π΄) β© {β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)}) = ({β¨π£, π€β© β£ (π£ β π΄ β§ π€ β π΄)} β© {β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)}) |
34 | | inopab 5790 |
. . . . . 6
β’
({β¨π£, π€β© β£ (π£ β π΄ β§ π€ β π΄)} β© {β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)}) = {β¨π£, π€β© β£ ((π£ β π΄ β§ π€ β π΄) β§ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€))} |
35 | 32, 33, 34 | 3eqtri 2769 |
. . . . 5
β’
({β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} β© (π΄ Γ π΄)) = {β¨π£, π€β© β£ ((π£ β π΄ β§ π€ β π΄) β§ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€))} |
36 | 25, 31, 35 | 3eqtr4g 2802 |
. . . 4
β’ (π β (π» β© (π΄ Γ π΄)) = ({β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} β© (π΄ Γ π΄))) |
37 | | weeq1 5626 |
. . . 4
β’ ((π» β© (π΄ Γ π΄)) = ({β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} β© (π΄ Γ π΄)) β ((π» β© (π΄ Γ π΄)) We π΄ β ({β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} β© (π΄ Γ π΄)) We π΄)) |
38 | 36, 37 | syl 17 |
. . 3
β’ (π β ((π» β© (π΄ Γ π΄)) We π΄ β ({β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} β© (π΄ Γ π΄)) We π΄)) |
39 | | weinxp 5721 |
. . 3
β’ (π» We π΄ β (π» β© (π΄ Γ π΄)) We π΄) |
40 | | weinxp 5721 |
. . 3
β’
({β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} We π΄ β ({β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} β© (π΄ Γ π΄)) We π΄) |
41 | 38, 39, 40 | 3bitr4g 314 |
. 2
β’ (π β (π» We π΄ β {β¨π£, π€β© β£ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) E ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€)} We π΄)) |
42 | 15, 41 | mpbird 257 |
1
β’ (π β π» We π΄) |