Metamath Proof Explorer


Theorem ppif

Description: Domain and range of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion ppif π_:0

Proof

Step Hyp Ref Expression
1 df-ppi π_=x0x
2 ppifi x0xFin
3 hashcl 0xFin0x0
4 2 3 syl x0x0
5 1 4 fmpti π_:0