Theorem brrtrclrec

Description: Two classes related by the indexed union of relation exponentiation over the natural numbers (including zero) 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	brrtrclrec.def	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
Assertion	brrtrclrec	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑋 ( 𝐶 ‘ 𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ ℕ0 𝑋 ( 𝑅 ↑𝑟 𝑛 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		brrtrclrec.def	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
2		nn0ex	⊢ ℕ0 ∈ V
3	1	briunov2	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ℕ0 ∈ V ) → ( 𝑋 ( 𝐶 ‘ 𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ ℕ0 𝑋 ( 𝑅 ↑𝑟 𝑛 ) 𝑌 ) )
4	2 3	mpan2	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑋 ( 𝐶 ‘ 𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ ℕ0 𝑋 ( 𝑅 ↑𝑟 𝑛 ) 𝑌 ) )