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 ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relexprng | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ran ( 𝑅 ↑𝑟 𝑁 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) | |
2 | dmrnssfld | ⊢ ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅 | |
3 | 1 2 | sstrdi | ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ) → ran ( 𝑅 ↑𝑟 𝑁 ) ⊆ ∪ ∪ 𝑅 ) |