Step | Hyp | Ref
| Expression |
1 | | prmex 16558 |
. . . . . 6
β’ β
β V |
2 | 1 | mptex 7174 |
. . . . 5
β’ (π β β β¦ (π pCnt π)) β V |
3 | | 1arith.1 |
. . . . 5
β’ π = (π β β β¦ (π β β β¦ (π pCnt π))) |
4 | 2, 3 | fnmpti 6645 |
. . . 4
β’ π Fn β |
5 | 3 | 1arithlem3 16802 |
. . . . . . 7
β’ (π₯ β β β (πβπ₯):ββΆβ0) |
6 | | nn0ex 12424 |
. . . . . . . 8
β’
β0 β V |
7 | 6, 1 | elmap 8812 |
. . . . . . 7
β’ ((πβπ₯) β (β0
βm β) β (πβπ₯):ββΆβ0) |
8 | 5, 7 | sylibr 233 |
. . . . . 6
β’ (π₯ β β β (πβπ₯) β (β0
βm β)) |
9 | | fzfi 13883 |
. . . . . . 7
β’
(1...π₯) β
Fin |
10 | | ffn 6669 |
. . . . . . . . . 10
β’ ((πβπ₯):ββΆβ0 β
(πβπ₯) Fn β) |
11 | | elpreima 7009 |
. . . . . . . . . 10
β’ ((πβπ₯) Fn β β (π β (β‘(πβπ₯) β β) β (π β β β§ ((πβπ₯)βπ) β β))) |
12 | 5, 10, 11 | 3syl 18 |
. . . . . . . . 9
β’ (π₯ β β β (π β (β‘(πβπ₯) β β) β (π β β β§ ((πβπ₯)βπ) β β))) |
13 | 3 | 1arithlem2 16801 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β ((πβπ₯)βπ) = (π pCnt π₯)) |
14 | 13 | eleq1d 2819 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π β β) β (((πβπ₯)βπ) β β β (π pCnt π₯) β β)) |
15 | | prmz 16556 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
16 | | id 22 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π₯ β
β) |
17 | | dvdsle 16197 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π₯ β β) β (π β₯ π₯ β π β€ π₯)) |
18 | 15, 16, 17 | syl2anr 598 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β (π β₯ π₯ β π β€ π₯)) |
19 | | pcelnn 16747 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π₯ β β) β ((π pCnt π₯) β β β π β₯ π₯)) |
20 | 19 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β ((π pCnt π₯) β β β π β₯ π₯)) |
21 | | prmnn 16555 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
22 | | nnuz 12811 |
. . . . . . . . . . . . . 14
β’ β =
(β€β₯β1) |
23 | 21, 22 | eleqtrdi 2844 |
. . . . . . . . . . . . 13
β’ (π β β β π β
(β€β₯β1)) |
24 | | nnz 12525 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π₯ β
β€) |
25 | | elfz5 13439 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β1) β§ π₯ β β€) β (π β (1...π₯) β π β€ π₯)) |
26 | 23, 24, 25 | syl2anr 598 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β (π β (1...π₯) β π β€ π₯)) |
27 | 18, 20, 26 | 3imtr4d 294 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π β β) β ((π pCnt π₯) β β β π β (1...π₯))) |
28 | 14, 27 | sylbid 239 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π β β) β (((πβπ₯)βπ) β β β π β (1...π₯))) |
29 | 28 | expimpd 455 |
. . . . . . . . 9
β’ (π₯ β β β ((π β β β§ ((πβπ₯)βπ) β β) β π β (1...π₯))) |
30 | 12, 29 | sylbid 239 |
. . . . . . . 8
β’ (π₯ β β β (π β (β‘(πβπ₯) β β) β π β (1...π₯))) |
31 | 30 | ssrdv 3951 |
. . . . . . 7
β’ (π₯ β β β (β‘(πβπ₯) β β) β (1...π₯)) |
32 | | ssfi 9120 |
. . . . . . 7
β’
(((1...π₯) β Fin
β§ (β‘(πβπ₯) β β) β (1...π₯)) β (β‘(πβπ₯) β β) β
Fin) |
33 | 9, 31, 32 | sylancr 588 |
. . . . . 6
β’ (π₯ β β β (β‘(πβπ₯) β β) β
Fin) |
34 | | cnveq 5830 |
. . . . . . . . 9
β’ (π = (πβπ₯) β β‘π = β‘(πβπ₯)) |
35 | 34 | imaeq1d 6013 |
. . . . . . . 8
β’ (π = (πβπ₯) β (β‘π β β) = (β‘(πβπ₯) β β)) |
36 | 35 | eleq1d 2819 |
. . . . . . 7
β’ (π = (πβπ₯) β ((β‘π β β) β Fin β (β‘(πβπ₯) β β) β
Fin)) |
37 | | 1arith.2 |
. . . . . . 7
β’ π
= {π β (β0
βm β) β£ (β‘π β β) β
Fin} |
38 | 36, 37 | elrab2 3649 |
. . . . . 6
β’ ((πβπ₯) β π
β ((πβπ₯) β (β0
βm β) β§ (β‘(πβπ₯) β β) β
Fin)) |
39 | 8, 33, 38 | sylanbrc 584 |
. . . . 5
β’ (π₯ β β β (πβπ₯) β π
) |
40 | 39 | rgen 3063 |
. . . 4
β’
βπ₯ β
β (πβπ₯) β π
|
41 | | ffnfv 7067 |
. . . 4
β’ (π:ββΆπ
β (π Fn β β§ βπ₯ β β (πβπ₯) β π
)) |
42 | 4, 40, 41 | mpbir2an 710 |
. . 3
β’ π:ββΆπ
|
43 | 13 | adantlr 714 |
. . . . . . . 8
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β ((πβπ₯)βπ) = (π pCnt π₯)) |
44 | 3 | 1arithlem2 16801 |
. . . . . . . . 9
β’ ((π¦ β β β§ π β β) β ((πβπ¦)βπ) = (π pCnt π¦)) |
45 | 44 | adantll 713 |
. . . . . . . 8
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β ((πβπ¦)βπ) = (π pCnt π¦)) |
46 | 43, 45 | eqeq12d 2749 |
. . . . . . 7
β’ (((π₯ β β β§ π¦ β β) β§ π β β) β (((πβπ₯)βπ) = ((πβπ¦)βπ) β (π pCnt π₯) = (π pCnt π¦))) |
47 | 46 | ralbidva 3169 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β
(βπ β β
((πβπ₯)βπ) = ((πβπ¦)βπ) β βπ β β (π pCnt π₯) = (π pCnt π¦))) |
48 | 3 | 1arithlem3 16802 |
. . . . . . 7
β’ (π¦ β β β (πβπ¦):ββΆβ0) |
49 | | ffn 6669 |
. . . . . . . 8
β’ ((πβπ¦):ββΆβ0 β
(πβπ¦) Fn β) |
50 | | eqfnfv 6983 |
. . . . . . . 8
β’ (((πβπ₯) Fn β β§ (πβπ¦) Fn β) β ((πβπ₯) = (πβπ¦) β βπ β β ((πβπ₯)βπ) = ((πβπ¦)βπ))) |
51 | 10, 49, 50 | syl2an 597 |
. . . . . . 7
β’ (((πβπ₯):ββΆβ0 β§
(πβπ¦):ββΆβ0) β
((πβπ₯) = (πβπ¦) β βπ β β ((πβπ₯)βπ) = ((πβπ¦)βπ))) |
52 | 5, 48, 51 | syl2an 597 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β ((πβπ₯) = (πβπ¦) β βπ β β ((πβπ₯)βπ) = ((πβπ¦)βπ))) |
53 | | nnnn0 12425 |
. . . . . . 7
β’ (π₯ β β β π₯ β
β0) |
54 | | nnnn0 12425 |
. . . . . . 7
β’ (π¦ β β β π¦ β
β0) |
55 | | pc11 16757 |
. . . . . . 7
β’ ((π₯ β β0
β§ π¦ β
β0) β (π₯ = π¦ β βπ β β (π pCnt π₯) = (π pCnt π¦))) |
56 | 53, 54, 55 | syl2an 597 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β (π₯ = π¦ β βπ β β (π pCnt π₯) = (π pCnt π¦))) |
57 | 47, 52, 56 | 3bitr4d 311 |
. . . . 5
β’ ((π₯ β β β§ π¦ β β) β ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
58 | 57 | biimpd 228 |
. . . 4
β’ ((π₯ β β β§ π¦ β β) β ((πβπ₯) = (πβπ¦) β π₯ = π¦)) |
59 | 58 | rgen2 3191 |
. . 3
β’
βπ₯ β
β βπ¦ β
β ((πβπ₯) = (πβπ¦) β π₯ = π¦) |
60 | | dff13 7203 |
. . 3
β’ (π:ββ1-1βπ
β (π:ββΆπ
β§ βπ₯ β β βπ¦ β β ((πβπ₯) = (πβπ¦) β π₯ = π¦))) |
61 | 42, 59, 60 | mpbir2an 710 |
. 2
β’ π:ββ1-1βπ
|
62 | | eqid 2733 |
. . . . . 6
β’ (π β β β¦ if(π β β, (πβ(πβπ)), 1)) = (π β β β¦ if(π β β, (πβ(πβπ)), 1)) |
63 | | cnveq 5830 |
. . . . . . . . . . . 12
β’ (π = π β β‘π = β‘π) |
64 | 63 | imaeq1d 6013 |
. . . . . . . . . . 11
β’ (π = π β (β‘π β β) = (β‘π β β)) |
65 | 64 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = π β ((β‘π β β) β Fin β (β‘π β β) β
Fin)) |
66 | 65, 37 | elrab2 3649 |
. . . . . . . . 9
β’ (π β π
β (π β (β0
βm β) β§ (β‘π β β) β
Fin)) |
67 | 66 | simplbi 499 |
. . . . . . . 8
β’ (π β π
β π β (β0
βm β)) |
68 | 6, 1 | elmap 8812 |
. . . . . . . 8
β’ (π β (β0
βm β) β π:ββΆβ0) |
69 | 67, 68 | sylib 217 |
. . . . . . 7
β’ (π β π
β π:ββΆβ0) |
70 | 69 | ad2antrr 725 |
. . . . . 6
β’ (((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β π:ββΆβ0) |
71 | | simplr 768 |
. . . . . . . . 9
β’ (((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β π¦ β β) |
72 | | 0re 11162 |
. . . . . . . . 9
β’ 0 β
β |
73 | | ifcl 4532 |
. . . . . . . . 9
β’ ((π¦ β β β§ 0 β
β) β if(0 β€ π¦, π¦, 0) β β) |
74 | 71, 72, 73 | sylancl 587 |
. . . . . . . 8
β’ (((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β if(0 β€ π¦, π¦, 0) β β) |
75 | | max1 13110 |
. . . . . . . . 9
β’ ((0
β β β§ π¦
β β) β 0 β€ if(0 β€ π¦, π¦, 0)) |
76 | 72, 71, 75 | sylancr 588 |
. . . . . . . 8
β’ (((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β 0 β€ if(0 β€ π¦, π¦, 0)) |
77 | | flge0nn0 13731 |
. . . . . . . 8
β’ ((if(0
β€ π¦, π¦, 0) β β β§ 0 β€ if(0 β€
π¦, π¦, 0)) β (ββif(0 β€ π¦, π¦, 0)) β
β0) |
78 | 74, 76, 77 | syl2anc 585 |
. . . . . . 7
β’ (((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β (ββif(0 β€ π¦, π¦, 0)) β
β0) |
79 | | nn0p1nn 12457 |
. . . . . . 7
β’
((ββif(0 β€ π¦, π¦, 0)) β β0 β
((ββif(0 β€ π¦, π¦, 0)) + 1) β β) |
80 | 78, 79 | syl 17 |
. . . . . 6
β’ (((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β ((ββif(0 β€ π¦, π¦, 0)) + 1) β β) |
81 | 71 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β π¦ β β) |
82 | 80 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β ((ββif(0 β€ π¦, π¦, 0)) + 1) β β) |
83 | 82 | nnred 12173 |
. . . . . . . . . 10
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β ((ββif(0 β€ π¦, π¦, 0)) + 1) β β) |
84 | 15 | ssriv 3949 |
. . . . . . . . . . . 12
β’ β
β β€ |
85 | | zssre 12511 |
. . . . . . . . . . . 12
β’ β€
β β |
86 | 84, 85 | sstri 3954 |
. . . . . . . . . . 11
β’ β
β β |
87 | | simprl 770 |
. . . . . . . . . . 11
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β π β β) |
88 | 86, 87 | sselid 3943 |
. . . . . . . . . 10
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β π β β) |
89 | 74 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β if(0 β€ π¦, π¦, 0) β β) |
90 | | max2 13112 |
. . . . . . . . . . . 12
β’ ((0
β β β§ π¦
β β) β π¦
β€ if(0 β€ π¦, π¦, 0)) |
91 | 72, 81, 90 | sylancr 588 |
. . . . . . . . . . 11
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β π¦ β€ if(0 β€ π¦, π¦, 0)) |
92 | | flltp1 13711 |
. . . . . . . . . . . 12
β’ (if(0
β€ π¦, π¦, 0) β β β if(0 β€ π¦, π¦, 0) < ((ββif(0 β€ π¦, π¦, 0)) + 1)) |
93 | 89, 92 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β if(0 β€ π¦, π¦, 0) < ((ββif(0 β€ π¦, π¦, 0)) + 1)) |
94 | 81, 89, 83, 91, 93 | lelttrd 11318 |
. . . . . . . . . 10
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β π¦ < ((ββif(0 β€ π¦, π¦, 0)) + 1)) |
95 | | simprr 772 |
. . . . . . . . . 10
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β ((ββif(0 β€ π¦, π¦, 0)) + 1) β€ π) |
96 | 81, 83, 88, 94, 95 | ltletrd 11320 |
. . . . . . . . 9
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β π¦ < π) |
97 | 81, 88 | ltnled 11307 |
. . . . . . . . 9
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β (π¦ < π β Β¬ π β€ π¦)) |
98 | 96, 97 | mpbid 231 |
. . . . . . . 8
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β Β¬ π β€ π¦) |
99 | 87 | biantrurd 534 |
. . . . . . . . . 10
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β ((πβπ) β β β (π β β β§ (πβπ) β β))) |
100 | 70 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β π:ββΆβ0) |
101 | | ffn 6669 |
. . . . . . . . . . 11
β’ (π:ββΆβ0 β
π Fn
β) |
102 | | elpreima 7009 |
. . . . . . . . . . 11
β’ (π Fn β β (π β (β‘π β β) β (π β β β§ (πβπ) β β))) |
103 | 100, 101,
102 | 3syl 18 |
. . . . . . . . . 10
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β (π β (β‘π β β) β (π β β β§ (πβπ) β β))) |
104 | 99, 103 | bitr4d 282 |
. . . . . . . . 9
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β ((πβπ) β β β π β (β‘π β β))) |
105 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β βπ β (β‘π β β)π β€ π¦) |
106 | | breq1 5109 |
. . . . . . . . . . 11
β’ (π = π β (π β€ π¦ β π β€ π¦)) |
107 | 106 | rspccv 3577 |
. . . . . . . . . 10
β’
(βπ β
(β‘π β β)π β€ π¦ β (π β (β‘π β β) β π β€ π¦)) |
108 | 105, 107 | syl 17 |
. . . . . . . . 9
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β (π β (β‘π β β) β π β€ π¦)) |
109 | 104, 108 | sylbid 239 |
. . . . . . . 8
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β ((πβπ) β β β π β€ π¦)) |
110 | 98, 109 | mtod 197 |
. . . . . . 7
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β Β¬ (πβπ) β β) |
111 | 100, 87 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β (πβπ) β
β0) |
112 | | elnn0 12420 |
. . . . . . . . 9
β’ ((πβπ) β β0 β ((πβπ) β β β¨ (πβπ) = 0)) |
113 | 111, 112 | sylib 217 |
. . . . . . . 8
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β ((πβπ) β β β¨ (πβπ) = 0)) |
114 | 113 | ord 863 |
. . . . . . 7
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β (Β¬ (πβπ) β β β (πβπ) = 0)) |
115 | 110, 114 | mpd 15 |
. . . . . 6
β’ ((((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β§ (π β β β§ ((ββif(0
β€ π¦, π¦, 0)) + 1) β€ π)) β (πβπ) = 0) |
116 | 3, 62, 70, 80, 115 | 1arithlem4 16803 |
. . . . 5
β’ (((π β π
β§ π¦ β β) β§ βπ β (β‘π β β)π β€ π¦) β βπ₯ β β π = (πβπ₯)) |
117 | | cnvimass 6034 |
. . . . . . 7
β’ (β‘π β β) β dom π |
118 | 69 | fdmd 6680 |
. . . . . . . 8
β’ (π β π
β dom π = β) |
119 | 118, 86 | eqsstrdi 3999 |
. . . . . . 7
β’ (π β π
β dom π β β) |
120 | 117, 119 | sstrid 3956 |
. . . . . 6
β’ (π β π
β (β‘π β β) β
β) |
121 | 66 | simprbi 498 |
. . . . . 6
β’ (π β π
β (β‘π β β) β
Fin) |
122 | | fimaxre2 12105 |
. . . . . 6
β’ (((β‘π β β) β β β§
(β‘π β β) β Fin) β
βπ¦ β β
βπ β (β‘π β β)π β€ π¦) |
123 | 120, 121,
122 | syl2anc 585 |
. . . . 5
β’ (π β π
β βπ¦ β β βπ β (β‘π β β)π β€ π¦) |
124 | 116, 123 | r19.29a 3156 |
. . . 4
β’ (π β π
β βπ₯ β β π = (πβπ₯)) |
125 | 124 | rgen 3063 |
. . 3
β’
βπ β
π
βπ₯ β β π = (πβπ₯) |
126 | | dffo3 7053 |
. . 3
β’ (π:ββontoβπ
β (π:ββΆπ
β§ βπ β π
βπ₯ β β π = (πβπ₯))) |
127 | 42, 125, 126 | mpbir2an 710 |
. 2
β’ π:ββontoβπ
|
128 | | df-f1o 6504 |
. 2
β’ (π:ββ1-1-ontoβπ
β (π:ββ1-1βπ
β§ π:ββontoβπ
)) |
129 | 61, 127, 128 | mpbir2an 710 |
1
β’ π:ββ1-1-ontoβπ
|