Theorem relexpdm

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	relexpdm	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		relexpdmg	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
2		dmrnssfld	⊢ ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅
3	1 2	sstrdi	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → dom ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 )