Metamath Proof Explorer


Theorem brtrclrec

Description: Two classes related by the indexed union of relation exponentiation over the natural numbers is equivalent to the existence of at least one number such that the two classes are related by that relationship power. (Contributed by RP, 2-Jun-2020)

Ref Expression
Hypothesis brtrclrec.def 𝐶 = ( 𝑟 ∈ V ↦ 𝑛 ∈ ℕ ( 𝑟𝑟 𝑛 ) )
Assertion brtrclrec ( 𝑅𝑉 → ( 𝑋 ( 𝐶𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ ℕ 𝑋 ( 𝑅𝑟 𝑛 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 brtrclrec.def 𝐶 = ( 𝑟 ∈ V ↦ 𝑛 ∈ ℕ ( 𝑟𝑟 𝑛 ) )
2 nnex ℕ ∈ V
3 1 briunov2 ( ( 𝑅𝑉 ∧ ℕ ∈ V ) → ( 𝑋 ( 𝐶𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ ℕ 𝑋 ( 𝑅𝑟 𝑛 ) 𝑌 ) )
4 2 3 mpan2 ( 𝑅𝑉 → ( 𝑋 ( 𝐶𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ ℕ 𝑋 ( 𝑅𝑟 𝑛 ) 𝑌 ) )