Metamath Proof Explorer

Theorem bj-inftyexpitaufo

Description: The function inftyexpitau written as a surjection with domain and range. (Contributed by BJ, 4-Feb-2023)

Ref Expression
Assertion bj-inftyexpitaufo 
|- inftyexpitau : RR -onto-> CCinftyN

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. ( {R ` ( 1st ` x ) ) , { R. } >. e. _V
2 df-bj-inftyexpitau 
 |-  inftyexpitau = ( x e. RR |-> <. ( {R ` ( 1st ` x ) ) , { R. } >. )
3 1 2 fnmpti 
 |-  inftyexpitau Fn RR
4 dffn4 
 |-  ( inftyexpitau Fn RR <-> inftyexpitau : RR -onto-> ran inftyexpitau )
5 3 4 mpbi 
 |-  inftyexpitau : RR -onto-> ran inftyexpitau
6 df-bj-ccinftyN 
 |-  CCinftyN = ran inftyexpitau
7 6 eqcomi 
 |-  ran inftyexpitau = CCinftyN
8 foeq3 
 |-  ( ran inftyexpitau = CCinftyN -> ( inftyexpitau : RR -onto-> ran inftyexpitau <-> inftyexpitau : RR -onto-> CCinftyN ) )
9 7 8 ax-mp 
 |-  ( inftyexpitau : RR -onto-> ran inftyexpitau <-> inftyexpitau : RR -onto-> CCinftyN )
10 5 9 mpbi 
 |-  inftyexpitau : RR -onto-> CCinftyN