Metamath Proof Explorer

Theorem eltrclrec

Description: Membership in the indexed union of relation exponentiation over the natural numbers 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	trclrec.def	$⊢ C = (r \in V ⟼ ⋃_{n \in ℕ} (r ↑_{r} n))$
	Assertion	eltrclrec	$⊢ R \in V \to (X \in C (R) \leftrightarrow \exists n \in ℕ X \in (R ↑_{r} n))$

Proof

Step	Hyp	Ref	Expression
1		trclrec.def	$⊢ C = (r \in V ⟼ ⋃_{n \in ℕ} (r ↑_{r} n))$
2		nnex	$⊢ ℕ \in V$
3	1	eliunov2	$⊢ (R \in V \land ℕ \in V) \to (X \in C (R) \leftrightarrow \exists n \in ℕ X \in (R ↑_{r} n))$
4	2 3	mpan2	$⊢ R \in V \to (X \in C (R) \leftrightarrow \exists n \in ℕ X \in (R ↑_{r} n))$