Metamath Proof Explorer

Theorem unblem3

Description: Lemma for unbnn . The value of the function F is less than its value at a successor. (Contributed by NM, 3-Dec-2003)

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

Proof

Step Hyp Ref Expression
1 unblem.2 
 |-  F = ( rec ( ( x e. _V |-> |^| ( A \ suc x ) ) , |^| A ) |` _om )
2 1 unblem2 
 |-  ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( z e. _om -> ( F ` z ) e. A ) )
3 2 imp 
 |-  ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ z e. _om ) -> ( F ` z ) e. A )
4 omsson 
 |-  _om C_ On
5 sstr 
 |-  ( ( A C_ _om /\ _om C_ On ) -> A C_ On )
6 4 5 mpan2 
 |-  ( A C_ _om -> A C_ On )
7 ssel 
 |-  ( A C_ On -> ( ( F ` z ) e. A -> ( F ` z ) e. On ) )
8 7 anc2li 
 |-  ( A C_ On -> ( ( F ` z ) e. A -> ( A C_ On /\ ( F ` z ) e. On ) ) )
9 6 8 syl 
 |-  ( A C_ _om -> ( ( F ` z ) e. A -> ( A C_ On /\ ( F ` z ) e. On ) ) )
10 9 ad2antrr 
 |-  ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ z e. _om ) -> ( ( F ` z ) e. A -> ( A C_ On /\ ( F ` z ) e. On ) ) )
11 3 10 mpd 
 |-  ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ z e. _om ) -> ( A C_ On /\ ( F ` z ) e. On ) )
12 onmindif 
 |-  ( ( A C_ On /\ ( F ` z ) e. On ) -> ( F ` z ) e. |^| ( A \ suc ( F ` z ) ) )
13 11 12 syl 
 |-  ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ z e. _om ) -> ( F ` z ) e. |^| ( A \ suc ( F ` z ) ) )
14 unblem1 
 |-  ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ ( F ` z ) e. A ) -> |^| ( A \ suc ( F ` z ) ) e. A )
15 14 ex 
 |-  ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( ( F ` z ) e. A -> |^| ( A \ suc ( F ` z ) ) e. A ) )
16 2 15 syld 
 |-  ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( z e. _om -> |^| ( A \ suc ( F ` z ) ) e. A ) )
17 suceq 
 |-  ( y = x -> suc y = suc x )
18 17 difeq2d 
 |-  ( y = x -> ( A \ suc y ) = ( A \ suc x ) )
19 18 inteqd 
 |-  ( y = x -> |^| ( A \ suc y ) = |^| ( A \ suc x ) )
20 suceq 
 |-  ( y = ( F ` z ) -> suc y = suc ( F ` z ) )
21 20 difeq2d 
 |-  ( y = ( F ` z ) -> ( A \ suc y ) = ( A \ suc ( F ` z ) ) )
22 21 inteqd 
 |-  ( y = ( F ` z ) -> |^| ( A \ suc y ) = |^| ( A \ suc ( F ` z ) ) )
23 1 19 22 frsucmpt2 
 |-  ( ( z e. _om /\ |^| ( A \ suc ( F ` z ) ) e. A ) -> ( F ` suc z ) = |^| ( A \ suc ( F ` z ) ) )
24 23 ex 
 |-  ( z e. _om -> ( |^| ( A \ suc ( F ` z ) ) e. A -> ( F ` suc z ) = |^| ( A \ suc ( F ` z ) ) ) )
25 16 24 sylcom 
 |-  ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( z e. _om -> ( F ` suc z ) = |^| ( A \ suc ( F ` z ) ) ) )
26 25 imp 
 |-  ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ z e. _om ) -> ( F ` suc z ) = |^| ( A \ suc ( F ` z ) ) )
27 13 26 eleqtrrd 
 |-  ( ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) /\ z e. _om ) -> ( F ` z ) e. ( F ` suc z ) )
28 27 ex 
 |-  ( ( A C_ _om /\ A. w e. _om E. v e. A w e. v ) -> ( z e. _om -> ( F ` z ) e. ( F ` suc z ) ) )