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 +∞e : onto ∞N

Proof

Step Hyp Ref Expression
1 opex { R 1 st x 𝑹 V
2 df-bj-inftyexpitau +∞e = x { R 1 st x 𝑹
3 1 2 fnmpti +∞e Fn
4 dffn4 +∞e Fn +∞e : onto ran +∞e
5 3 4 mpbi +∞e : onto ran +∞e
6 df-bj-ccinftyN ∞N = ran +∞e
7 6 eqcomi ran +∞e = ∞N
8 foeq3 ran +∞e = ∞N +∞e : onto ran +∞e +∞e : onto ∞N
9 7 8 ax-mp +∞e : onto ran +∞e +∞e : onto ∞N
10 5 9 mpbi +∞e : onto ∞N