Metamath Proof Explorer

Theorem relexpss1d

Description: The relational power of a subset is a subset. (Contributed by RP, 17-Jun-2020)

Ref Expression
Hypotheses relexpss1d.a 
|- ( ph -> A C_ B )
relexpss1d.b 
|- ( ph -> B e. _V )
relexpss1d.n 
|- ( ph -> N e. NN0 )
Assertion relexpss1d 
|- ( ph -> ( A ^r N ) C_ ( B ^r N ) )

Proof

Step Hyp Ref Expression
1 relexpss1d.a 
 |-  ( ph -> A C_ B )
2 relexpss1d.b 
 |-  ( ph -> B e. _V )
3 relexpss1d.n 
 |-  ( ph -> N e. NN0 )
4 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
5 3 4 sylib 
 |-  ( ph -> ( N e. NN \/ N = 0 ) )
6 oveq2 
 |-  ( x = 1 -> ( A ^r x ) = ( A ^r 1 ) )
7 oveq2 
 |-  ( x = 1 -> ( B ^r x ) = ( B ^r 1 ) )
8 6 7 sseq12d 
 |-  ( x = 1 -> ( ( A ^r x ) C_ ( B ^r x ) <-> ( A ^r 1 ) C_ ( B ^r 1 ) ) )
9 8 imbi2d 
 |-  ( x = 1 -> ( ( ph -> ( A ^r x ) C_ ( B ^r x ) ) <-> ( ph -> ( A ^r 1 ) C_ ( B ^r 1 ) ) ) )
10 oveq2 
 |-  ( x = y -> ( A ^r x ) = ( A ^r y ) )
11 oveq2 
 |-  ( x = y -> ( B ^r x ) = ( B ^r y ) )
12 10 11 sseq12d 
 |-  ( x = y -> ( ( A ^r x ) C_ ( B ^r x ) <-> ( A ^r y ) C_ ( B ^r y ) ) )
13 12 imbi2d 
 |-  ( x = y -> ( ( ph -> ( A ^r x ) C_ ( B ^r x ) ) <-> ( ph -> ( A ^r y ) C_ ( B ^r y ) ) ) )
14 oveq2 
 |-  ( x = ( y + 1 ) -> ( A ^r x ) = ( A ^r ( y + 1 ) ) )
15 oveq2 
 |-  ( x = ( y + 1 ) -> ( B ^r x ) = ( B ^r ( y + 1 ) ) )
16 14 15 sseq12d 
 |-  ( x = ( y + 1 ) -> ( ( A ^r x ) C_ ( B ^r x ) <-> ( A ^r ( y + 1 ) ) C_ ( B ^r ( y + 1 ) ) ) )
17 16 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ph -> ( A ^r x ) C_ ( B ^r x ) ) <-> ( ph -> ( A ^r ( y + 1 ) ) C_ ( B ^r ( y + 1 ) ) ) ) )
18 oveq2 
 |-  ( x = N -> ( A ^r x ) = ( A ^r N ) )
19 oveq2 
 |-  ( x = N -> ( B ^r x ) = ( B ^r N ) )
20 18 19 sseq12d 
 |-  ( x = N -> ( ( A ^r x ) C_ ( B ^r x ) <-> ( A ^r N ) C_ ( B ^r N ) ) )
21 20 imbi2d 
 |-  ( x = N -> ( ( ph -> ( A ^r x ) C_ ( B ^r x ) ) <-> ( ph -> ( A ^r N ) C_ ( B ^r N ) ) ) )
22 2 1 ssexd 
 |-  ( ph -> A e. _V )
23 22 relexp1d 
 |-  ( ph -> ( A ^r 1 ) = A )
24 2 relexp1d 
 |-  ( ph -> ( B ^r 1 ) = B )
25 1 23 24 3sstr4d 
 |-  ( ph -> ( A ^r 1 ) C_ ( B ^r 1 ) )
26 simp3 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> ( A ^r y ) C_ ( B ^r y ) )
27 1 3ad2ant2 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> A C_ B )
28 26 27 coss12d 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> ( ( A ^r y ) o. A ) C_ ( ( B ^r y ) o. B ) )
29 22 3ad2ant2 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> A e. _V )
30 simp1 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> y e. NN )
31 relexpsucnnr 
 |-  ( ( A e. _V /\ y e. NN ) -> ( A ^r ( y + 1 ) ) = ( ( A ^r y ) o. A ) )
32 29 30 31 syl2anc 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> ( A ^r ( y + 1 ) ) = ( ( A ^r y ) o. A ) )
33 2 3ad2ant2 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> B e. _V )
34 relexpsucnnr 
 |-  ( ( B e. _V /\ y e. NN ) -> ( B ^r ( y + 1 ) ) = ( ( B ^r y ) o. B ) )
35 33 30 34 syl2anc 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> ( B ^r ( y + 1 ) ) = ( ( B ^r y ) o. B ) )
36 28 32 35 3sstr4d 
 |-  ( ( y e. NN /\ ph /\ ( A ^r y ) C_ ( B ^r y ) ) -> ( A ^r ( y + 1 ) ) C_ ( B ^r ( y + 1 ) ) )
37 36 3exp 
 |-  ( y e. NN -> ( ph -> ( ( A ^r y ) C_ ( B ^r y ) -> ( A ^r ( y + 1 ) ) C_ ( B ^r ( y + 1 ) ) ) ) )
38 37 a2d 
 |-  ( y e. NN -> ( ( ph -> ( A ^r y ) C_ ( B ^r y ) ) -> ( ph -> ( A ^r ( y + 1 ) ) C_ ( B ^r ( y + 1 ) ) ) ) )
39 9 13 17 21 25 38 nnind 
 |-  ( N e. NN -> ( ph -> ( A ^r N ) C_ ( B ^r N ) ) )
40 simpr 
 |-  ( ( N = 0 /\ ph ) -> ph )
41 dmss 
 |-  ( A C_ B -> dom A C_ dom B )
42 rnss 
 |-  ( A C_ B -> ran A C_ ran B )
43 41 42 jca 
 |-  ( A C_ B -> ( dom A C_ dom B /\ ran A C_ ran B ) )
44 unss12 
 |-  ( ( dom A C_ dom B /\ ran A C_ ran B ) -> ( dom A u. ran A ) C_ ( dom B u. ran B ) )
45 1 43 44 3syl 
 |-  ( ph -> ( dom A u. ran A ) C_ ( dom B u. ran B ) )
46 ssres2 
 |-  ( ( dom A u. ran A ) C_ ( dom B u. ran B ) -> ( _I |` ( dom A u. ran A ) ) C_ ( _I |` ( dom B u. ran B ) ) )
47 40 45 46 3syl 
 |-  ( ( N = 0 /\ ph ) -> ( _I |` ( dom A u. ran A ) ) C_ ( _I |` ( dom B u. ran B ) ) )
48 simpl 
 |-  ( ( N = 0 /\ ph ) -> N = 0 )
49 48 oveq2d 
 |-  ( ( N = 0 /\ ph ) -> ( A ^r N ) = ( A ^r 0 ) )
50 relexp0g 
 |-  ( A e. _V -> ( A ^r 0 ) = ( _I |` ( dom A u. ran A ) ) )
51 40 22 50 3syl 
 |-  ( ( N = 0 /\ ph ) -> ( A ^r 0 ) = ( _I |` ( dom A u. ran A ) ) )
52 49 51 eqtrd 
 |-  ( ( N = 0 /\ ph ) -> ( A ^r N ) = ( _I |` ( dom A u. ran A ) ) )
53 48 oveq2d 
 |-  ( ( N = 0 /\ ph ) -> ( B ^r N ) = ( B ^r 0 ) )
54 relexp0g 
 |-  ( B e. _V -> ( B ^r 0 ) = ( _I |` ( dom B u. ran B ) ) )
55 40 2 54 3syl 
 |-  ( ( N = 0 /\ ph ) -> ( B ^r 0 ) = ( _I |` ( dom B u. ran B ) ) )
56 53 55 eqtrd 
 |-  ( ( N = 0 /\ ph ) -> ( B ^r N ) = ( _I |` ( dom B u. ran B ) ) )
57 47 52 56 3sstr4d 
 |-  ( ( N = 0 /\ ph ) -> ( A ^r N ) C_ ( B ^r N ) )
58 57 ex 
 |-  ( N = 0 -> ( ph -> ( A ^r N ) C_ ( B ^r N ) ) )
59 39 58 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ph -> ( A ^r N ) C_ ( B ^r N ) ) )
60 5 59 mpcom 
 |-  ( ph -> ( A ^r N ) C_ ( B ^r N ) )