Database
REAL AND COMPLEX NUMBERS
Reflexive and transitive closures of relations
Exponentiation of relations
relexpfldd
Metamath Proof Explorer
Description: The field 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
relexpfldd.2
⊢ φ → R ∈ V
Assertion
relexpfldd
⊢ φ → N ∈ ℕ 0 → ⋃ ⋃ R ↑ r N ⊆ ⋃ ⋃ R
Proof
Step
Hyp
Ref
Expression
1
relexpfldd.2
⊢ φ → R ∈ V
2
relexpfld
⊢ N ∈ ℕ 0 ∧ R ∈ V → ⋃ ⋃ R ↑ r N ⊆ ⋃ ⋃ R
3
2
ex
⊢ N ∈ ℕ 0 → R ∈ V → ⋃ ⋃ R ↑ r N ⊆ ⋃ ⋃ R
4
1 3
syl5com
⊢ φ → N ∈ ℕ 0 → ⋃ ⋃ R ↑ r N ⊆ ⋃ ⋃ R