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		ordom	|- Ord _om
4		ordirr	|- ( Ord _om -> -. _om e. _om )
5	3 4	ax-mp	|- -. _om e. _om
6	5	a1i	|- ( T. -> -. _om e. _om )
7		omex	|- _om e. _V
8	7	a1i	|- ( T. -> _om e. _V )
9		bj-pinftyccb	|- pinfty e. CCbar
10	9	a1i	|- ( T. -> pinfty e. CCbar )
11	2 6 8 10	bj-fvmptunsn1	|- ( T. -> ( iomnn ` _om ) = pinfty )
12	11	mptru	|- ( iomnn ` _om ) = pinfty