Theorem nfttrcl

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

	Ref	Expression
Hypothesis	nfttrcl.1	$$⊢\underset{\_}{Ⅎ}xR$$
Assertion	nfttrcl	$$⊢\underset{\_}{Ⅎ}x\mathrm{t++}R$$

Proof

Step	Hyp	Ref	Expression
1		nfttrcl.1	$$⊢\underset{\_}{Ⅎ}xR$$
2	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xR$$
3	2	nfttrcld	$$⊢\top \to \underset{\_}{Ⅎ}x\mathrm{t++}R$$
4	3	mptru	$$⊢\underset{\_}{Ⅎ}x\mathrm{t++}R$$