Step | Hyp | Ref
| Expression |
1 | | cnvimass 6038 |
. . . . 5
β’ (β‘πΉ β {π₯}) β dom πΉ |
2 | | dnnumch.f |
. . . . . . 7
β’ πΉ = recs((π§ β V β¦ (πΊβ(π΄ β ran π§)))) |
3 | 2 | tfr1 8348 |
. . . . . 6
β’ πΉ Fn On |
4 | 3 | fndmi 6611 |
. . . . 5
β’ dom πΉ = On |
5 | 1, 4 | sseqtri 3985 |
. . . 4
β’ (β‘πΉ β {π₯}) β On |
6 | | dnnumch.a |
. . . . . . 7
β’ (π β π΄ β π) |
7 | | dnnumch.g |
. . . . . . 7
β’ (π β βπ¦ β π« π΄(π¦ β β
β (πΊβπ¦) β π¦)) |
8 | 2, 6, 7 | dnnumch2 41401 |
. . . . . 6
β’ (π β π΄ β ran πΉ) |
9 | 8 | sselda 3949 |
. . . . 5
β’ ((π β§ π₯ β π΄) β π₯ β ran πΉ) |
10 | | inisegn0 6055 |
. . . . 5
β’ (π₯ β ran πΉ β (β‘πΉ β {π₯}) β β
) |
11 | 9, 10 | sylib 217 |
. . . 4
β’ ((π β§ π₯ β π΄) β (β‘πΉ β {π₯}) β β
) |
12 | | oninton 7735 |
. . . 4
β’ (((β‘πΉ β {π₯}) β On β§ (β‘πΉ β {π₯}) β β
) β β© (β‘πΉ β {π₯}) β On) |
13 | 5, 11, 12 | sylancr 588 |
. . 3
β’ ((π β§ π₯ β π΄) β β© (β‘πΉ β {π₯}) β On) |
14 | 13 | fmpttd 7068 |
. 2
β’ (π β (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄βΆOn) |
15 | 2, 6, 7 | dnnumch3lem 41402 |
. . . . . 6
β’ ((π β§ π£ β π΄) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) = β© (β‘πΉ β {π£})) |
16 | 15 | adantrr 716 |
. . . . 5
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) = β© (β‘πΉ β {π£})) |
17 | 2, 6, 7 | dnnumch3lem 41402 |
. . . . . 6
β’ ((π β§ π€ β π΄) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) = β© (β‘πΉ β {π€})) |
18 | 17 | adantrl 715 |
. . . . 5
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) = β© (β‘πΉ β {π€})) |
19 | 16, 18 | eqeq12d 2753 |
. . . 4
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β (((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) = ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) β β© (β‘πΉ β {π£}) = β© (β‘πΉ β {π€}))) |
20 | | fveq2 6847 |
. . . . . . 7
β’ (β© (β‘πΉ β {π£}) = β© (β‘πΉ β {π€}) β (πΉββ© (β‘πΉ β {π£})) = (πΉββ© (β‘πΉ β {π€}))) |
21 | 20 | adantl 483 |
. . . . . 6
β’ (((π β§ (π£ β π΄ β§ π€ β π΄)) β§ β© (β‘πΉ β {π£}) = β© (β‘πΉ β {π€})) β (πΉββ© (β‘πΉ β {π£})) = (πΉββ© (β‘πΉ β {π€}))) |
22 | | cnvimass 6038 |
. . . . . . . . . . 11
β’ (β‘πΉ β {π£}) β dom πΉ |
23 | 22, 4 | sseqtri 3985 |
. . . . . . . . . 10
β’ (β‘πΉ β {π£}) β On |
24 | 8 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β§ π£ β π΄) β π£ β ran πΉ) |
25 | | inisegn0 6055 |
. . . . . . . . . . 11
β’ (π£ β ran πΉ β (β‘πΉ β {π£}) β β
) |
26 | 24, 25 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π£ β π΄) β (β‘πΉ β {π£}) β β
) |
27 | | onint 7730 |
. . . . . . . . . 10
β’ (((β‘πΉ β {π£}) β On β§ (β‘πΉ β {π£}) β β
) β β© (β‘πΉ β {π£}) β (β‘πΉ β {π£})) |
28 | 23, 26, 27 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ π£ β π΄) β β© (β‘πΉ β {π£}) β (β‘πΉ β {π£})) |
29 | | fniniseg 7015 |
. . . . . . . . . . 11
β’ (πΉ Fn On β (β© (β‘πΉ β {π£}) β (β‘πΉ β {π£}) β (β©
(β‘πΉ β {π£}) β On β§ (πΉββ© (β‘πΉ β {π£})) = π£))) |
30 | 3, 29 | ax-mp 5 |
. . . . . . . . . 10
β’ (β© (β‘πΉ β {π£}) β (β‘πΉ β {π£}) β (β©
(β‘πΉ β {π£}) β On β§ (πΉββ© (β‘πΉ β {π£})) = π£)) |
31 | 30 | simprbi 498 |
. . . . . . . . 9
β’ (β© (β‘πΉ β {π£}) β (β‘πΉ β {π£}) β (πΉββ© (β‘πΉ β {π£})) = π£) |
32 | 28, 31 | syl 17 |
. . . . . . . 8
β’ ((π β§ π£ β π΄) β (πΉββ© (β‘πΉ β {π£})) = π£) |
33 | 32 | adantrr 716 |
. . . . . . 7
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β (πΉββ© (β‘πΉ β {π£})) = π£) |
34 | 33 | adantr 482 |
. . . . . 6
β’ (((π β§ (π£ β π΄ β§ π€ β π΄)) β§ β© (β‘πΉ β {π£}) = β© (β‘πΉ β {π€})) β (πΉββ© (β‘πΉ β {π£})) = π£) |
35 | | cnvimass 6038 |
. . . . . . . . . . 11
β’ (β‘πΉ β {π€}) β dom πΉ |
36 | 35, 4 | sseqtri 3985 |
. . . . . . . . . 10
β’ (β‘πΉ β {π€}) β On |
37 | 8 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β§ π€ β π΄) β π€ β ran πΉ) |
38 | | inisegn0 6055 |
. . . . . . . . . . 11
β’ (π€ β ran πΉ β (β‘πΉ β {π€}) β β
) |
39 | 37, 38 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π€ β π΄) β (β‘πΉ β {π€}) β β
) |
40 | | onint 7730 |
. . . . . . . . . 10
β’ (((β‘πΉ β {π€}) β On β§ (β‘πΉ β {π€}) β β
) β β© (β‘πΉ β {π€}) β (β‘πΉ β {π€})) |
41 | 36, 39, 40 | sylancr 588 |
. . . . . . . . 9
β’ ((π β§ π€ β π΄) β β© (β‘πΉ β {π€}) β (β‘πΉ β {π€})) |
42 | | fniniseg 7015 |
. . . . . . . . . . 11
β’ (πΉ Fn On β (β© (β‘πΉ β {π€}) β (β‘πΉ β {π€}) β (β©
(β‘πΉ β {π€}) β On β§ (πΉββ© (β‘πΉ β {π€})) = π€))) |
43 | 3, 42 | ax-mp 5 |
. . . . . . . . . 10
β’ (β© (β‘πΉ β {π€}) β (β‘πΉ β {π€}) β (β©
(β‘πΉ β {π€}) β On β§ (πΉββ© (β‘πΉ β {π€})) = π€)) |
44 | 43 | simprbi 498 |
. . . . . . . . 9
β’ (β© (β‘πΉ β {π€}) β (β‘πΉ β {π€}) β (πΉββ© (β‘πΉ β {π€})) = π€) |
45 | 41, 44 | syl 17 |
. . . . . . . 8
β’ ((π β§ π€ β π΄) β (πΉββ© (β‘πΉ β {π€})) = π€) |
46 | 45 | adantrl 715 |
. . . . . . 7
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β (πΉββ© (β‘πΉ β {π€})) = π€) |
47 | 46 | adantr 482 |
. . . . . 6
β’ (((π β§ (π£ β π΄ β§ π€ β π΄)) β§ β© (β‘πΉ β {π£}) = β© (β‘πΉ β {π€})) β (πΉββ© (β‘πΉ β {π€})) = π€) |
48 | 21, 34, 47 | 3eqtr3d 2785 |
. . . . 5
β’ (((π β§ (π£ β π΄ β§ π€ β π΄)) β§ β© (β‘πΉ β {π£}) = β© (β‘πΉ β {π€})) β π£ = π€) |
49 | 48 | ex 414 |
. . . 4
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β (β©
(β‘πΉ β {π£}) = β© (β‘πΉ β {π€}) β π£ = π€)) |
50 | 19, 49 | sylbid 239 |
. . 3
β’ ((π β§ (π£ β π΄ β§ π€ β π΄)) β (((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) = ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) β π£ = π€)) |
51 | 50 | ralrimivva 3198 |
. 2
β’ (π β βπ£ β π΄ βπ€ β π΄ (((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) = ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) β π£ = π€)) |
52 | | dff13 7207 |
. 2
β’ ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1βOn β ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄βΆOn β§ βπ£ β π΄ βπ€ β π΄ (((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ£) = ((π₯ β π΄ β¦ β© (β‘πΉ β {π₯}))βπ€) β π£ = π€))) |
53 | 14, 51, 52 | sylanbrc 584 |
1
β’ (π β (π₯ β π΄ β¦ β© (β‘πΉ β {π₯})):π΄β1-1βOn) |