Theorem relexpaddss 36223

Description: The composition of two powers of a relation is a subset of the relation raised to the sum of those exponents. This is equality where R is a relation as shown by relexpaddd 13056 or when the sum of the powers isn't 1 as shown by relexpaddg 13055. (Contributed by RP, 3-Jun-2020.)

Assertion

Ref	Expression
relexpaddss	|- ( ( N e. NN0 /\ M e. NN0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )

Proof of Theorem relexpaddss

Step	Hyp	Ref	Expression
1		elnn0 10817	. . 3 |- ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
2		elnn0 10817	. . . . . 6 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
3	2	biimpi 197	. . . . 5 |- ( N e. NN0 -> ( N e. NN \/ N = 0 ) )
4		relexpaddnn 13053	. . . . . . . 8 |- ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
5		eqimss 3454	. . . . . . . 8 |- ( ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
6	4, 5	syl 17	. . . . . . 7 |- ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
7	6	3exp 1204	. . . . . 6 |- ( N e. NN -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
8		elnn1uz2 11181	. . . . . . 7 |- ( M e. NN <-> ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) )
9		relco 5290	. . . . . . . . . . . . . 14 |- Rel ( ( _I |` ( dom R u. ran R ) ) o. R )
10		dfrel2 5243	. . . . . . . . . . . . . . 15 |- ( Rel ( ( _I |` ( dom R u. ran R ) ) o. R ) <-> `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( ( _I |` ( dom R u. ran R ) ) o. R ) )
11	10	biimpi 197	. . . . . . . . . . . . . 14 |- ( Rel ( ( _I |` ( dom R u. ran R ) ) o. R ) -> `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( ( _I |` ( dom R u. ran R ) ) o. R ) )
12	9, 11	ax-mp 5	. . . . . . . . . . . . 13 |- `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( ( _I |` ( dom R u. ran R ) ) o. R )
13		cnvco 4977	. . . . . . . . . . . . . . . . 17 |- `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R o. `' ( _I |` ( dom R u. ran R ) ) )
14		cnvresid 5609	. . . . . . . . . . . . . . . . . 18 |- `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom R u. ran R ) )
15	14	coeq2i 4952	. . . . . . . . . . . . . . . . 17 |- ( `' R o. `' ( _I |` ( dom R u. ran R ) ) ) = ( `' R o. ( _I |` ( dom R u. ran R ) ) )
16		coires1 5310	. . . . . . . . . . . . . . . . 17 |- ( `' R o. ( _I |` ( dom R u. ran R ) ) ) = ( `' R |` ( dom R u. ran R ) )
17	13, 15, 16	3eqtri 2449	. . . . . . . . . . . . . . . 16 |- `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R |` ( dom R u. ran R ) )
18		eqimss 3454	. . . . . . . . . . . . . . . 16 |- ( `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R |` ( dom R u. ran R ) ) -> `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ ( `' R |` ( dom R u. ran R ) ) )
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15 |- `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ ( `' R |` ( dom R u. ran R ) )
20		cnvss 4964	. . . . . . . . . . . . . . 15 |- ( `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ ( `' R |` ( dom R u. ran R ) ) -> `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' ( `' R |` ( dom R u. ran R ) ) )
21	19, 20	ax-mp 5	. . . . . . . . . . . . . 14 |- `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' ( `' R |` ( dom R u. ran R ) )
22		resss 5085	. . . . . . . . . . . . . . 15 |- ( `' R |` ( dom R u. ran R ) ) C_ `' R
23		cnvss 4964	. . . . . . . . . . . . . . 15 |- ( ( `' R |` ( dom R u. ran R ) ) C_ `' R -> `' ( `' R |` ( dom R u. ran R ) ) C_ `' `' R )
24	22, 23	ax-mp 5	. . . . . . . . . . . . . 14 |- `' ( `' R |` ( dom R u. ran R ) ) C_ `' `' R
25	21, 24	sstri 3411	. . . . . . . . . . . . 13 |- `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' `' R
26	12, 25	eqsstr3i 3433	. . . . . . . . . . . 12 |- ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' `' R
27		cnvcnvss 5247	. . . . . . . . . . . 12 |- `' `' R C_ R
28	26, 27	sstri 3411	. . . . . . . . . . 11 |- ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ R
29	28	a1i 11	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ R )
30		simp1 1005	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> N = 0 )
31	30	oveq2d 6260	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
32		relexp0g 13024	. . . . . . . . . . . . 13 |- ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
33	32	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
34	31, 33	eqtrd 2457	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
35		simp2 1006	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> M = 1 )
36	35	oveq2d 6260	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r M ) = ( R ^r 1 ) )
37		relexp1g 13028	. . . . . . . . . . . . 13 |- ( R e. V -> ( R ^r 1 ) = R )
38	37	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r 1 ) = R )
39	36, 38	eqtrd 2457	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r M ) = R )
40	34, 39	coeq12d 4956	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( _I |` ( dom R u. ran R ) ) o. R ) )
41	30, 35	oveq12d 6262	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( N + M ) = ( 0 + 1 ) )
42		1cnd 9605	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> 1 e. CC )
43	42	addid2d 9780	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( 0 + 1 ) = 1 )
44	41, 43	eqtrd 2457	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( N + M ) = 1 )
45	44	oveq2d 6260	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
46	45, 38	eqtrd 2457	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
47	29, 40, 46	3sstr4d 3445	. . . . . . . . 9 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
48	47	3exp 1204	. . . . . . . 8 |- ( N = 0 -> ( M = 1 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
49		coires1 5310	. . . . . . . . . . . . . 14 |- ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( `' R ^r M ) |` ( dom R u. ran R ) )
50		simp2 1006	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. ( ZZ>= ` 2 ) )
51		cnvexg 6692	. . . . . . . . . . . . . . . . 17 |- ( R e. V -> `' R e. _V )
52	51	3ad2ant3 1028	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' R e. _V )
53		relexpuzrel 13054	. . . . . . . . . . . . . . . 16 |- ( ( M e. ( ZZ>= ` 2 ) /\ `' R e. _V ) -> Rel ( `' R ^r M ) )
54	50, 52, 53	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( `' R ^r M ) )
55		eluz2nn 11143	. . . . . . . . . . . . . . . . . 18 |- ( M e. ( ZZ>= ` 2 ) -> M e. NN )
56	50, 55	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN )
57		relexpnndm 13043	. . . . . . . . . . . . . . . . 17 |- ( ( M e. NN /\ `' R e. _V ) -> dom ( `' R ^r M ) C_ dom `' R )
58	56, 52, 57	syl2anc 665	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ dom `' R )
59		df-rn 4802	. . . . . . . . . . . . . . . . 17 |- ran R = dom `' R
60		ssun2 3568	. . . . . . . . . . . . . . . . 17 |- ran R C_ ( dom R u. ran R )
61	59, 60	eqsstr3i 3433	. . . . . . . . . . . . . . . 16 |- dom `' R C_ ( dom R u. ran R )
62	58, 61	syl6ss 3414	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ ( dom R u. ran R ) )
63		relssres 5099	. . . . . . . . . . . . . . 15 |- ( ( Rel ( `' R ^r M ) /\ dom ( `' R ^r M ) C_ ( dom R u. ran R ) ) -> ( ( `' R ^r M ) |` ( dom R u. ran R ) ) = ( `' R ^r M ) )
64	54, 62, 63	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) |` ( dom R u. ran R ) ) = ( `' R ^r M ) )
65	49, 64	syl5eq 2469	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) = ( `' R ^r M ) )
66		cnvco 4977	. . . . . . . . . . . . . 14 |- `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( `' ( R ^r M ) o. `' ( _I |` ( dom R u. ran R ) ) )
67		eluzge2nn0 11144	. . . . . . . . . . . . . . . . 17 |- ( M e. ( ZZ>= ` 2 ) -> M e. NN0 )
68	50, 67	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. NN0 )
69		simp3 1007	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> R e. V )
70		relexpcnv 13037	. . . . . . . . . . . . . . . 16 |- ( ( M e. NN0 /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
71	68, 69, 70	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
72	14	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom R u. ran R ) ) )
73	71, 72	coeq12d 4956	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( `' ( R ^r M ) o. `' ( _I |` ( dom R u. ran R ) ) ) = ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) )
74	66, 73	syl5eq 2469	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) )
75	65, 74, 71	3eqtr4d 2467	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = `' ( R ^r M ) )
76		relco 5290	. . . . . . . . . . . . 13 |- Rel ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) )
77		relexpuzrel 13054	. . . . . . . . . . . . . 14 |- ( ( M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
78	77	3adant1 1023	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
79		cnveqb 5248	. . . . . . . . . . . . 13 |- ( ( Rel ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) /\ Rel ( R ^r M ) ) -> ( ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( R ^r M ) <-> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = `' ( R ^r M ) ) )
80	76, 78, 79	sylancr 667	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( R ^r M ) <-> `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = `' ( R ^r M ) ) )
81	75, 80	mpbird 235	. . . . . . . . . . 11 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( R ^r M ) )
82		simp1 1005	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N = 0 )
83	82	oveq2d 6260	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
84	32	3ad2ant3 1028	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
85	83, 84	eqtrd 2457	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
86	85	coeq1d 4953	. . . . . . . . . . 11 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) )
87	82	oveq1d 6259	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = ( 0 + M ) )
88		eluzelcn 11116	. . . . . . . . . . . . . . 15 |- ( M e. ( ZZ>= ` 2 ) -> M e. CC )
89	50, 88	syl 17	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. CC )
90	89	addid2d 9780	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( 0 + M ) = M )
91	87, 90	eqtrd 2457	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = M )
92	91	oveq2d 6260	. . . . . . . . . . 11 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r M ) )
93	81, 86, 92	3eqtr4d 2467	. . . . . . . . . 10 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
94	93, 5	syl 17	. . . . . . . . 9 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
95	94	3exp 1204	. . . . . . . 8 |- ( N = 0 -> ( M e. ( ZZ>= ` 2 ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
96	48, 95	jaod 381	. . . . . . 7 |- ( N = 0 -> ( ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
97	8, 96	syl5bi 220	. . . . . 6 |- ( N = 0 -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
98	7, 97	jaoi 380	. . . . 5 |- ( ( N e. NN \/ N = 0 ) -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
99	3, 98	syl 17	. . . 4 |- ( N e. NN0 -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
100		elnn1uz2 11181	. . . . . . . 8 |- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
101	100	biimpi 197	. . . . . . 7 |- ( N e. NN -> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
102		coires1 5310	. . . . . . . . . . . 12 |- ( R o. ( _I |` ( dom R u. ran R ) ) ) = ( R |` ( dom R u. ran R ) )
103		resss 5085	. . . . . . . . . . . 12 |- ( R |` ( dom R u. ran R ) ) C_ R
104	102, 103	eqsstri 3432	. . . . . . . . . . 11 |- ( R o. ( _I |` ( dom R u. ran R ) ) ) C_ R
105	104	a1i 11	. . . . . . . . . 10 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R o. ( _I |` ( dom R u. ran R ) ) ) C_ R )
106		simp1 1005	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> N = 1 )
107	106	oveq2d 6260	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 1 ) )
108	37	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 1 ) = R )
109	107, 108	eqtrd 2457	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = R )
110		simp2 1006	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> M = 0 )
111	110	oveq2d 6260	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
112	32	3ad2ant3 1028	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
113	111, 112	eqtrd 2457	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
114	109, 113	coeq12d 4956	. . . . . . . . . 10 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R o. ( _I |` ( dom R u. ran R ) ) ) )
115	106, 110	oveq12d 6262	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 1 + 0 ) )
116		1cnd 9605	. . . . . . . . . . . . . 14 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> 1 e. CC )
117	116	addid1d 9779	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( 1 + 0 ) = 1 )
118	115, 117	eqtrd 2457	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = 1 )
119	118	oveq2d 6260	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
120	119, 108	eqtrd 2457	. . . . . . . . . 10 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
121	105, 114, 120	3sstr4d 3445	. . . . . . . . 9 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
122	121	3exp 1204	. . . . . . . 8 |- ( N = 1 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
123		coires1 5310	. . . . . . . . . . . 12 |- ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r N ) |` ( dom R u. ran R ) )
124		relexpuzrel 13054	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )
125	124	3adant2 1024	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> Rel ( R ^r N ) )
126		simp1 1005	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. ( ZZ>= ` 2 ) )
127		eluz2nn 11143	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` 2 ) -> N e. NN )
128	126, 127	syl 17	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. NN )
129		simp3 1007	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> R e. V )
130		relexpnndm 13043	. . . . . . . . . . . . . . 15 |- ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
131	128, 129, 130	syl2anc 665	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
132		ssun1 3567	. . . . . . . . . . . . . 14 |- dom R C_ ( dom R u. ran R )
133	131, 132	syl6ss 3414	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
134		relssres 5099	. . . . . . . . . . . . 13 |- ( ( Rel ( R ^r N ) /\ dom ( R ^r N ) C_ ( dom R u. ran R ) ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
135	125, 133, 134	syl2anc 665	. . . . . . . . . . . 12 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) |` ( dom R u. ran R ) ) = ( R ^r N ) )
136	123, 135	syl5eq 2469	. . . . . . . . . . 11 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( R ^r N ) )
137		simp2 1006	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> M = 0 )
138	137	oveq2d 6260	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
139	32	3ad2ant3 1028	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
140	138, 139	eqtrd 2457	. . . . . . . . . . . 12 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
141	140	coeq2d 4954	. . . . . . . . . . 11 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) )
142	137	oveq2d 6260	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = ( N + 0 ) )
143		eluzelcn 11116	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` 2 ) -> N e. CC )
144	126, 143	syl 17	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. CC )
145	144	addid1d 9779	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + 0 ) = N )
146	142, 145	eqtrd 2457	. . . . . . . . . . . 12 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = N )
147	146	oveq2d 6260	. . . . . . . . . . 11 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
148	136, 141, 147	3eqtr4d 2467	. . . . . . . . . 10 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
149	148, 5	syl 17	. . . . . . . . 9 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
150	149	3exp 1204	. . . . . . . 8 |- ( N e. ( ZZ>= ` 2 ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
151	122, 150	jaoi 380	. . . . . . 7 |- ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
152	101, 151	syl 17	. . . . . 6 |- ( N e. NN -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
153		coires1 5310	. . . . . . . . . 10 |- ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( _I |` ( dom R u. ran R ) ) |` ( dom R u. ran R ) )
154		resres 5074	. . . . . . . . . 10 |- ( ( _I |` ( dom R u. ran R ) ) |` ( dom R u. ran R ) ) = ( _I |` ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) )
155		inidm 3609	. . . . . . . . . . 11 |- ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) = ( dom R u. ran R )
156	155	reseq2i 5059	. . . . . . . . . 10 |- ( _I |` ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
157	153, 154, 156	3eqtri 2449	. . . . . . . . 9 |- ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
158		simp1 1005	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> N = 0 )
159	158	oveq2d 6260	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
160	32	3ad2ant3 1028	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
161	159, 160	eqtrd 2457	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
162		simp2 1006	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> M = 0 )
163	162	oveq2d 6260	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
164	163, 160	eqtrd 2457	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
165	161, 164	coeq12d 4956	. . . . . . . . 9 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) )
166	158, 162	oveq12d 6262	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 0 + 0 ) )
167		00id 9754	. . . . . . . . . . . . 13 |- ( 0 + 0 ) = 0
168	167	a1i 11	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( 0 + 0 ) = 0 )
169	166, 168	eqtrd 2457	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = 0 )
170	169	oveq2d 6260	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 0 ) )
171	170, 160	eqtrd 2457	. . . . . . . . 9 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( _I |` ( dom R u. ran R ) ) )
172	157, 165, 171	3eqtr4a 2483	. . . . . . . 8 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
173	172, 5	syl 17	. . . . . . 7 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
174	173	3exp 1204	. . . . . 6 |- ( N = 0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
175	152, 174	jaoi 380	. . . . 5 |- ( ( N e. NN \/ N = 0 ) -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
176	3, 175	syl 17	. . . 4 |- ( N e. NN0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
177	99, 176	jaod 381	. . 3 |- ( N e. NN0 -> ( ( M e. NN \/ M = 0 ) -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
178	1, 177	syl5bi 220	. 2 |- ( N e. NN0 -> ( M e. NN0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
179	178	3imp 1199	1 |- ( ( N e. NN0 /\ M e. NN0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )

Syntax hints:   -> wi 4   <-> wb 187   \/ wo 369   /\ w3a 982   = wceq 1437   e. wcel 1872   _Vcvv 3017   u. cun 3372   i^i cin 3373   C_ wss 3374   _I cid 4701   `'ccnv 4790   dom cdm 4791   ran crn 4792   |` cres 4793   o. ccom 4795   Rel wrel 4796   ` cfv 5539  (class class class)co 6244   CCcc 9483   0cc0 9485   1c1 9486   + caddc 9488   NNcn 10555   2c2 10605   NN0cn0 10815   ZZ>=cuz 11105   ^r crelexp 13022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556  df-2 10614  df-n0 10816  df-z 10884  df-uz 11106  df-seq 12159  df-relexp 13023

This theorem is referenced by:  iunrelexpuztr  36224  cotrclrcl  36247