Metamath Proof Explorer

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 ⊢ N ∈ ℕ ∧ R ∈ V → ran ⁡ R ↑ r N ⊆ ran ⁡ R

Proof

Step Hyp Ref Expression
1 cnvexg ⊢ R ∈ V → R -1 ∈ V
2 relexpnndm ⊢ N ∈ ℕ ∧ R -1 ∈ V → dom ⁡ R -1 ↑ r N ⊆ dom ⁡ R -1
3 1 2 sylan2 ⊢ N ∈ ℕ ∧ R ∈ V → dom ⁡ R -1 ↑ r N ⊆ dom ⁡ R -1
4 df-rn ⊢ ran ⁡ R ↑ r N = dom ⁡ R ↑ r N -1
5 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
6 relexpcnv ⊢ N ∈ ℕ 0 ∧ R ∈ V → R ↑ r N -1 = R -1 ↑ r N
7 5 6 sylan ⊢ N ∈ ℕ ∧ R ∈ V → R ↑ r N -1 = R -1 ↑ r N
8 7 dmeqd ⊢ N ∈ ℕ ∧ R ∈ V → dom ⁡ R ↑ r N -1 = dom ⁡ R -1 ↑ r N
9 4 8 syl5eq ⊢ N ∈ ℕ ∧ R ∈ V → ran ⁡ R ↑ r N = dom ⁡ R -1 ↑ r N
10 df-rn ⊢ ran ⁡ R = dom ⁡ R -1
11 10 a1i ⊢ N ∈ ℕ ∧ R ∈ V → ran ⁡ R = dom ⁡ R -1
12 3 9 11 3sstr4d ⊢ N ∈ ℕ ∧ R ∈ V → ran ⁡ R ↑ r N ⊆ ran ⁡ R