Theorem nfttc

Description: Bound-variable hypothesis builder for transitive closure. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Hypothesis	nfttc.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfttc	Could not format assertion : No typesetting found for |- F/_ x TC+ A with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nfttc.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		df-ttc	Could not format TC+ A = U_ y e. A U. ( rec ( ( z e. _V |-> U. z ) , { y } ) " _om ) : No typesetting found for |- TC+ A = U_ y e. A U. ( rec ( ( z e. _V |-> U. z ) , { y } ) " _om ) with typecode |-
3		nfcv	$$⊢\underset{\_}{Ⅎ}x\bigcup \mathrm{rec}\left(\left(z\in \mathrm{V}⟼\bigcup z\right),\left\{y\right\}\right)\left[\mathrm{\omega }\right]$$
4	1 3	nfiun	$$⊢\underset{\_}{Ⅎ}x\bigcup _{y\in A}\bigcup \mathrm{rec}\left(\left(z\in \mathrm{V}⟼\bigcup z\right),\left\{y\right\}\right)\left[\mathrm{\omega }\right]$$
5	2 4	nfcxfr	Could not format F/_ x TC+ A : No typesetting found for |- F/_ x TC+ A with typecode |-