Metamath Proof Explorer

Theorem trclimalb2

Description: Lower bound for image under a transitive closure. (Contributed by RP, 1-Jul-2020)

Ref Expression
Assertion trclimalb2 
|- ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( t+ ` R ) " A ) C_ B )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( R e. V -> R e. _V )
2 1 adantr 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> R e. _V )
3 oveq1 
 |-  ( r = R -> ( r ^r k ) = ( R ^r k ) )
4 3 iuneq2d 
 |-  ( r = R -> U_ k e. NN ( r ^r k ) = U_ k e. NN ( R ^r k ) )
5 dftrcl3 
 |-  t+ = ( r e. _V |-> U_ k e. NN ( r ^r k ) )
6 nnex 
 |-  NN e. _V
7 ovex 
 |-  ( R ^r k ) e. _V
8 6 7 iunex 
 |-  U_ k e. NN ( R ^r k ) e. _V
9 4 5 8 fvmpt 
 |-  ( R e. _V -> ( t+ ` R ) = U_ k e. NN ( R ^r k ) )
10 9 imaeq1d 
 |-  ( R e. _V -> ( ( t+ ` R ) " A ) = ( U_ k e. NN ( R ^r k ) " A ) )
11 imaiun1 
 |-  ( U_ k e. NN ( R ^r k ) " A ) = U_ k e. NN ( ( R ^r k ) " A )
12 10 11 eqtrdi 
 |-  ( R e. _V -> ( ( t+ ` R ) " A ) = U_ k e. NN ( ( R ^r k ) " A ) )
13 2 12 syl 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( t+ ` R ) " A ) = U_ k e. NN ( ( R ^r k ) " A ) )
14 oveq2 
 |-  ( x = 1 -> ( R ^r x ) = ( R ^r 1 ) )
15 14 imaeq1d 
 |-  ( x = 1 -> ( ( R ^r x ) " A ) = ( ( R ^r 1 ) " A ) )
16 15 sseq1d 
 |-  ( x = 1 -> ( ( ( R ^r x ) " A ) C_ B <-> ( ( R ^r 1 ) " A ) C_ B ) )
17 16 imbi2d 
 |-  ( x = 1 -> ( ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r x ) " A ) C_ B ) <-> ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r 1 ) " A ) C_ B ) ) )
18 oveq2 
 |-  ( x = y -> ( R ^r x ) = ( R ^r y ) )
19 18 imaeq1d 
 |-  ( x = y -> ( ( R ^r x ) " A ) = ( ( R ^r y ) " A ) )
20 19 sseq1d 
 |-  ( x = y -> ( ( ( R ^r x ) " A ) C_ B <-> ( ( R ^r y ) " A ) C_ B ) )
21 20 imbi2d 
 |-  ( x = y -> ( ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r x ) " A ) C_ B ) <-> ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r y ) " A ) C_ B ) ) )
22 oveq2 
 |-  ( x = ( y + 1 ) -> ( R ^r x ) = ( R ^r ( y + 1 ) ) )
23 22 imaeq1d 
 |-  ( x = ( y + 1 ) -> ( ( R ^r x ) " A ) = ( ( R ^r ( y + 1 ) ) " A ) )
24 23 sseq1d 
 |-  ( x = ( y + 1 ) -> ( ( ( R ^r x ) " A ) C_ B <-> ( ( R ^r ( y + 1 ) ) " A ) C_ B ) )
25 24 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r x ) " A ) C_ B ) <-> ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r ( y + 1 ) ) " A ) C_ B ) ) )
26 oveq2 
 |-  ( x = k -> ( R ^r x ) = ( R ^r k ) )
27 26 imaeq1d 
 |-  ( x = k -> ( ( R ^r x ) " A ) = ( ( R ^r k ) " A ) )
28 27 sseq1d 
 |-  ( x = k -> ( ( ( R ^r x ) " A ) C_ B <-> ( ( R ^r k ) " A ) C_ B ) )
29 28 imbi2d 
 |-  ( x = k -> ( ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r x ) " A ) C_ B ) <-> ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r k ) " A ) C_ B ) ) )
30 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
31 30 imaeq1d 
 |-  ( R e. V -> ( ( R ^r 1 ) " A ) = ( R " A ) )
32 31 adantr 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r 1 ) " A ) = ( R " A ) )
33 ssun1 
 |-  A C_ ( A u. B )
34 imass2 
 |-  ( A C_ ( A u. B ) -> ( R " A ) C_ ( R " ( A u. B ) ) )
35 33 34 mp1i 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( R " A ) C_ ( R " ( A u. B ) ) )
36 simpr 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( R " ( A u. B ) ) C_ B )
37 35 36 sstrd 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( R " A ) C_ B )
38 32 37 eqsstrd 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r 1 ) " A ) C_ B )
39 simp2l 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> R e. V )
40 simp1 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> y e. NN )
41 relexpsucnnl 
 |-  ( ( R e. V /\ y e. NN ) -> ( R ^r ( y + 1 ) ) = ( R o. ( R ^r y ) ) )
42 41 imaeq1d 
 |-  ( ( R e. V /\ y e. NN ) -> ( ( R ^r ( y + 1 ) ) " A ) = ( ( R o. ( R ^r y ) ) " A ) )
43 imaco 
 |-  ( ( R o. ( R ^r y ) ) " A ) = ( R " ( ( R ^r y ) " A ) )
44 42 43 eqtrdi 
 |-  ( ( R e. V /\ y e. NN ) -> ( ( R ^r ( y + 1 ) ) " A ) = ( R " ( ( R ^r y ) " A ) ) )
45 39 40 44 syl2anc 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> ( ( R ^r ( y + 1 ) ) " A ) = ( R " ( ( R ^r y ) " A ) ) )
46 imass2 
 |-  ( ( ( R ^r y ) " A ) C_ B -> ( R " ( ( R ^r y ) " A ) ) C_ ( R " B ) )
47 46 3ad2ant3 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> ( R " ( ( R ^r y ) " A ) ) C_ ( R " B ) )
48 ssun2 
 |-  B C_ ( A u. B )
49 imass2 
 |-  ( B C_ ( A u. B ) -> ( R " B ) C_ ( R " ( A u. B ) ) )
50 48 49 mp1i 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> ( R " B ) C_ ( R " ( A u. B ) ) )
51 simp2r 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> ( R " ( A u. B ) ) C_ B )
52 50 51 sstrd 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> ( R " B ) C_ B )
53 47 52 sstrd 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> ( R " ( ( R ^r y ) " A ) ) C_ B )
54 45 53 eqsstrd 
 |-  ( ( y e. NN /\ ( R e. V /\ ( R " ( A u. B ) ) C_ B ) /\ ( ( R ^r y ) " A ) C_ B ) -> ( ( R ^r ( y + 1 ) ) " A ) C_ B )
55 54 3exp 
 |-  ( y e. NN -> ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( ( R ^r y ) " A ) C_ B -> ( ( R ^r ( y + 1 ) ) " A ) C_ B ) ) )
56 55 a2d 
 |-  ( y e. NN -> ( ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r y ) " A ) C_ B ) -> ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r ( y + 1 ) ) " A ) C_ B ) ) )
57 17 21 25 29 38 56 nnind 
 |-  ( k e. NN -> ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( R ^r k ) " A ) C_ B ) )
58 57 com12 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( k e. NN -> ( ( R ^r k ) " A ) C_ B ) )
59 58 ralrimiv 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> A. k e. NN ( ( R ^r k ) " A ) C_ B )
60 iunss 
 |-  ( U_ k e. NN ( ( R ^r k ) " A ) C_ B <-> A. k e. NN ( ( R ^r k ) " A ) C_ B )
61 59 60 sylibr 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> U_ k e. NN ( ( R ^r k ) " A ) C_ B )
62 13 61 eqsstrd 
 |-  ( ( R e. V /\ ( R " ( A u. B ) ) C_ B ) -> ( ( t+ ` R ) " A ) C_ B )