Theorem relexpnnrn

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

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

Proof

Step	Hyp	Ref	Expression
1		cnvexg	⊢ ( 𝑅 ∈ 𝑉 → ◡ 𝑅 ∈ V )
2		relexpnndm	⊢ ( ( 𝑁 ∈ ℕ ∧ ◡ 𝑅 ∈ V ) → dom ( ◡ 𝑅 ↑𝑟 𝑁 ) ⊆ dom ◡ 𝑅 )
3	1 2	sylan2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ( ◡ 𝑅 ↑𝑟 𝑁 ) ⊆ dom ◡ 𝑅 )
4		df-rn	⊢ ran ( 𝑅 ↑𝑟 𝑁 ) = dom ◡ ( 𝑅 ↑𝑟 𝑁 )
5		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
6		relexpcnv	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )
7	5 6	sylan	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ◡ ( 𝑅 ↑𝑟 𝑁 ) = ( ◡ 𝑅 ↑𝑟 𝑁 ) )
8	7	dmeqd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → dom ◡ ( 𝑅 ↑𝑟 𝑁 ) = dom ( ◡ 𝑅 ↑𝑟 𝑁 ) )
9	4 8	syl5eq	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ran ( 𝑅 ↑𝑟 𝑁 ) = dom ( ◡ 𝑅 ↑𝑟 𝑁 ) )
10		df-rn	⊢ ran 𝑅 = dom ◡ 𝑅
11	10	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ran 𝑅 = dom ◡ 𝑅 )
12	3 9 11	3sstr4d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ) → ran ( 𝑅 ↑𝑟 𝑁 ) ⊆ ran 𝑅 )