Theorem nfttrcl

Description: Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Hypothesis	nfttrcl.1	⊢ Ⅎ 𝑥 𝑅
Assertion	nfttrcl	⊢ Ⅎ 𝑥 t++ 𝑅

Proof

Step	Hyp	Ref	Expression
1		nfttrcl.1	⊢ Ⅎ 𝑥 𝑅
2	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝑅 )
3	2	nfttrcld	⊢ ( ⊤ → Ⅎ 𝑥 t++ 𝑅 )
4	3	mptru	⊢ Ⅎ 𝑥 t++ 𝑅