Theorem brfvtrcld

Description: If two elements are connected by the transitive closure of a relation, then they are connected via n instances the relation, for some counting number n . (Contributed by RP, 22-Jul-2020)

	Ref	Expression
Hypothesis	brfvtrcld.r	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	brfvtrcld	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)B\leftrightarrow \exists n\in \mathbb{N}A\left(R{\uparrow }_{r}n\right)B\right)$$

Proof

Step	Hyp	Ref	Expression
1		brfvtrcld.r	$$⊢\phi \to R\in \mathrm{V}$$
2		dftrcl3	$$⊢\mathrm{t+}=\left(r\in \mathrm{V}⟼\bigcup _{n\in \mathbb{N}}\left(r{\uparrow }_{r}n\right)\right)$$
3		nnssnn0	$$⊢\mathbb{N}\subseteq {\mathbb{N}}_0$$
4	3	a1i	$$⊢\phi \to \mathbb{N}\subseteq {\mathbb{N}}_0$$
5	2 1 4	brmptiunrelexpd	$$⊢\phi \to \left(A\mathrm{t+}\left(R\right)B\leftrightarrow \exists n\in \mathbb{N}A\left(R{\uparrow }_{r}n\right)B\right)$$