Metamath Proof Explorer


Theorem relexprn

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 relexprn ( ( 𝑁 ∈ ℕ0𝑅𝑉 ) → ran ( 𝑅𝑟 𝑁 ) ⊆ 𝑅 )

Proof

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