Database
REAL AND COMPLEX NUMBERS
Reflexive and transitive closures of relations
Exponentiation of relations
relexpdmd
Metamath Proof Explorer
Description: The domain of an exponentiation of a relation a subset of the relation's
field. (Contributed by Drahflow , 12-Nov-2015) (Revised by RP , 30-May-2020)
Ref
Expression
Hypothesis
relexpdmd.2
⊢ φ → R ∈ V
Assertion
relexpdmd
⊢ φ → N ∈ ℕ 0 → dom ⁡ R ↑ r N ⊆ ⋃ ⋃ R
Proof
Step
Hyp
Ref
Expression
1
relexpdmd.2
⊢ φ → R ∈ V
2
relexpdm
⊢ N ∈ ℕ 0 ∧ R ∈ V → dom ⁡ R ↑ r N ⊆ ⋃ ⋃ R
3
2
ex
⊢ N ∈ ℕ 0 → R ∈ V → dom ⁡ R ↑ r N ⊆ ⋃ ⋃ R
4
1 3
syl5com
⊢ φ → N ∈ ℕ 0 → dom ⁡ R ↑ r N ⊆ ⋃ ⋃ R