Step | Hyp | Ref
| Expression |
1 | | eleq1 2240 |
. . . . 5
β’ (π₯ = π§ β (π₯ β π΄ β π§ β π΄)) |
2 | 1 | dcbid 838 |
. . . 4
β’ (π₯ = π§ β (DECID π₯ β π΄ β DECID π§ β π΄)) |
3 | 2 | cbvralv 2704 |
. . 3
β’
(βπ₯ β
β DECID π₯ β π΄ β βπ§ β β DECID π§ β π΄) |
4 | | imassrn 4982 |
. . . . 5
β’ (β‘πΊ β π΄) β ran β‘πΊ |
5 | | 1z 9279 |
. . . . . . . . . 10
β’ 1 β
β€ |
6 | | id 19 |
. . . . . . . . . . 11
β’ (1 β
β€ β 1 β β€) |
7 | | ssnnctlem.g |
. . . . . . . . . . 11
β’ πΊ = frec((π₯ β β€ β¦ (π₯ + 1)), 1) |
8 | 6, 7 | frec2uzf1od 10406 |
. . . . . . . . . 10
β’ (1 β
β€ β πΊ:Οβ1-1-ontoβ(β€β₯β1)) |
9 | 5, 8 | ax-mp 5 |
. . . . . . . . 9
β’ πΊ:Οβ1-1-ontoβ(β€β₯β1) |
10 | | nnuz 9563 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
11 | | f1oeq3 5452 |
. . . . . . . . . 10
β’ (β
= (β€β₯β1) β (πΊ:Οβ1-1-ontoββ β πΊ:Οβ1-1-ontoβ(β€β₯β1))) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
β’ (πΊ:Οβ1-1-ontoββ β πΊ:Οβ1-1-ontoβ(β€β₯β1)) |
13 | 9, 12 | mpbir 146 |
. . . . . . . 8
β’ πΊ:Οβ1-1-ontoββ |
14 | | f1ocnv 5475 |
. . . . . . . 8
β’ (πΊ:Οβ1-1-ontoββ β β‘πΊ:ββ1-1-ontoβΟ) |
15 | 13, 14 | ax-mp 5 |
. . . . . . 7
β’ β‘πΊ:ββ1-1-ontoβΟ |
16 | | dff1o5 5471 |
. . . . . . 7
β’ (β‘πΊ:ββ1-1-ontoβΟ β (β‘πΊ:ββ1-1βΟ β§ ran β‘πΊ = Ο)) |
17 | 15, 16 | mpbi 145 |
. . . . . 6
β’ (β‘πΊ:ββ1-1βΟ β§ ran β‘πΊ = Ο) |
18 | 17 | simpri 113 |
. . . . 5
β’ ran β‘πΊ = Ο |
19 | 4, 18 | sseqtri 3190 |
. . . 4
β’ (β‘πΊ β π΄) β Ο |
20 | | eleq1 2240 |
. . . . . . . 8
β’ (π§ = (πΊβπ¦) β (π§ β π΄ β (πΊβπ¦) β π΄)) |
21 | 20 | dcbid 838 |
. . . . . . 7
β’ (π§ = (πΊβπ¦) β (DECID π§ β π΄ β DECID (πΊβπ¦) β π΄)) |
22 | | simplr 528 |
. . . . . . 7
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β
βπ§ β β
DECID π§
β π΄) |
23 | | f1of 5462 |
. . . . . . . . 9
β’ (πΊ:Οβ1-1-ontoββ β πΊ:ΟβΆβ) |
24 | 13, 23 | mp1i 10 |
. . . . . . . 8
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β πΊ:ΟβΆβ) |
25 | | simpr 110 |
. . . . . . . 8
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β π¦ β
Ο) |
26 | 24, 25 | ffvelcdmd 5653 |
. . . . . . 7
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β (πΊβπ¦) β β) |
27 | 21, 22, 26 | rspcdva 2847 |
. . . . . 6
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β
DECID (πΊβπ¦) β π΄) |
28 | | f1of1 5461 |
. . . . . . . . . 10
β’ (β‘πΊ:ββ1-1-ontoβΟ β β‘πΊ:ββ1-1βΟ) |
29 | 15, 28 | ax-mp 5 |
. . . . . . . . 9
β’ β‘πΊ:ββ1-1βΟ |
30 | | simpll 527 |
. . . . . . . . 9
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β π΄ β
β) |
31 | | f1elima 5774 |
. . . . . . . . 9
β’ ((β‘πΊ:ββ1-1βΟ β§ (πΊβπ¦) β β β§ π΄ β β) β ((β‘πΊβ(πΊβπ¦)) β (β‘πΊ β π΄) β (πΊβπ¦) β π΄)) |
32 | 29, 26, 30, 31 | mp3an2i 1342 |
. . . . . . . 8
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β ((β‘πΊβ(πΊβπ¦)) β (β‘πΊ β π΄) β (πΊβπ¦) β π΄)) |
33 | | f1ocnvfv1 5778 |
. . . . . . . . . . 11
β’ ((πΊ:Οβ1-1-ontoββ β§ π¦ β Ο) β (β‘πΊβ(πΊβπ¦)) = π¦) |
34 | 13, 33 | mpan 424 |
. . . . . . . . . 10
β’ (π¦ β Ο β (β‘πΊβ(πΊβπ¦)) = π¦) |
35 | 34 | adantl 277 |
. . . . . . . . 9
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β (β‘πΊβ(πΊβπ¦)) = π¦) |
36 | 35 | eleq1d 2246 |
. . . . . . . 8
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β ((β‘πΊβ(πΊβπ¦)) β (β‘πΊ β π΄) β π¦ β (β‘πΊ β π΄))) |
37 | 32, 36 | bitr3d 190 |
. . . . . . 7
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β ((πΊβπ¦) β π΄ β π¦ β (β‘πΊ β π΄))) |
38 | 37 | dcbid 838 |
. . . . . 6
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β
(DECID (πΊβπ¦) β π΄ β DECID π¦ β (β‘πΊ β π΄))) |
39 | 27, 38 | mpbid 147 |
. . . . 5
β’ (((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β§ π¦ β Ο) β
DECID π¦
β (β‘πΊ β π΄)) |
40 | 39 | ralrimiva 2550 |
. . . 4
β’ ((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β
βπ¦ β Ο
DECID π¦
β (β‘πΊ β π΄)) |
41 | | ssomct 12446 |
. . . 4
β’ (((β‘πΊ β π΄) β Ο β§ βπ¦ β Ο
DECID π¦
β (β‘πΊ β π΄)) β βπ π:Οβontoβ((β‘πΊ β π΄) β 1o)) |
42 | 19, 40, 41 | sylancr 414 |
. . 3
β’ ((π΄ β β β§
βπ§ β β
DECID π§
β π΄) β
βπ π:Οβontoβ((β‘πΊ β π΄) β 1o)) |
43 | 3, 42 | sylan2b 287 |
. 2
β’ ((π΄ β β β§
βπ₯ β β
DECID π₯
β π΄) β
βπ π:Οβontoβ((β‘πΊ β π΄) β 1o)) |
44 | | nnex 8925 |
. . . . . 6
β’ β
β V |
45 | 44 | ssex 4141 |
. . . . 5
β’ (π΄ β β β π΄ β V) |
46 | | f1ores 5477 |
. . . . . 6
β’ ((β‘πΊ:ββ1-1βΟ β§ π΄ β β) β (β‘πΊ βΎ π΄):π΄β1-1-ontoβ(β‘πΊ β π΄)) |
47 | 29, 46 | mpan 424 |
. . . . 5
β’ (π΄ β β β (β‘πΊ βΎ π΄):π΄β1-1-ontoβ(β‘πΊ β π΄)) |
48 | | f1oeng 6757 |
. . . . 5
β’ ((π΄ β V β§ (β‘πΊ βΎ π΄):π΄β1-1-ontoβ(β‘πΊ β π΄)) β π΄ β (β‘πΊ β π΄)) |
49 | 45, 47, 48 | syl2anc 411 |
. . . 4
β’ (π΄ β β β π΄ β (β‘πΊ β π΄)) |
50 | | enct 12434 |
. . . 4
β’ (π΄ β (β‘πΊ β π΄) β (βπ π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβ((β‘πΊ β π΄) β 1o))) |
51 | 49, 50 | syl 14 |
. . 3
β’ (π΄ β β β
(βπ π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβ((β‘πΊ β π΄) β 1o))) |
52 | 51 | adantr 276 |
. 2
β’ ((π΄ β β β§
βπ₯ β β
DECID π₯
β π΄) β
(βπ π:Οβontoβ(π΄ β 1o) β βπ π:Οβontoβ((β‘πΊ β π΄) β 1o))) |
53 | 43, 52 | mpbird 167 |
1
β’ ((π΄ β β β§
βπ₯ β β
DECID π₯
β π΄) β
βπ π:Οβontoβ(π΄ β 1o)) |