Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . . . 6
β’ (π β β β
(1...π) β
Fin) |
2 | | ficardom 9904 |
. . . . . 6
β’
((1...π) β Fin
β (cardβ(1...π))
β Ο) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β β β
(cardβ(1...π)) β
Ο) |
4 | | isinf 9211 |
. . . . 5
β’ (Β¬
π΄ β Fin β
βπ β Ο
βπ₯(π₯ β π΄ β§ π₯ β π)) |
5 | | breq2 5114 |
. . . . . . . 8
β’ (π = (cardβ(1...π)) β (π₯ β π β π₯ β (cardβ(1...π)))) |
6 | 5 | anbi2d 630 |
. . . . . . 7
β’ (π = (cardβ(1...π)) β ((π₯ β π΄ β§ π₯ β π) β (π₯ β π΄ β§ π₯ β (cardβ(1...π))))) |
7 | 6 | exbidv 1925 |
. . . . . 6
β’ (π = (cardβ(1...π)) β (βπ₯(π₯ β π΄ β§ π₯ β π) β βπ₯(π₯ β π΄ β§ π₯ β (cardβ(1...π))))) |
8 | 7 | rspcva 3582 |
. . . . 5
β’
(((cardβ(1...π)) β Ο β§ βπ β Ο βπ₯(π₯ β π΄ β§ π₯ β π)) β βπ₯(π₯ β π΄ β§ π₯ β (cardβ(1...π)))) |
9 | 3, 4, 8 | syl2anr 598 |
. . . 4
β’ ((Β¬
π΄ β Fin β§ π β β) β
βπ₯(π₯ β π΄ β§ π₯ β (cardβ(1...π)))) |
10 | | velpw 4570 |
. . . . . . . 8
β’ (π₯ β π« π΄ β π₯ β π΄) |
11 | 10 | biimpri 227 |
. . . . . . 7
β’ (π₯ β π΄ β π₯ β π« π΄) |
12 | 11 | a1i 11 |
. . . . . 6
β’ ((Β¬
π΄ β Fin β§ π β β) β (π₯ β π΄ β π₯ β π« π΄)) |
13 | | hasheni 14255 |
. . . . . . . . 9
β’ (π₯ β (cardβ(1...π)) β (β―βπ₯) =
(β―β(cardβ(1...π)))) |
14 | 13 | adantl 483 |
. . . . . . . 8
β’ (((Β¬
π΄ β Fin β§ π β β) β§ π₯ β (cardβ(1...π))) β (β―βπ₯) =
(β―β(cardβ(1...π)))) |
15 | | hashcard 14262 |
. . . . . . . . . . 11
β’
((1...π) β Fin
β (β―β(cardβ(1...π))) = (β―β(1...π))) |
16 | 1, 15 | syl 17 |
. . . . . . . . . 10
β’ (π β β β
(β―β(cardβ(1...π))) = (β―β(1...π))) |
17 | | nnnn0 12427 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
18 | | hashfz1 14253 |
. . . . . . . . . . 11
β’ (π β β0
β (β―β(1...π)) = π) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
β’ (π β β β
(β―β(1...π)) =
π) |
20 | 16, 19 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β β β
(β―β(cardβ(1...π))) = π) |
21 | 20 | ad2antlr 726 |
. . . . . . . 8
β’ (((Β¬
π΄ β Fin β§ π β β) β§ π₯ β (cardβ(1...π))) β
(β―β(cardβ(1...π))) = π) |
22 | 14, 21 | eqtrd 2777 |
. . . . . . 7
β’ (((Β¬
π΄ β Fin β§ π β β) β§ π₯ β (cardβ(1...π))) β (β―βπ₯) = π) |
23 | 22 | ex 414 |
. . . . . 6
β’ ((Β¬
π΄ β Fin β§ π β β) β (π₯ β (cardβ(1...π)) β (β―βπ₯) = π)) |
24 | 12, 23 | anim12d 610 |
. . . . 5
β’ ((Β¬
π΄ β Fin β§ π β β) β ((π₯ β π΄ β§ π₯ β (cardβ(1...π))) β (π₯ β π« π΄ β§ (β―βπ₯) = π))) |
25 | 24 | eximdv 1921 |
. . . 4
β’ ((Β¬
π΄ β Fin β§ π β β) β
(βπ₯(π₯ β π΄ β§ π₯ β (cardβ(1...π))) β βπ₯(π₯ β π« π΄ β§ (β―βπ₯) = π))) |
26 | 9, 25 | mpd 15 |
. . 3
β’ ((Β¬
π΄ β Fin β§ π β β) β
βπ₯(π₯ β π« π΄ β§ (β―βπ₯) = π)) |
27 | | df-rex 3075 |
. . 3
β’
(βπ₯ β
π« π΄(β―βπ₯) = π β βπ₯(π₯ β π« π΄ β§ (β―βπ₯) = π)) |
28 | 26, 27 | sylibr 233 |
. 2
β’ ((Β¬
π΄ β Fin β§ π β β) β
βπ₯ β π«
π΄(β―βπ₯) = π) |
29 | 28 | ralrimiva 3144 |
1
β’ (Β¬
π΄ β Fin β
βπ β β
βπ₯ β π«
π΄(β―βπ₯) = π) |