Metamath Proof Explorer

Theorem unblem2

Description: Lemma for unbnn . The value of the function F belongs to the unbounded set of 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 unblem2 
|- ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( z e. _om -> ( F ` z ) e. A ) )

Proof

Step Hyp Ref Expression
1 unblem.2 
 |-  F = ( rec ( ( x e. _V |-> |^| ( A \ suc x ) ) , |^| A ) |` _om )
2 fveq2 
 |-  ( z = (/) -> ( F ` z ) = ( F ` (/) ) )
3 2 eleq1d 
 |-  ( z = (/) -> ( ( F ` z ) e. A <-> ( F ` (/) ) e. A ) )
4 fveq2 
 |-  ( z = u -> ( F ` z ) = ( F ` u ) )
5 4 eleq1d 
 |-  ( z = u -> ( ( F ` z ) e. A <-> ( F ` u ) e. A ) )
6 fveq2 
 |-  ( z = suc u -> ( F ` z ) = ( F ` suc u ) )
7 6 eleq1d 
 |-  ( z = suc u -> ( ( F ` z ) e. A <-> ( F ` suc u ) e. A ) )
8 omsson 
 |-  _om C_ On
9 sstr 
 |-  ( ( A C_ _om /\ _om C_ On ) -> A C_ On )
10 8 9 mpan2 
 |-  ( A C_ _om -> A C_ On )
11 peano1 
 |-  (/) e. _om
12 eleq1 
 |-  ( w = (/) -> ( w e. v <-> (/) e. v ) )
13 12 rexbidv 
 |-  ( w = (/) -> ( E. v e. A w e. v <-> E. v e. A (/) e. v ) )
14 13 rspcv 
 |-  ( (/) e. _om -> ( A. w e. _om E. v e. A w e. v -> E. v e. A (/) e. v ) )
15 11 14 ax-mp 
 |-  ( A. w e. _om E. v e. A w e. v -> E. v e. A (/) e. v )
16 df-rex 
 |-  ( E. v e. A (/) e. v <-> E. v ( v e. A /\ (/) e. v ) )
17 15 16 sylib 
 |-  ( A. w e. _om E. v e. A w e. v -> E. v ( v e. A /\ (/) e. v ) )
18 exsimpl 
 |-  ( E. v ( v e. A /\ (/) e. v ) -> E. v v e. A )
19 17 18 syl 
 |-  ( A. w e. _om E. v e. A w e. v -> E. v v e. A )
20 n0 
 |-  ( A =/= (/) <-> E. v v e. A )
21 19 20 sylibr 
 |-  ( A. w e. _om E. v e. A w e. v -> A =/= (/) )
22 onint 
 |-  ( ( A C_ On /\ A =/= (/) ) -> |^| A e. A )
23 10 21 22 syl2an 
 |-  ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> |^| A e. A )
24 1 fveq1i 
 |-  ( F ` (/) ) = ( ( rec ( ( x e. _V |-> |^| ( A \ suc x ) ) , |^| A ) |` _om ) ` (/) )
25 fr0g 
 |-  ( |^| A e. A -> ( ( rec ( ( x e. _V |-> |^| ( A \ suc x ) ) , |^| A ) |` _om ) ` (/) ) = |^| A )
26 24 25 eqtr2id 
 |-  ( |^| A e. A -> |^| A = ( F ` (/) ) )
27 26 eleq1d 
 |-  ( |^| A e. A -> ( |^| A e. A <-> ( F ` (/) ) e. A ) )
28 27 ibi 
 |-  ( |^| A e. A -> ( F ` (/) ) e. A )
29 23 28 syl 
 |-  ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( F ` (/) ) e. A )
30 unblem1 
 |-  ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ ( F ` u ) e. A ) -> |^| ( A \ suc ( F ` u ) ) e. A )
31 suceq 
 |-  ( y = x -> suc y = suc x )
32 31 difeq2d 
 |-  ( y = x -> ( A \ suc y ) = ( A \ suc x ) )
33 32 inteqd 
 |-  ( y = x -> |^| ( A \ suc y ) = |^| ( A \ suc x ) )
34 suceq 
 |-  ( y = ( F ` u ) -> suc y = suc ( F ` u ) )
35 34 difeq2d 
 |-  ( y = ( F ` u ) -> ( A \ suc y ) = ( A \ suc ( F ` u ) ) )
36 35 inteqd 
 |-  ( y = ( F ` u ) -> |^| ( A \ suc y ) = |^| ( A \ suc ( F ` u ) ) )
37 1 33 36 frsucmpt2 
 |-  ( ( u e. _om /\ |^| ( A \ suc ( F ` u ) ) e. A ) -> ( F ` suc u ) = |^| ( A \ suc ( F ` u ) ) )
38 37 eqcomd 
 |-  ( ( u e. _om /\ |^| ( A \ suc ( F ` u ) ) e. A ) -> |^| ( A \ suc ( F ` u ) ) = ( F ` suc u ) )
39 38 eleq1d 
 |-  ( ( u e. _om /\ |^| ( A \ suc ( F ` u ) ) e. A ) -> ( |^| ( A \ suc ( F ` u ) ) e. A <-> ( F ` suc u ) e. A ) )
40 39 ex 
 |-  ( u e. _om -> ( |^| ( A \ suc ( F ` u ) ) e. A -> ( |^| ( A \ suc ( F ` u ) ) e. A <-> ( F ` suc u ) e. A ) ) )
41 40 ibd 
 |-  ( u e. _om -> ( |^| ( A \ suc ( F ` u ) ) e. A -> ( F ` suc u ) e. A ) )
42 30 41 syl5 
 |-  ( u e. _om -> ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ ( F ` u ) e. A ) -> ( F ` suc u ) e. A ) )
43 42 expd 
 |-  ( u e. _om -> ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( ( F ` u ) e. A -> ( F ` suc u ) e. A ) ) )
44 3 5 7 29 43 finds2 
 |-  ( z e. _om -> ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( F ` z ) e. A ) )
45 44 com12 
 |-  ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( z e. _om -> ( F ` z ) e. A ) )