Theorem elrtrclrec

Description: Membership in 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 element is a member of that relationship power. (Contributed by RP, 2-Jun-2020)

	Ref	Expression
Hypothesis	rtrclrec.def	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
Assertion	elrtrclrec	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ ℕ0 𝑋 ∈ ( 𝑅 ↑𝑟 𝑛 ) ) )

Proof

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