Theorem relexpnndm

Description: The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020)

	Ref	Expression
Assertion	relexpnndm	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 1 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 1 ) )
2	1	dmeqd	⊢ ( 𝑛 = 1 → dom ( 𝑅 ↑𝑟 𝑛 ) = dom ( 𝑅 ↑𝑟 1 ) )
3	2	sseq1d	⊢ ( 𝑛 = 1 → ( dom ( 𝑅 ↑𝑟 𝑛 ) ⊆ dom 𝑅 ↔ dom ( 𝑅 ↑𝑟 1 ) ⊆ dom 𝑅 ) )
4	3	imbi2d	⊢ ( 𝑛 = 1 → ( ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑛 ) ⊆ dom 𝑅 ) ↔ ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 1 ) ⊆ dom 𝑅 ) ) )
5		oveq2	⊢ ( 𝑛 = 𝑚 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑚 ) )
6	5	dmeqd	⊢ ( 𝑛 = 𝑚 → dom ( 𝑅 ↑𝑟 𝑛 ) = dom ( 𝑅 ↑𝑟 𝑚 ) )
7	6	sseq1d	⊢ ( 𝑛 = 𝑚 → ( dom ( 𝑅 ↑𝑟 𝑛 ) ⊆ dom 𝑅 ↔ dom ( 𝑅 ↑𝑟 𝑚 ) ⊆ dom 𝑅 ) )
8	7	imbi2d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑛 ) ⊆ dom 𝑅 ) ↔ ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑚 ) ⊆ dom 𝑅 ) ) )
9		oveq2	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
10	9	dmeqd	⊢ ( 𝑛 = ( 𝑚 + 1 ) → dom ( 𝑅 ↑𝑟 𝑛 ) = dom ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) )
11	10	sseq1d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( dom ( 𝑅 ↑𝑟 𝑛 ) ⊆ dom 𝑅 ↔ dom ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ dom 𝑅 ) )
12	11	imbi2d	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑛 ) ⊆ dom 𝑅 ) ↔ ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ dom 𝑅 ) ) )
13		oveq2	⊢ ( 𝑛 = 𝑁 → ( 𝑅 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑁 ) )
14	13	dmeqd	⊢ ( 𝑛 = 𝑁 → dom ( 𝑅 ↑𝑟 𝑛 ) = dom ( 𝑅 ↑𝑟 𝑁 ) )
15	14	sseq1d	⊢ ( 𝑛 = 𝑁 → ( dom ( 𝑅 ↑𝑟 𝑛 ) ⊆ dom 𝑅 ↔ dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 ) )
16	15	imbi2d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑛 ) ⊆ dom 𝑅 ) ↔ ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 ) ) )
17		relexp1g	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )
18	17	dmeqd	⊢ ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 1 ) = dom 𝑅 )
19		eqimss	⊢ ( dom ( 𝑅 ↑𝑟 1 ) = dom 𝑅 → dom ( 𝑅 ↑𝑟 1 ) ⊆ dom 𝑅 )
20	18 19	syl	⊢ ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 1 ) ⊆ dom 𝑅 )
21		relexpsucnnr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑚 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
22	21	ancoms	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
23	22	dmeqd	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) = dom ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) )
24		dmcoss	⊢ dom ( ( 𝑅 ↑𝑟 𝑚 ) ∘ 𝑅 ) ⊆ dom 𝑅
25	23 24	eqsstrdi	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ dom 𝑅 )
26	25	a1d	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ( dom ( 𝑅 ↑𝑟 𝑚 ) ⊆ dom 𝑅 → dom ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ dom 𝑅 ) )
27	26	ex	⊢ ( 𝑚 ∈ ℕ → ( 𝑅 ∈ 𝑉 → ( dom ( 𝑅 ↑𝑟 𝑚 ) ⊆ dom 𝑅 → dom ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ dom 𝑅 ) ) )
28	27	a2d	⊢ ( 𝑚 ∈ ℕ → ( ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑚 ) ⊆ dom 𝑅 ) → ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 ( 𝑚 + 1 ) ) ⊆ dom 𝑅 ) ) )
29	4 8 12 16 20 28	nnind	⊢ ( 𝑁 ∈ ℕ → ( 𝑅 ∈ 𝑉 → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 ) )
30	29	imp	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ dom 𝑅 )