Theorem bj-iomnnom

Description: The canonical bijection from (om u. { om } ) onto ( NN0 u. { pinfty } ) maps _om to pinfty . (Contributed by BJ, 18-Feb-2023)

	Ref	Expression
Assertion	bj-iomnnom	|- ( iomnn ` _om ) = pinfty

Proof

Step	Hyp	Ref	Expression
1		df-bj-iomnn	|- iomnn = ( ( n e. _om |-> <. [ <. { r e. Q. | r . } , 1P >. ] ~R , 0R >. ) u. { <. _om , pinfty >. } )
2	1	a1i	|- ( T. -> iomnn = ( ( n e. _om |-> <. [ <. { r e. Q. | r . } , 1P >. ] ~R , 0R >. ) u. { <. _om , pinfty >. } ) )
3		elirr	|- -. _om e. _om
4	3	a1i	|- ( T. -> -. _om e. _om )
5		omex	|- _om e. _V
6	5	a1i	|- ( T. -> _om e. _V )
7		bj-pinftyccb	|- pinfty e. CCbar
8	7	a1i	|- ( T. -> pinfty e. CCbar )
9	2 4 6 8	bj-fvmptunsn1	|- ( T. -> ( iomnn ` _om ) = pinfty )
10	9	mptru	|- ( iomnn ` _om ) = pinfty