Theorem relexpaddss 36354

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 13165 or when the sum of the powers isn't 1 as shown by relexpaddg 13164. (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 10899	. . 3 |- ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
2		elnn0 10899	. . . . . 6 |- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
3	2	biimpi 199	. . . . 5 |- ( N e. NN0 -> ( N e. NN \/ N = 0 ) )
4		relexpaddnn 13162	. . . . . . . 8 |- ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
5		eqimss 3495	. . . . . . . 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 1214	. . . . . 6 |- ( N e. NN -> ( M e. NN -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
8		elnn1uz2 11263	. . . . . . 7 |- ( M e. NN <-> ( M = 1 \/ M e. ( ZZ>= ` 2 ) ) )
9		relco 5351	. . . . . . . . . . . . . 14 |- Rel ( ( _I |` ( dom R u. ran R ) ) o. R )
10		dfrel2 5304	. . . . . . . . . . . . . . 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 199	. . . . . . . . . . . . . 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 5038	. . . . . . . . . . . . . . . . 17 |- `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R o. `' ( _I |` ( dom R u. ran R ) ) )
14		cnvresid 5674	. . . . . . . . . . . . . . . . . 18 |- `' ( _I |` ( dom R u. ran R ) ) = ( _I |` ( dom R u. ran R ) )
15	14	coeq2i 5013	. . . . . . . . . . . . . . . . 17 |- ( `' R o. `' ( _I |` ( dom R u. ran R ) ) ) = ( `' R o. ( _I |` ( dom R u. ran R ) ) )
16		coires1 5371	. . . . . . . . . . . . . . . . 17 |- ( `' R o. ( _I |` ( dom R u. ran R ) ) ) = ( `' R |` ( dom R u. ran R ) )
17	13, 15, 16	3eqtri 2487	. . . . . . . . . . . . . . . 16 |- `' ( ( _I |` ( dom R u. ran R ) ) o. R ) = ( `' R |` ( dom R u. ran R ) )
18		eqimss 3495	. . . . . . . . . . . . . . . 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 5025	. . . . . . . . . . . . . . 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 5146	. . . . . . . . . . . . . . 15 |- ( `' R |` ( dom R u. ran R ) ) C_ `' R
23		cnvss 5025	. . . . . . . . . . . . . . 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 3452	. . . . . . . . . . . . 13 |- `' `' ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' `' R
26	12, 25	eqsstr3i 3474	. . . . . . . . . . . 12 |- ( ( _I |` ( dom R u. ran R ) ) o. R ) C_ `' `' R
27		cnvcnvss 5308	. . . . . . . . . . . 12 |- `' `' R C_ R
28	26, 27	sstri 3452	. . . . . . . . . . 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 1014	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> N = 0 )
31	30	oveq2d 6330	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
32		relexp0g 13133	. . . . . . . . . . . . 13 |- ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
33	32	3ad2ant3 1037	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
34	31, 33	eqtrd 2495	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
35		simp2 1015	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> M = 1 )
36	35	oveq2d 6330	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r M ) = ( R ^r 1 ) )
37		relexp1g 13137	. . . . . . . . . . . . 13 |- ( R e. V -> ( R ^r 1 ) = R )
38	37	3ad2ant3 1037	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r 1 ) = R )
39	36, 38	eqtrd 2495	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r M ) = R )
40	34, 39	coeq12d 5017	. . . . . . . . . 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 6332	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( N + M ) = ( 0 + 1 ) )
42		1cnd 9684	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> 1 e. CC )
43	42	addid2d 9859	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( 0 + 1 ) = 1 )
44	41, 43	eqtrd 2495	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( N + M ) = 1 )
45	44	oveq2d 6330	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
46	45, 38	eqtrd 2495	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
47	29, 40, 46	3sstr4d 3486	. . . . . . . . 9 |- ( ( N = 0 /\ M = 1 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
48	47	3exp 1214	. . . . . . . 8 |- ( N = 0 -> ( M = 1 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
49		coires1 5371	. . . . . . . . . . . . . 14 |- ( ( `' R ^r M ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( `' R ^r M ) |` ( dom R u. ran R ) )
50		simp2 1015	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> M e. ( ZZ>= ` 2 ) )
51		cnvexg 6765	. . . . . . . . . . . . . . . . 17 |- ( R e. V -> `' R e. _V )
52	51	3ad2ant3 1037	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> `' R e. _V )
53		relexpuzrel 13163	. . . . . . . . . . . . . . . 16 |- ( ( M e. ( ZZ>= ` 2 ) /\ `' R e. _V ) -> Rel ( `' R ^r M ) )
54	50, 52, 53	syl2anc 671	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( `' R ^r M ) )
55		eluz2nn 11225	. . . . . . . . . . . . . . . . . 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 13152	. . . . . . . . . . . . . . . . 17 |- ( ( M e. NN /\ `' R e. _V ) -> dom ( `' R ^r M ) C_ dom `' R )
58	56, 52, 57	syl2anc 671	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ dom `' R )
59		df-rn 4863	. . . . . . . . . . . . . . . . 17 |- ran R = dom `' R
60		ssun2 3609	. . . . . . . . . . . . . . . . 17 |- ran R C_ ( dom R u. ran R )
61	59, 60	eqsstr3i 3474	. . . . . . . . . . . . . . . 16 |- dom `' R C_ ( dom R u. ran R )
62	58, 61	syl6ss 3455	. . . . . . . . . . . . . . 15 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> dom ( `' R ^r M ) C_ ( dom R u. ran R ) )
63		relssres 5160	. . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . 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 2507	. . . . . . . . . . . . 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 5038	. . . . . . . . . . . . . 14 |- `' ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) ) = ( `' ( R ^r M ) o. `' ( _I |` ( dom R u. ran R ) ) )
67		eluzge2nn0 11226	. . . . . . . . . . . . . . . . 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 1016	. . . . . . . . . . . . . . . 16 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> R e. V )
70		relexpcnv 13146	. . . . . . . . . . . . . . . 16 |- ( ( M e. NN0 /\ R e. V ) -> `' ( R ^r M ) = ( `' R ^r M ) )
71	68, 69, 70	syl2anc 671	. . . . . . . . . . . . . . 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 5017	. . . . . . . . . . . . . 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 2507	. . . . . . . . . . . . 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 2505	. . . . . . . . . . . 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 5351	. . . . . . . . . . . . 13 |- Rel ( ( _I |` ( dom R u. ran R ) ) o. ( R ^r M ) )
77		relexpuzrel 13163	. . . . . . . . . . . . . 14 |- ( ( M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
78	77	3adant1 1032	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r M ) )
79		cnveqb 5309	. . . . . . . . . . . . 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 674	. . . . . . . . . . . 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 240	. . . . . . . . . . 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 1014	. . . . . . . . . . . . . 14 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> N = 0 )
83	82	oveq2d 6330	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
84	32	3ad2ant3 1037	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
85	83, 84	eqtrd 2495	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
86	85	coeq1d 5014	. . . . . . . . . . 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 6329	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = ( 0 + M ) )
88		eluzelcn 11198	. . . . . . . . . . . . . . 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 9859	. . . . . . . . . . . . 13 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( 0 + M ) = M )
91	87, 90	eqtrd 2495	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( N + M ) = M )
92	91	oveq2d 6330	. . . . . . . . . . 11 |- ( ( N = 0 /\ M e. ( ZZ>= ` 2 ) /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r M ) )
93	81, 86, 92	3eqtr4d 2505	. . . . . . . . . 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 1214	. . . . . . . 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 386	. . . . . . 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 225	. . . . . 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 385	. . . . 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 11263	. . . . . . . 8 |- ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
101	100	biimpi 199	. . . . . . 7 |- ( N e. NN -> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
102		coires1 5371	. . . . . . . . . . . 12 |- ( R o. ( _I |` ( dom R u. ran R ) ) ) = ( R |` ( dom R u. ran R ) )
103		resss 5146	. . . . . . . . . . . 12 |- ( R |` ( dom R u. ran R ) ) C_ R
104	102, 103	eqsstri 3473	. . . . . . . . . . 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 1014	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> N = 1 )
107	106	oveq2d 6330	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 1 ) )
108	37	3ad2ant3 1037	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 1 ) = R )
109	107, 108	eqtrd 2495	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = R )
110		simp2 1015	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> M = 0 )
111	110	oveq2d 6330	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
112	32	3ad2ant3 1037	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
113	111, 112	eqtrd 2495	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
114	109, 113	coeq12d 5017	. . . . . . . . . 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 6332	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 1 + 0 ) )
116		1cnd 9684	. . . . . . . . . . . . . 14 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> 1 e. CC )
117	116	addid1d 9858	. . . . . . . . . . . . 13 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( 1 + 0 ) = 1 )
118	115, 117	eqtrd 2495	. . . . . . . . . . . 12 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( N + M ) = 1 )
119	118	oveq2d 6330	. . . . . . . . . . 11 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 1 ) )
120	119, 108	eqtrd 2495	. . . . . . . . . 10 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = R )
121	105, 114, 120	3sstr4d 3486	. . . . . . . . 9 |- ( ( N = 1 /\ M = 0 /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) )
122	121	3exp 1214	. . . . . . . 8 |- ( N = 1 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
123		coires1 5371	. . . . . . . . . . . 12 |- ( ( R ^r N ) o. ( _I |` ( dom R u. ran R ) ) ) = ( ( R ^r N ) |` ( dom R u. ran R ) )
124		relexpuzrel 13163	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )
125	124	3adant2 1033	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> Rel ( R ^r N ) )
126		simp1 1014	. . . . . . . . . . . . . . . 16 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> N e. ( ZZ>= ` 2 ) )
127		eluz2nn 11225	. . . . . . . . . . . . . . . 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 1016	. . . . . . . . . . . . . . 15 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> R e. V )
130		relexpnndm 13152	. . . . . . . . . . . . . . 15 |- ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
131	128, 129, 130	syl2anc 671	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
132		ssun1 3608	. . . . . . . . . . . . . 14 |- dom R C_ ( dom R u. ran R )
133	131, 132	syl6ss 3455	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
134		relssres 5160	. . . . . . . . . . . . 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 671	. . . . . . . . . . . 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 2507	. . . . . . . . . . 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 1015	. . . . . . . . . . . . . 14 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> M = 0 )
138	137	oveq2d 6330	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
139	32	3ad2ant3 1037	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
140	138, 139	eqtrd 2495	. . . . . . . . . . . 12 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
141	140	coeq2d 5015	. . . . . . . . . . 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 6330	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = ( N + 0 ) )
143		eluzelcn 11198	. . . . . . . . . . . . . . 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 9858	. . . . . . . . . . . . 13 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + 0 ) = N )
146	142, 145	eqtrd 2495	. . . . . . . . . . . 12 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( N + M ) = N )
147	146	oveq2d 6330	. . . . . . . . . . 11 |- ( ( N e. ( ZZ>= ` 2 ) /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r N ) )
148	136, 141, 147	3eqtr4d 2505	. . . . . . . . . 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 1214	. . . . . . . 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 385	. . . . . . 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 5371	. . . . . . . . . 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 5135	. . . . . . . . . 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 3652	. . . . . . . . . . 11 |- ( ( dom R u. ran R ) i^i ( dom R u. ran R ) ) = ( dom R u. ran R )
156	155	reseq2i 5120	. . . . . . . . . 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 2487	. . . . . . . . 9 |- ( ( _I |` ( dom R u. ran R ) ) o. ( _I |` ( dom R u. ran R ) ) ) = ( _I |` ( dom R u. ran R ) )
158		simp1 1014	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> N = 0 )
159	158	oveq2d 6330	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
160	32	3ad2ant3 1037	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
161	159, 160	eqtrd 2495	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r N ) = ( _I |` ( dom R u. ran R ) ) )
162		simp2 1015	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> M = 0 )
163	162	oveq2d 6330	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( R ^r 0 ) )
164	163, 160	eqtrd 2495	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r M ) = ( _I |` ( dom R u. ran R ) ) )
165	161, 164	coeq12d 5017	. . . . . . . . 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 6332	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = ( 0 + 0 ) )
167		00id 9833	. . . . . . . . . . . . 13 |- ( 0 + 0 ) = 0
168	167	a1i 11	. . . . . . . . . . . 12 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( 0 + 0 ) = 0 )
169	166, 168	eqtrd 2495	. . . . . . . . . . 11 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( N + M ) = 0 )
170	169	oveq2d 6330	. . . . . . . . . 10 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( R ^r 0 ) )
171	170, 160	eqtrd 2495	. . . . . . . . 9 |- ( ( N = 0 /\ M = 0 /\ R e. V ) -> ( R ^r ( N + M ) ) = ( _I |` ( dom R u. ran R ) ) )
172	157, 165, 171	3eqtr4a 2521	. . . . . . . 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 1214	. . . . . 6 |- ( N = 0 -> ( M = 0 -> ( R e. V -> ( ( R ^r N ) o. ( R ^r M ) ) C_ ( R ^r ( N + M ) ) ) ) )
175	152, 174	jaoi 385	. . . . 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 386	. . 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 225	. 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 1208	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 189   \/ wo 374   /\ w3a 991   = wceq 1454   e. wcel 1897   _Vcvv 3056   u. cun 3413   i^i cin 3414   C_ wss 3415   _I cid 4762   `'ccnv 4851   dom cdm 4852   ran crn 4853   |` cres 4854   o. ccom 4856   Rel wrel 4857   ` cfv 5600  (class class class)co 6314   CCcc 9562   0cc0 9564   1c1 9565   + caddc 9567   NNcn 10636   2c2 10686   NN0cn0 10897   ZZ>=cuz 11187   ^r crelexp 13131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-2nd 6820  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-2 10695  df-n0 10898  df-z 10966  df-uz 11188  df-seq 12245  df-relexp 13132

This theorem is referenced by:  iunrelexpuztr  36355  cotrclrcl  36378