Metamath Proof Explorer

Theorem incssnn0

Description: Transitivity induction of subsets, lemma for nacsfix . (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Assertion incssnn0 
|- ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 /\ B e. ( ZZ>= ` A ) ) -> ( F ` A ) C_ ( F ` B ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = A -> ( F ` a ) = ( F ` A ) )
2 1 sseq2d 
 |-  ( a = A -> ( ( F ` A ) C_ ( F ` a ) <-> ( F ` A ) C_ ( F ` A ) ) )
3 2 imbi2d 
 |-  ( a = A -> ( ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` a ) ) <-> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` A ) ) ) )
4 fveq2 
 |-  ( a = b -> ( F ` a ) = ( F ` b ) )
5 4 sseq2d 
 |-  ( a = b -> ( ( F ` A ) C_ ( F ` a ) <-> ( F ` A ) C_ ( F ` b ) ) )
6 5 imbi2d 
 |-  ( a = b -> ( ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` a ) ) <-> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` b ) ) ) )
7 fveq2 
 |-  ( a = ( b + 1 ) -> ( F ` a ) = ( F ` ( b + 1 ) ) )
8 7 sseq2d 
 |-  ( a = ( b + 1 ) -> ( ( F ` A ) C_ ( F ` a ) <-> ( F ` A ) C_ ( F ` ( b + 1 ) ) ) )
9 8 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` a ) ) <-> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` ( b + 1 ) ) ) ) )
10 fveq2 
 |-  ( a = B -> ( F ` a ) = ( F ` B ) )
11 10 sseq2d 
 |-  ( a = B -> ( ( F ` A ) C_ ( F ` a ) <-> ( F ` A ) C_ ( F ` B ) ) )
12 11 imbi2d 
 |-  ( a = B -> ( ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` a ) ) <-> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` B ) ) ) )
13 ssid 
 |-  ( F ` A ) C_ ( F ` A )
14 13 2a1i 
 |-  ( A e. ZZ -> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` A ) ) )
15 eluznn0 
 |-  ( ( A e. NN0 /\ b e. ( ZZ>= ` A ) ) -> b e. NN0 )
16 15 ancoms 
 |-  ( ( b e. ( ZZ>= ` A ) /\ A e. NN0 ) -> b e. NN0 )
17 fveq2 
 |-  ( x = b -> ( F ` x ) = ( F ` b ) )
18 fvoveq1 
 |-  ( x = b -> ( F ` ( x + 1 ) ) = ( F ` ( b + 1 ) ) )
19 17 18 sseq12d 
 |-  ( x = b -> ( ( F ` x ) C_ ( F ` ( x + 1 ) ) <-> ( F ` b ) C_ ( F ` ( b + 1 ) ) ) )
20 19 rspcv 
 |-  ( b e. NN0 -> ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) -> ( F ` b ) C_ ( F ` ( b + 1 ) ) ) )
21 16 20 syl 
 |-  ( ( b e. ( ZZ>= ` A ) /\ A e. NN0 ) -> ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) -> ( F ` b ) C_ ( F ` ( b + 1 ) ) ) )
22 21 expimpd 
 |-  ( b e. ( ZZ>= ` A ) -> ( ( A e. NN0 /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> ( F ` b ) C_ ( F ` ( b + 1 ) ) ) )
23 22 ancomsd 
 |-  ( b e. ( ZZ>= ` A ) -> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` b ) C_ ( F ` ( b + 1 ) ) ) )
24 sstr2 
 |-  ( ( F ` A ) C_ ( F ` b ) -> ( ( F ` b ) C_ ( F ` ( b + 1 ) ) -> ( F ` A ) C_ ( F ` ( b + 1 ) ) ) )
25 24 com12 
 |-  ( ( F ` b ) C_ ( F ` ( b + 1 ) ) -> ( ( F ` A ) C_ ( F ` b ) -> ( F ` A ) C_ ( F ` ( b + 1 ) ) ) )
26 23 25 syl6 
 |-  ( b e. ( ZZ>= ` A ) -> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( ( F ` A ) C_ ( F ` b ) -> ( F ` A ) C_ ( F ` ( b + 1 ) ) ) ) )
27 26 a2d 
 |-  ( b e. ( ZZ>= ` A ) -> ( ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` b ) ) -> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` ( b + 1 ) ) ) ) )
28 3 6 9 12 14 27 uzind4 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( F ` A ) C_ ( F ` B ) ) )
29 28 com12 
 |-  ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 ) -> ( B e. ( ZZ>= ` A ) -> ( F ` A ) C_ ( F ` B ) ) )
30 29 3impia 
 |-  ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 /\ B e. ( ZZ>= ` A ) ) -> ( F ` A ) C_ ( F ` B ) )