This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )