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	$⊢ C = (r \in V ⟼ ⋃_{n \in ℕ} (r ↑_{r} n))$
	Assertion	brtrclrec	$⊢ R \in V \to (X C (R) Y \leftrightarrow \exists n \in ℕ X (R ↑_{r} n) Y)$

Proof

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