Step | Hyp | Ref
| Expression |
1 | | nn0ennn 10433 |
. . . 4
β’
β0 β β |
2 | 1 | ensymi 6782 |
. . 3
β’ β
β β0 |
3 | | entr 6784 |
. . 3
β’ ((π΄ β β β§ β
β β0) β π΄ β
β0) |
4 | 2, 3 | mpan2 425 |
. 2
β’ (π΄ β β β π΄ β
β0) |
5 | | bren 6747 |
. . . 4
β’ (π΄ β β0
β βπ π:π΄β1-1-ontoββ0) |
6 | 5 | biimpi 120 |
. . 3
β’ (π΄ β β0
β βπ π:π΄β1-1-ontoββ0) |
7 | | f1of 5462 |
. . . . . . . . . . 11
β’ (π:π΄β1-1-ontoββ0 β π:π΄βΆβ0) |
8 | 7 | adantr 276 |
. . . . . . . . . 10
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β π:π΄βΆβ0) |
9 | | simprl 529 |
. . . . . . . . . 10
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β π₯ β π΄) |
10 | 8, 9 | ffvelcdmd 5653 |
. . . . . . . . 9
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β (πβπ₯) β
β0) |
11 | 10 | nn0zd 9373 |
. . . . . . . 8
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β (πβπ₯) β β€) |
12 | | simprr 531 |
. . . . . . . . . 10
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β π¦ β π΄) |
13 | 8, 12 | ffvelcdmd 5653 |
. . . . . . . . 9
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β (πβπ¦) β
β0) |
14 | 13 | nn0zd 9373 |
. . . . . . . 8
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β (πβπ¦) β β€) |
15 | | zdceq 9328 |
. . . . . . . 8
β’ (((πβπ₯) β β€ β§ (πβπ¦) β β€) β DECID
(πβπ₯) = (πβπ¦)) |
16 | 11, 14, 15 | syl2anc 411 |
. . . . . . 7
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β DECID (πβπ₯) = (πβπ¦)) |
17 | | dff1o6 5777 |
. . . . . . . . . . . . 13
β’ (π:π΄β1-1-ontoββ0 β (π Fn π΄ β§ ran π = β0 β§ βπ₯ β π΄ βπ¦ β π΄ ((πβπ₯) = (πβπ¦) β π₯ = π¦))) |
18 | 17 | simp3bi 1014 |
. . . . . . . . . . . 12
β’ (π:π΄β1-1-ontoββ0 β βπ₯ β π΄ βπ¦ β π΄ ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
19 | 18 | r19.21bi 2565 |
. . . . . . . . . . 11
β’ ((π:π΄β1-1-ontoββ0 β§ π₯ β π΄) β βπ¦ β π΄ ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
20 | 19 | r19.21bi 2565 |
. . . . . . . . . 10
β’ (((π:π΄β1-1-ontoββ0 β§ π₯ β π΄) β§ π¦ β π΄) β ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
21 | 20 | anasss 399 |
. . . . . . . . 9
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
22 | | fveq2 5516 |
. . . . . . . . 9
β’ (π₯ = π¦ β (πβπ₯) = (πβπ¦)) |
23 | 21, 22 | impbid1 142 |
. . . . . . . 8
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
24 | 23 | dcbid 838 |
. . . . . . 7
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β (DECID (πβπ₯) = (πβπ¦) β DECID π₯ = π¦)) |
25 | 16, 24 | mpbid 147 |
. . . . . 6
β’ ((π:π΄β1-1-ontoββ0 β§ (π₯ β π΄ β§ π¦ β π΄)) β DECID π₯ = π¦) |
26 | 25 | ralrimivva 2559 |
. . . . 5
β’ (π:π΄β1-1-ontoββ0 β βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦) |
27 | | f1ocnv 5475 |
. . . . . . 7
β’ (π:π΄β1-1-ontoββ0 β β‘π:β0β1-1-ontoβπ΄) |
28 | | f1ofo 5469 |
. . . . . . 7
β’ (β‘π:β0β1-1-ontoβπ΄ β β‘π:β0βontoβπ΄) |
29 | 27, 28 | syl 14 |
. . . . . 6
β’ (π:π΄β1-1-ontoββ0 β β‘π:β0βontoβπ΄) |
30 | | peano2nn0 9216 |
. . . . . . . . 9
β’ (π β β0
β (π + 1) β
β0) |
31 | 30 | adantl 277 |
. . . . . . . 8
β’ ((π:π΄β1-1-ontoββ0 β§ π β β0) β (π + 1) β
β0) |
32 | | elfznn0 10114 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β π β β0) |
33 | 32 | adantl 277 |
. . . . . . . . . . . . . 14
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β π β β0) |
34 | 33 | nn0red 9230 |
. . . . . . . . . . . . 13
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β π β β) |
35 | | elfzle2 10028 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β π β€ π) |
36 | 35 | adantl 277 |
. . . . . . . . . . . . . 14
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β π β€ π) |
37 | | simplr 528 |
. . . . . . . . . . . . . . 15
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β π β β0) |
38 | | nn0leltp1 9316 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π β
β0) β (π β€ π β π < (π + 1))) |
39 | 33, 37, 38 | syl2anc 411 |
. . . . . . . . . . . . . 14
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β (π β€ π β π < (π + 1))) |
40 | 36, 39 | mpbid 147 |
. . . . . . . . . . . . 13
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β π < (π + 1)) |
41 | 34, 40 | gtned 8070 |
. . . . . . . . . . . 12
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β (π + 1) β π) |
42 | 41 | neneqd 2368 |
. . . . . . . . . . 11
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β Β¬ (π + 1) = π) |
43 | | dff1o6 5777 |
. . . . . . . . . . . . . . 15
β’ (β‘π:β0β1-1-ontoβπ΄ β (β‘π Fn β0 β§ ran β‘π = π΄ β§ βπ₯ β β0 βπ¦ β β0
((β‘πβπ₯) = (β‘πβπ¦) β π₯ = π¦))) |
44 | 27, 43 | sylib 122 |
. . . . . . . . . . . . . 14
β’ (π:π΄β1-1-ontoββ0 β (β‘π Fn β0 β§ ran β‘π = π΄ β§ βπ₯ β β0 βπ¦ β β0
((β‘πβπ₯) = (β‘πβπ¦) β π₯ = π¦))) |
45 | 44 | simp3d 1011 |
. . . . . . . . . . . . 13
β’ (π:π΄β1-1-ontoββ0 β βπ₯ β β0
βπ¦ β
β0 ((β‘πβπ₯) = (β‘πβπ¦) β π₯ = π¦)) |
46 | 45 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β βπ₯ β β0 βπ¦ β β0
((β‘πβπ₯) = (β‘πβπ¦) β π₯ = π¦)) |
47 | 31 | adantr 276 |
. . . . . . . . . . . . 13
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β (π + 1) β
β0) |
48 | | fveqeq2 5525 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π + 1) β ((β‘πβπ₯) = (β‘πβπ¦) β (β‘πβ(π + 1)) = (β‘πβπ¦))) |
49 | | eqeq1 2184 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (π + 1) β (π₯ = π¦ β (π + 1) = π¦)) |
50 | 48, 49 | imbi12d 234 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π + 1) β (((β‘πβπ₯) = (β‘πβπ¦) β π₯ = π¦) β ((β‘πβ(π + 1)) = (β‘πβπ¦) β (π + 1) = π¦))) |
51 | | fveq2 5516 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (β‘πβπ¦) = (β‘πβπ)) |
52 | 51 | eqeq2d 2189 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((β‘πβ(π + 1)) = (β‘πβπ¦) β (β‘πβ(π + 1)) = (β‘πβπ))) |
53 | | eqeq2 2187 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((π + 1) = π¦ β (π + 1) = π)) |
54 | 52, 53 | imbi12d 234 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β (((β‘πβ(π + 1)) = (β‘πβπ¦) β (π + 1) = π¦) β ((β‘πβ(π + 1)) = (β‘πβπ) β (π + 1) = π))) |
55 | 50, 54 | rspc2v 2855 |
. . . . . . . . . . . . 13
β’ (((π + 1) β β0
β§ π β
β0) β (βπ₯ β β0 βπ¦ β β0
((β‘πβπ₯) = (β‘πβπ¦) β π₯ = π¦) β ((β‘πβ(π + 1)) = (β‘πβπ) β (π + 1) = π))) |
56 | 47, 33, 55 | syl2anc 411 |
. . . . . . . . . . . 12
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β (βπ₯ β β0 βπ¦ β β0
((β‘πβπ₯) = (β‘πβπ¦) β π₯ = π¦) β ((β‘πβ(π + 1)) = (β‘πβπ) β (π + 1) = π))) |
57 | 46, 56 | mpd 13 |
. . . . . . . . . . 11
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β ((β‘πβ(π + 1)) = (β‘πβπ) β (π + 1) = π)) |
58 | 42, 57 | mtod 663 |
. . . . . . . . . 10
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β Β¬ (β‘πβ(π + 1)) = (β‘πβπ)) |
59 | 58 | neqned 2354 |
. . . . . . . . 9
β’ (((π:π΄β1-1-ontoββ0 β§ π β β0) β§ π β (0...π)) β (β‘πβ(π + 1)) β (β‘πβπ)) |
60 | 59 | ralrimiva 2550 |
. . . . . . . 8
β’ ((π:π΄β1-1-ontoββ0 β§ π β β0) β
βπ β (0...π)(β‘πβ(π + 1)) β (β‘πβπ)) |
61 | | fveq2 5516 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (β‘πβπ) = (β‘πβ(π + 1))) |
62 | 61 | neeq1d 2365 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((β‘πβπ) β (β‘πβπ) β (β‘πβ(π + 1)) β (β‘πβπ))) |
63 | 62 | ralbidv 2477 |
. . . . . . . . 9
β’ (π = (π + 1) β (βπ β (0...π)(β‘πβπ) β (β‘πβπ) β βπ β (0...π)(β‘πβ(π + 1)) β (β‘πβπ))) |
64 | 63 | rspcev 2842 |
. . . . . . . 8
β’ (((π + 1) β β0
β§ βπ β
(0...π)(β‘πβ(π + 1)) β (β‘πβπ)) β βπ β β0 βπ β (0...π)(β‘πβπ) β (β‘πβπ)) |
65 | 31, 60, 64 | syl2anc 411 |
. . . . . . 7
β’ ((π:π΄β1-1-ontoββ0 β§ π β β0) β
βπ β
β0 βπ β (0...π)(β‘πβπ) β (β‘πβπ)) |
66 | 65 | ralrimiva 2550 |
. . . . . 6
β’ (π:π΄β1-1-ontoββ0 β βπ β β0
βπ β
β0 βπ β (0...π)(β‘πβπ) β (β‘πβπ)) |
67 | | cnvexg 5167 |
. . . . . . . 8
β’ (π β V β β‘π β V) |
68 | 67 | elv 2742 |
. . . . . . 7
β’ β‘π β V |
69 | | foeq1 5435 |
. . . . . . . 8
β’ (π = β‘π β (π:β0βontoβπ΄ β β‘π:β0βontoβπ΄)) |
70 | | fveq1 5515 |
. . . . . . . . . . 11
β’ (π = β‘π β (πβπ) = (β‘πβπ)) |
71 | | fveq1 5515 |
. . . . . . . . . . 11
β’ (π = β‘π β (πβπ) = (β‘πβπ)) |
72 | 70, 71 | neeq12d 2367 |
. . . . . . . . . 10
β’ (π = β‘π β ((πβπ) β (πβπ) β (β‘πβπ) β (β‘πβπ))) |
73 | 72 | rexralbidv 2503 |
. . . . . . . . 9
β’ (π = β‘π β (βπ β β0 βπ β (0...π)(πβπ) β (πβπ) β βπ β β0 βπ β (0...π)(β‘πβπ) β (β‘πβπ))) |
74 | 73 | ralbidv 2477 |
. . . . . . . 8
β’ (π = β‘π β (βπ β β0 βπ β β0
βπ β (0...π)(πβπ) β (πβπ) β βπ β β0 βπ β β0
βπ β (0...π)(β‘πβπ) β (β‘πβπ))) |
75 | 69, 74 | anbi12d 473 |
. . . . . . 7
β’ (π = β‘π β ((π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(πβπ) β (πβπ)) β (β‘π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(β‘πβπ) β (β‘πβπ)))) |
76 | 68, 75 | spcev 2833 |
. . . . . 6
β’ ((β‘π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(β‘πβπ) β (β‘πβπ)) β βπ(π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(πβπ) β (πβπ))) |
77 | 29, 66, 76 | syl2anc 411 |
. . . . 5
β’ (π:π΄β1-1-ontoββ0 β βπ(π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(πβπ) β (πβπ))) |
78 | 26, 77 | jca 306 |
. . . 4
β’ (π:π΄β1-1-ontoββ0 β (βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ βπ(π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(πβπ) β (πβπ)))) |
79 | 78 | adantl 277 |
. . 3
β’ ((π΄ β β0
β§ π:π΄β1-1-ontoββ0) β (βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ βπ(π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(πβπ) β (πβπ)))) |
80 | 6, 79 | exlimddv 1898 |
. 2
β’ (π΄ β β0
β (βπ₯ β
π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ βπ(π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(πβπ) β (πβπ)))) |
81 | 4, 80 | syl 14 |
1
β’ (π΄ β β β
(βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦ β§ βπ(π:β0βontoβπ΄ β§ βπ β β0 βπ β β0
βπ β (0...π)(πβπ) β (πβπ)))) |