Metamath Proof Explorer

Theorem relexpaddss

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 or when the sum of the powers isn't 1 as shown by relexpaddg . (Contributed by RP, 3-Jun-2020)

Ref Expression
Assertion relexpaddss ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
2 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
3 2 biimpi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
4 relexpaddnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
5 eqimss ⊢ ( ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
6 4 5 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
7 6 3exp ⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
8 elnn1uz2 ⊢ ( 𝑀 ∈ ℕ ↔ ( 𝑀 = 1 ∨ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) )
9 relco ⊢ Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 )
10 dfrel2 ⊢ ( Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ↔ ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) )
11 10 biimpi ⊢ ( Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) → ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) )
12 9 11 ax-mp ⊢ ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 )
13 cnvco ⊢ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ◡ 𝑅 ∘ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
14 cnvresid ⊢ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
15 14 coeq2i ⊢ ( ◡ 𝑅 ∘ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ◡ 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
16 coires1 ⊢ ( ◡ 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
17 13 15 16 3eqtri ⊢ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
18 eqimss ⊢ ( ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) = ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) → ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
19 17 18 ax-mp ⊢ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
20 cnvss ⊢ ( ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) → ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ◡ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
21 19 20 ax-mp ⊢ ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ◡ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
22 resss ⊢ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ◡ 𝑅
23 cnvss ⊢ ( ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ◡ 𝑅 → ◡ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ◡ ◡ 𝑅 )
24 22 23 ax-mp ⊢ ◡ ( ◡ 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ ◡ ◡ 𝑅
25 21 24 sstri ⊢ ◡ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ◡ ◡ 𝑅
26 12 25 eqsstrri ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ◡ ◡ 𝑅
27 cnvcnvss ⊢ ◡ ◡ 𝑅 ⊆ 𝑅
28 26 27 sstri ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ 𝑅
29 28 a1i ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) ⊆ 𝑅 )
30 simp1 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
31 30 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
32 relexp0g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
33 32 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
34 31 33 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
35 simp2 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → 𝑀 = 1 )
36 35 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( 𝑅 ↑𝑟 1 ) )
37 relexp1g ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
38 37 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
39 36 38 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = 𝑅 )
40 34 39 coeq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ 𝑅 ) )
41 30 35 oveq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 0 + 1 ) )
42 1cnd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → 1 ∈ ℂ )
43 42 addid2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 0 + 1 ) = 1 )
44 41 43 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 1 )
45 44 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 1 ) )
46 45 38 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = 𝑅 )
47 29 40 46 3sstr4d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 1 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
48 47 3exp ⊢ ( 𝑁 = 0 → ( 𝑀 = 1 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
49 coires1 ⊢ ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
50 simp2 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
51 cnvexg ⊢ ( 𝑅 ∈ 𝑉 → ◡ 𝑅 ∈ V )
52 51 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ 𝑅 ∈ V )
53 relexpuzrel ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ◡ 𝑅 ∈ V ) → Rel ( ◡ 𝑅 ↑𝑟 𝑀 ) )
54 50 52 53 syl2anc ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( ◡ 𝑅 ↑𝑟 𝑀 ) )
55 eluz2nn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ )
56 50 55 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑀 ∈ ℕ )
57 relexpnndm ⊢ ( ( 𝑀 ∈ ℕ ∧ ◡ 𝑅 ∈ V ) → dom ( ◡ 𝑅 ↑𝑟 𝑀 ) ⊆ dom ◡ 𝑅 )
58 56 52 57 syl2anc ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → dom ( ◡ 𝑅 ↑𝑟 𝑀 ) ⊆ dom ◡ 𝑅 )
59 df-rn ⊢ ran 𝑅 = dom ◡ 𝑅
60 ssun2 ⊢ ran 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
61 59 60 eqsstrri ⊢ dom ◡ 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
62 58 61 sstrdi ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → dom ( ◡ 𝑅 ↑𝑟 𝑀 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
63 relssres ⊢ ( ( Rel ( ◡ 𝑅 ↑𝑟 𝑀 ) ∧ dom ( ◡ 𝑅 ↑𝑟 𝑀 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
64 54 62 63 syl2anc ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
65 49 64 syl5eq ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
66 cnvco ⊢ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ◡ ( 𝑅 ↑𝑟 𝑀 ) ∘ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
67 eluzge2nn0 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ0 )
68 50 67 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑀 ∈ ℕ0 )
69 simp3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
70 relexpcnv ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑀 ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
71 68 69 70 syl2anc ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑀 ) = ( ◡ 𝑅 ↑𝑟 𝑀 ) )
72 14 a1i ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
73 71 72 coeq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ◡ ( 𝑅 ↑𝑟 𝑀 ) ∘ ◡ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
74 66 73 syl5eq ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( ◡ 𝑅 ↑𝑟 𝑀 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
75 65 74 71 3eqtr4d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ◡ ( 𝑅 ↑𝑟 𝑀 ) )
76 relco ⊢ Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) )
77 relexpuzrel ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑀 ) )
78 77 3adant1 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑀 ) )
79 cnveqb ⊢ ( ( Rel ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ∧ Rel ( 𝑅 ↑𝑟 𝑀 ) ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑀 ) ↔ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ◡ ( 𝑅 ↑𝑟 𝑀 ) ) )
80 76 78 79 sylancr ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑀 ) ↔ ◡ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ◡ ( 𝑅 ↑𝑟 𝑀 ) ) )
81 75 80 mpbird ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑀 ) )
82 simp1 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
83 82 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
84 32 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
85 83 84 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
86 85 coeq1d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) )
87 82 oveq1d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 0 + 𝑀 ) )
88 eluzelcn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℂ )
89 50 88 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → 𝑀 ∈ ℂ )
90 89 addid2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 0 + 𝑀 ) = 𝑀 )
91 87 90 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 𝑀 )
92 91 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑀 ) )
93 81 86 92 3eqtr4d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
94 93 5 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
95 94 3exp ⊢ ( 𝑁 = 0 → ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
96 48 95 jaod ⊢ ( 𝑁 = 0 → ( ( 𝑀 = 1 ∨ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
97 8 96 syl5bi ⊢ ( 𝑁 = 0 → ( 𝑀 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
98 7 97 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑀 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
99 3 98 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
100 elnn1uz2 ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
101 100 biimpi ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) )
102 coires1 ⊢ ( 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
103 resss ⊢ ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ⊆ 𝑅
104 102 103 eqsstri ⊢ ( 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ⊆ 𝑅
105 104 a1i ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ⊆ 𝑅 )
106 simp1 ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 1 )
107 106 oveq2d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 1 ) )
108 37 3ad2ant3 ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
109 107 108 eqtrd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = 𝑅 )
110 simp2 ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑀 = 0 )
111 110 oveq2d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( 𝑅 ↑𝑟 0 ) )
112 32 3ad2ant3 ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
113 111 112 eqtrd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
114 109 113 coeq12d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
115 106 110 oveq12d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 1 + 0 ) )
116 1cnd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 1 ∈ ℂ )
117 116 addid1d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 1 + 0 ) = 1 )
118 115 117 eqtrd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 1 )
119 118 oveq2d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 1 ) )
120 119 108 eqtrd ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = 𝑅 )
121 105 114 120 3sstr4d ⊢ ( ( 𝑁 = 1 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
122 121 3exp ⊢ ( 𝑁 = 1 → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
123 coires1 ⊢ ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
124 relexpuzrel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
125 124 3adant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → Rel ( 𝑅 ↑𝑟 𝑁 ) )
126 simp1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
127 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
128 126 127 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ℕ )
129 simp3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ 𝑉 )
130 relexpnndm ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 )
131 128 129 130 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 )
132 ssun1 ⊢ dom 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
133 131 132 sstrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
134 relssres ⊢ ( ( Rel ( 𝑅 ↑𝑟 𝑁 ) ∧ dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ( ( 𝑅 ↑𝑟 𝑁 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( 𝑅 ↑𝑟 𝑁 ) )
135 125 133 134 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( 𝑅 ↑𝑟 𝑁 ) )
136 123 135 syl5eq ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( 𝑅 ↑𝑟 𝑁 ) )
137 simp2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑀 = 0 )
138 137 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( 𝑅 ↑𝑟 0 ) )
139 32 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
140 138 139 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
141 140 coeq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
142 137 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 𝑁 + 0 ) )
143 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℂ )
144 126 143 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ ℂ )
145 144 addid1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 0 ) = 𝑁 )
146 142 145 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 𝑁 )
147 146 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 𝑁 ) )
148 136 141 147 3eqtr4d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
149 148 5 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
150 149 3exp ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
151 122 150 jaoi ⊢ ( ( 𝑁 = 1 ∨ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
152 101 151 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
153 coires1 ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
154 resres ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( I ↾ ( ( dom 𝑅 ∪ ran 𝑅 ) ∩ ( dom 𝑅 ∪ ran 𝑅 ) ) )
155 inidm ⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) ∩ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( dom 𝑅 ∪ ran 𝑅 )
156 155 reseq2i ⊢ ( I ↾ ( ( dom 𝑅 ∪ ran 𝑅 ) ∩ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
157 153 154 156 3eqtri ⊢ ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
158 simp1 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑁 = 0 )
159 158 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( 𝑅 ↑𝑟 0 ) )
160 32 3ad2ant3 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
161 159 160 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑁 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
162 simp2 ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → 𝑀 = 0 )
163 162 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( 𝑅 ↑𝑟 0 ) )
164 163 160 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 𝑀 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
165 161 164 coeq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∘ ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
166 158 162 oveq12d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = ( 0 + 0 ) )
167 00id ⊢ ( 0 + 0 ) = 0
168 167 a1i ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 0 + 0 ) = 0 )
169 166 168 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 + 𝑀 ) = 0 )
170 169 oveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( 𝑅 ↑𝑟 0 ) )
171 170 160 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
172 157 165 171 3eqtr4a ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) = ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
173 172 5 syl ⊢ ( ( 𝑁 = 0 ∧ 𝑀 = 0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )
174 173 3exp ⊢ ( 𝑁 = 0 → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
175 152 174 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
176 3 175 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 = 0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
177 99 176 jaod ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
178 1 177 syl5bi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) ) ) )
179 178 3imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ( ( 𝑅 ↑𝑟 𝑁 ) ∘ ( 𝑅 ↑𝑟 𝑀 ) ) ⊆ ( 𝑅 ↑𝑟 ( 𝑁 + 𝑀 ) ) )