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	⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion	brfvtrcld	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brfvtrcld.r	⊢ ( 𝜑 → 𝑅 ∈ V )
2		dftrcl3	⊢ t+ = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) )
3		nnssnn0	⊢ ℕ ⊆ ℕ0
4	3	a1i	⊢ ( 𝜑 → ℕ ⊆ ℕ0 )
5	2 1 4	brmptiunrelexpd	⊢ ( 𝜑 → ( 𝐴 ( t+ ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )