Step | Hyp | Ref
| Expression |
1 | | suceq 4403 |
. . . . 5
β’ (π = (β‘πβπ) β suc π = suc (β‘πβπ)) |
2 | 1 | raleqdv 2679 |
. . . 4
β’ (π = (β‘πβπ) β (βπ β suc π(πΉβπ) β (πΉβπ) β βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) |
3 | 2 | rexbidv 2478 |
. . 3
β’ (π = (β‘πβπ) β (βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ) β βπ β Ο βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) |
4 | | ennnfonelemh.ne |
. . 3
β’ (π β βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
5 | | ennnfonelemh.n |
. . . . . . 7
β’ π = frec((π₯ β β€ β¦ (π₯ + 1)), 0) |
6 | 5 | frechashgf1o 10428 |
. . . . . 6
β’ π:Οβ1-1-ontoββ0 |
7 | | f1ocnv 5475 |
. . . . . 6
β’ (π:Οβ1-1-ontoββ0 β β‘π:β0β1-1-ontoβΟ) |
8 | 6, 7 | ax-mp 5 |
. . . . 5
β’ β‘π:β0β1-1-ontoβΟ |
9 | | f1of 5462 |
. . . . 5
β’ (β‘π:β0β1-1-ontoβΟ β β‘π:β0βΆΟ) |
10 | 8, 9 | mp1i 10 |
. . . 4
β’ (π β β‘π:β0βΆΟ) |
11 | | ennnfonelemex.p |
. . . 4
β’ (π β π β
β0) |
12 | 10, 11 | ffvelcdmd 5653 |
. . 3
β’ (π β (β‘πβπ) β Ο) |
13 | 3, 4, 12 | rspcdva 2847 |
. 2
β’ (π β βπ β Ο βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ)) |
14 | | f1of 5462 |
. . . . 5
β’ (π:Οβ1-1-ontoββ0 β π:ΟβΆβ0) |
15 | 6, 14 | mp1i 10 |
. . . 4
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β π:ΟβΆβ0) |
16 | | peano2 4595 |
. . . . 5
β’ (π β Ο β suc π β
Ο) |
17 | 16 | ad2antrl 490 |
. . . 4
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β suc π β Ο) |
18 | 15, 17 | ffvelcdmd 5653 |
. . 3
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (πβsuc π) β
β0) |
19 | | ennnfonelemh.f |
. . . . . . . . 9
β’ (π β πΉ:Οβontoβπ΄) |
20 | 19 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β πΉ:Οβontoβπ΄) |
21 | | fofun 5440 |
. . . . . . . 8
β’ (πΉ:Οβontoβπ΄ β Fun πΉ) |
22 | 20, 21 | syl 14 |
. . . . . . 7
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β Fun πΉ) |
23 | | vex 2741 |
. . . . . . . . . 10
β’ π β V |
24 | 23 | sucid 4418 |
. . . . . . . . 9
β’ π β suc π |
25 | | simprl 529 |
. . . . . . . . . . . 12
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β π β Ο) |
26 | 25 | adantr 276 |
. . . . . . . . . . 11
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β π β Ο) |
27 | | fof 5439 |
. . . . . . . . . . . 12
β’ (πΉ:Οβontoβπ΄ β πΉ:ΟβΆπ΄) |
28 | | fdm 5372 |
. . . . . . . . . . . 12
β’ (πΉ:ΟβΆπ΄ β dom πΉ = Ο) |
29 | 20, 27, 28 | 3syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β dom πΉ = Ο) |
30 | 26, 29 | eleqtrrd 2257 |
. . . . . . . . . 10
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β π β dom πΉ) |
31 | | funfvima 5749 |
. . . . . . . . . 10
β’ ((Fun
πΉ β§ π β dom πΉ) β (π β suc π β (πΉβπ) β (πΉ β suc π))) |
32 | 22, 30, 31 | syl2anc 411 |
. . . . . . . . 9
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β (π β suc π β (πΉβπ) β (πΉ β suc π))) |
33 | 24, 32 | mpi 15 |
. . . . . . . 8
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β (πΉβπ) β (πΉ β suc π)) |
34 | | simpr 110 |
. . . . . . . . . . 11
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β dom (π»βπ) = dom (π»β(πβsuc π))) |
35 | | ennnfonelemh.dceq |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦) |
36 | 35 | adantr 276 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β βπ₯ β π΄ βπ¦ β π΄ DECID π₯ = π¦) |
37 | 19 | adantr 276 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β πΉ:Οβontoβπ΄) |
38 | 4 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
39 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πΉβπ) = (πΉβπ)) |
40 | 39 | neeq2d 2366 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((πΉβπ) β (πΉβπ) β (πΉβπ) β (πΉβπ))) |
41 | 40 | cbvralv 2704 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
suc π(πΉβπ) β (πΉβπ) β βπ β suc π(πΉβπ) β (πΉβπ)) |
42 | 41 | rexbii 2484 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
Ο βπ β
suc π(πΉβπ) β (πΉβπ) β βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
43 | | fveq2 5516 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πΉβπ) = (πΉβπ)) |
44 | 43 | neeq1d 2365 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((πΉβπ) β (πΉβπ) β (πΉβπ) β (πΉβπ))) |
45 | 44 | ralbidv 2477 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (βπ β suc π(πΉβπ) β (πΉβπ) β βπ β suc π(πΉβπ) β (πΉβπ))) |
46 | 45 | cbvrexv 2705 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
Ο βπ β
suc π(πΉβπ) β (πΉβπ) β βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
47 | 42, 46 | bitri 184 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ β
Ο βπ β
suc π(πΉβπ) β (πΉβπ) β βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
48 | 47 | ralbii 2483 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
Ο βπ β
Ο βπ β
suc π(πΉβπ) β (πΉβπ) β βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
49 | 38, 48 | sylib 122 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
50 | | ennnfonelemh.g |
. . . . . . . . . . . . . . . . 17
β’ πΊ = (π₯ β (π΄ βpm Ο), π¦ β Ο β¦
if((πΉβπ¦) β (πΉ β π¦), π₯, (π₯ βͺ {β¨dom π₯, (πΉβπ¦)β©}))) |
51 | | ennnfonelemh.j |
. . . . . . . . . . . . . . . . 17
β’ π½ = (π₯ β β0 β¦ if(π₯ = 0, β
, (β‘πβ(π₯ β 1)))) |
52 | | ennnfonelemh.h |
. . . . . . . . . . . . . . . . 17
β’ π» = seq0(πΊ, π½) |
53 | 36, 37, 49, 50, 5, 51, 52, 18 | ennnfonelemhf1o 12414 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1-ontoβ(πΉ β (β‘πβ(πβsuc π)))) |
54 | | f1ofun 5464 |
. . . . . . . . . . . . . . . 16
β’ ((π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1-ontoβ(πΉ β (β‘πβ(πβsuc π))) β Fun (π»β(πβsuc π))) |
55 | 53, 54 | syl 14 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β Fun (π»β(πβsuc π))) |
56 | 55 | ad2antrr 488 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ π β dom (π»βπ)) β Fun (π»β(πβsuc π))) |
57 | 11 | adantr 276 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β π β
β0) |
58 | 6, 14 | mp1i 10 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β Ο) β π:ΟβΆβ0) |
59 | 16 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β Ο) β suc π β
Ο) |
60 | 58, 59 | ffvelcdmd 5653 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β Ο) β (πβsuc π) β
β0) |
61 | 60 | adantrr 479 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (πβsuc π) β
β0) |
62 | 57 | nn0red 9230 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β π β β) |
63 | 61 | nn0red 9230 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (πβsuc π) β β) |
64 | | f1ocnvfv2 5779 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:Οβ1-1-ontoββ0 β§ π β β0) β (πβ(β‘πβπ)) = π) |
65 | 6, 57, 64 | sylancr 414 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (πβ(β‘πβπ)) = π) |
66 | 12 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (β‘πβπ) β Ο) |
67 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ)) |
68 | 37, 25, 66, 67 | ennnfonelemk 12401 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (β‘πβπ) β π) |
69 | | elelsuc 4410 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((β‘πβπ) β π β (β‘πβπ) β suc π) |
70 | 68, 69 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (β‘πβπ) β suc π) |
71 | | 0zd 9265 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β 0 β β€) |
72 | 71, 5, 66, 17 | frec2uzltd 10403 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β ((β‘πβπ) β suc π β (πβ(β‘πβπ)) < (πβsuc π))) |
73 | 70, 72 | mpd 13 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (πβ(β‘πβπ)) < (πβsuc π)) |
74 | 65, 73 | eqbrtrrd 4028 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β π < (πβsuc π)) |
75 | 62, 63, 74 | ltled 8076 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β π β€ (πβsuc π)) |
76 | 36, 37, 38, 50, 5, 51, 52, 57, 61, 75 | ennnfoneleminc 12412 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (π»βπ) β (π»β(πβsuc π))) |
77 | 76 | ad2antrr 488 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ π β dom (π»βπ)) β (π»βπ) β (π»β(πβsuc π))) |
78 | | simpr 110 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ π β dom (π»βπ)) β π β dom (π»βπ)) |
79 | | funssfv 5542 |
. . . . . . . . . . . . . 14
β’ ((Fun
(π»β(πβsuc π)) β§ (π»βπ) β (π»β(πβsuc π)) β§ π β dom (π»βπ)) β ((π»β(πβsuc π))βπ ) = ((π»βπ)βπ )) |
80 | 56, 77, 78, 79 | syl3anc 1238 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ π β dom (π»βπ)) β ((π»β(πβsuc π))βπ ) = ((π»βπ)βπ )) |
81 | 80 | eqcomd 2183 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ π β dom (π»βπ)) β ((π»βπ)βπ ) = ((π»β(πβsuc π))βπ )) |
82 | 81 | ralrimiva 2550 |
. . . . . . . . . . 11
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β βπ β dom (π»βπ)((π»βπ)βπ ) = ((π»β(πβsuc π))βπ )) |
83 | 36, 37, 49, 50, 5, 51, 52, 57 | ennnfonelemhf1o 12414 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (π»βπ):dom (π»βπ)β1-1-ontoβ(πΉ β (β‘πβπ))) |
84 | | f1ofun 5464 |
. . . . . . . . . . . . . 14
β’ ((π»βπ):dom (π»βπ)β1-1-ontoβ(πΉ β (β‘πβπ)) β Fun (π»βπ)) |
85 | 83, 84 | syl 14 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β Fun (π»βπ)) |
86 | | eqfunfv 5619 |
. . . . . . . . . . . . 13
β’ ((Fun
(π»βπ) β§ Fun (π»β(πβsuc π))) β ((π»βπ) = (π»β(πβsuc π)) β (dom (π»βπ) = dom (π»β(πβsuc π)) β§ βπ β dom (π»βπ)((π»βπ)βπ ) = ((π»β(πβsuc π))βπ )))) |
87 | 85, 55, 86 | syl2anc 411 |
. . . . . . . . . . . 12
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β ((π»βπ) = (π»β(πβsuc π)) β (dom (π»βπ) = dom (π»β(πβsuc π)) β§ βπ β dom (π»βπ)((π»βπ)βπ ) = ((π»β(πβsuc π))βπ )))) |
88 | 87 | adantr 276 |
. . . . . . . . . . 11
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β ((π»βπ) = (π»β(πβsuc π)) β (dom (π»βπ) = dom (π»β(πβsuc π)) β§ βπ β dom (π»βπ)((π»βπ)βπ ) = ((π»β(πβsuc π))βπ )))) |
89 | 34, 82, 88 | mpbir2and 944 |
. . . . . . . . . 10
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β (π»βπ) = (π»β(πβsuc π))) |
90 | 89 | rneqd 4857 |
. . . . . . . . 9
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β ran (π»βπ) = ran (π»β(πβsuc π))) |
91 | | dff1o5 5471 |
. . . . . . . . . . . 12
β’ ((π»βπ):dom (π»βπ)β1-1-ontoβ(πΉ β (β‘πβπ)) β ((π»βπ):dom (π»βπ)β1-1β(πΉ β (β‘πβπ)) β§ ran (π»βπ) = (πΉ β (β‘πβπ)))) |
92 | 83, 91 | sylib 122 |
. . . . . . . . . . 11
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β ((π»βπ):dom (π»βπ)β1-1β(πΉ β (β‘πβπ)) β§ ran (π»βπ) = (πΉ β (β‘πβπ)))) |
93 | 92 | simprd 114 |
. . . . . . . . . 10
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β ran (π»βπ) = (πΉ β (β‘πβπ))) |
94 | 93 | adantr 276 |
. . . . . . . . 9
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β ran (π»βπ) = (πΉ β (β‘πβπ))) |
95 | | f1ocnvfv1 5778 |
. . . . . . . . . . . . . . . 16
β’ ((π:Οβ1-1-ontoββ0 β§ suc π β Ο) β (β‘πβ(πβsuc π)) = suc π) |
96 | 6, 17, 95 | sylancr 414 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (β‘πβ(πβsuc π)) = suc π) |
97 | 96 | imaeq2d 4971 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (πΉ β (β‘πβ(πβsuc π))) = (πΉ β suc π)) |
98 | | f1oeq3 5452 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (β‘πβ(πβsuc π))) = (πΉ β suc π) β ((π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1-ontoβ(πΉ β (β‘πβ(πβsuc π))) β (π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1-ontoβ(πΉ β suc π))) |
99 | 97, 98 | syl 14 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β ((π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1-ontoβ(πΉ β (β‘πβ(πβsuc π))) β (π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1-ontoβ(πΉ β suc π))) |
100 | 53, 99 | mpbid 147 |
. . . . . . . . . . . 12
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1-ontoβ(πΉ β suc π)) |
101 | | dff1o5 5471 |
. . . . . . . . . . . 12
β’ ((π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1-ontoβ(πΉ β suc π) β ((π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1β(πΉ β suc π) β§ ran (π»β(πβsuc π)) = (πΉ β suc π))) |
102 | 100, 101 | sylib 122 |
. . . . . . . . . . 11
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β ((π»β(πβsuc π)):dom (π»β(πβsuc π))β1-1β(πΉ β suc π) β§ ran (π»β(πβsuc π)) = (πΉ β suc π))) |
103 | 102 | simprd 114 |
. . . . . . . . . 10
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β ran (π»β(πβsuc π)) = (πΉ β suc π)) |
104 | 103 | adantr 276 |
. . . . . . . . 9
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β ran (π»β(πβsuc π)) = (πΉ β suc π)) |
105 | 90, 94, 104 | 3eqtr3d 2218 |
. . . . . . . 8
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β (πΉ β (β‘πβπ)) = (πΉ β suc π)) |
106 | 33, 105 | eleqtrrd 2257 |
. . . . . . 7
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β (πΉβπ) β (πΉ β (β‘πβπ))) |
107 | | fvelima 5568 |
. . . . . . 7
β’ ((Fun
πΉ β§ (πΉβπ) β (πΉ β (β‘πβπ))) β βπ β (β‘πβπ)(πΉβπ) = (πΉβπ)) |
108 | 22, 106, 107 | syl2anc 411 |
. . . . . 6
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β βπ β (β‘πβπ)(πΉβπ) = (πΉβπ)) |
109 | | simprr 531 |
. . . . . . 7
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ (π β (β‘πβπ) β§ (πΉβπ) = (πΉβπ))) β (πΉβπ) = (πΉβπ)) |
110 | | fveq2 5516 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
111 | 110 | neeq2d 2366 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) β (πΉβπ) β (πΉβπ) β (πΉβπ))) |
112 | 67 | ad2antrr 488 |
. . . . . . . . 9
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ (π β (β‘πβπ) β§ (πΉβπ) = (πΉβπ))) β βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ)) |
113 | | elelsuc 4410 |
. . . . . . . . . 10
β’ (π β (β‘πβπ) β π β suc (β‘πβπ)) |
114 | 113 | ad2antrl 490 |
. . . . . . . . 9
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ (π β (β‘πβπ) β§ (πΉβπ) = (πΉβπ))) β π β suc (β‘πβπ)) |
115 | 111, 112,
114 | rspcdva 2847 |
. . . . . . . 8
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ (π β (β‘πβπ) β§ (πΉβπ) = (πΉβπ))) β (πΉβπ) β (πΉβπ)) |
116 | 115 | necomd 2433 |
. . . . . . 7
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ (π β (β‘πβπ) β§ (πΉβπ) = (πΉβπ))) β (πΉβπ) β (πΉβπ)) |
117 | 109, 116 | pm2.21ddne 2430 |
. . . . . 6
β’ ((((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β§ (π β (β‘πβπ) β§ (πΉβπ) = (πΉβπ))) β β₯) |
118 | 108, 117 | rexlimddv 2599 |
. . . . 5
β’ (((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β§ dom (π»βπ) = dom (π»β(πβsuc π))) β β₯) |
119 | 118 | inegd 1372 |
. . . 4
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β Β¬ dom (π»βπ) = dom (π»β(πβsuc π))) |
120 | | dmss 4827 |
. . . . . 6
β’ ((π»βπ) β (π»β(πβsuc π)) β dom (π»βπ) β dom (π»β(πβsuc π))) |
121 | 76, 120 | syl 14 |
. . . . 5
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β dom (π»βπ) β dom (π»β(πβsuc π))) |
122 | 35, 19, 4, 50, 5, 51, 52, 11 | ennnfonelemom 12409 |
. . . . . . 7
β’ (π β dom (π»βπ) β Ο) |
123 | 122 | adantr 276 |
. . . . . 6
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β dom (π»βπ) β Ο) |
124 | 42 | a1i 9 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ) β βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ))) |
125 | 124 | ralbidv 2477 |
. . . . . . . 8
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ) β βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ))) |
126 | 38, 125 | mpbid 147 |
. . . . . . 7
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β βπ β Ο βπ β Ο βπ β suc π(πΉβπ) β (πΉβπ)) |
127 | 36, 37, 126, 50, 5, 51, 52, 61 | ennnfonelemom 12409 |
. . . . . 6
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β dom (π»β(πβsuc π)) β Ο) |
128 | | nntri1 6497 |
. . . . . 6
β’ ((dom
(π»βπ) β Ο β§ dom (π»β(πβsuc π)) β Ο) β (dom (π»βπ) β dom (π»β(πβsuc π)) β Β¬ dom (π»β(πβsuc π)) β dom (π»βπ))) |
129 | 123, 127,
128 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (dom (π»βπ) β dom (π»β(πβsuc π)) β Β¬ dom (π»β(πβsuc π)) β dom (π»βπ))) |
130 | 121, 129 | mpbid 147 |
. . . 4
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β Β¬ dom (π»β(πβsuc π)) β dom (π»βπ)) |
131 | | nntri3or 6494 |
. . . . 5
β’ ((dom
(π»βπ) β Ο β§ dom (π»β(πβsuc π)) β Ο) β (dom (π»βπ) β dom (π»β(πβsuc π)) β¨ dom (π»βπ) = dom (π»β(πβsuc π)) β¨ dom (π»β(πβsuc π)) β dom (π»βπ))) |
132 | 123, 127,
131 | syl2anc 411 |
. . . 4
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β (dom (π»βπ) β dom (π»β(πβsuc π)) β¨ dom (π»βπ) = dom (π»β(πβsuc π)) β¨ dom (π»β(πβsuc π)) β dom (π»βπ))) |
133 | 119, 130,
132 | ecase23d 1350 |
. . 3
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β dom (π»βπ) β dom (π»β(πβsuc π))) |
134 | | fveq2 5516 |
. . . . . 6
β’ (π = (πβsuc π) β (π»βπ) = (π»β(πβsuc π))) |
135 | 134 | dmeqd 4830 |
. . . . 5
β’ (π = (πβsuc π) β dom (π»βπ) = dom (π»β(πβsuc π))) |
136 | 135 | eleq2d 2247 |
. . . 4
β’ (π = (πβsuc π) β (dom (π»βπ) β dom (π»βπ) β dom (π»βπ) β dom (π»β(πβsuc π)))) |
137 | 136 | rspcev 2842 |
. . 3
β’ (((πβsuc π) β β0 β§ dom (π»βπ) β dom (π»β(πβsuc π))) β βπ β β0 dom (π»βπ) β dom (π»βπ)) |
138 | 18, 133, 137 | syl2anc 411 |
. 2
β’ ((π β§ (π β Ο β§ βπ β suc (β‘πβπ)(πΉβπ) β (πΉβπ))) β βπ β β0 dom (π»βπ) β dom (π»βπ)) |
139 | 13, 138 | rexlimddv 2599 |
1
β’ (π β βπ β β0 dom (π»βπ) β dom (π»βπ)) |