Theorem unblem4

Description: Lemma for unbnn . The function F maps the set of natural numbers one-to-one to the set of unbounded natural numbers A . (Contributed by NM, 3-Dec-2003)

	Ref	Expression
Hypothesis	unblem.2	|- F = ( rec ( ( x e. _V |-> |^| ( A \ suc x ) ) , |^| A ) |` _om )
Assertion	unblem4	|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> F : _om -1-1-> A )

Proof

Step	Hyp	Ref	Expression
1		unblem.2	|- F = ( rec ( ( x e. _V |-> |^| ( A \ suc x ) ) , |^| A ) |` _om )
2		omsson	|- _om C_ On
3		sstr	|- ( ( A C_ _om /\ _om C_ On ) -> A C_ On )
4	2 3	mpan2	|- ( A C_ _om -> A C_ On )
5	4	adantr	|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> A C_ On )
6		frfnom	|- ( rec ( ( x e. _V |-> |^| ( A \ suc x ) ) , |^| A ) |` _om ) Fn _om
7	1	fneq1i	|- ( F Fn _om <-> ( rec ( ( x e. _V |-> |^| ( A \ suc x ) ) , |^| A ) |` _om ) Fn _om )
8	6 7	mpbir	|- F Fn _om
9	1	unblem2	|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( z e. _om -> ( F ` z ) e. A ) )
10	9	ralrimiv	|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> A. z e. _om ( F ` z ) e. A )
11		ffnfv	|- ( F : _om --> A <-> ( F Fn _om /\ A. z e. _om ( F ` z ) e. A ) )
12	11	biimpri	|- ( ( F Fn _om /\ A. z e. _om ( F ` z ) e. A ) -> F : _om --> A )
13	8 10 12	sylancr	|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> F : _om --> A )
14	1	unblem3	|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( z e. _om -> ( F ` z ) e. ( F ` suc z ) ) )
15	14	ralrimiv	|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> A. z e. _om ( F ` z ) e. ( F ` suc z ) )
16		omsmo	|- ( ( ( A C_ On /\ F : _om --> A ) /\ A. z e. _om ( F ` z ) e. ( F ` suc z ) ) -> F : _om -1-1-> A )
17	5 13 15 16	syl21anc	|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> F : _om -1-1-> A )