Theorem nfttrcld

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

	Ref	Expression
Hypothesis	nfttrcld.1	$$⊢\phi \to \underset{\_}{Ⅎ}xR$$
Assertion	nfttrcld	Could not format assertion : No typesetting found for |- ( ph -> F/_ x t++ R ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nfttrcld.1	$$⊢\phi \to \underset{\_}{Ⅎ}xR$$
2		df-ttrcl	Could not format t++ R = { <. y , z >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = y /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } : No typesetting found for |- t++ R = { <. y , z >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = y /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } with typecode |-
3		nfv	$$⊢Ⅎy\phi$$
4		nfv	$$⊢Ⅎz\phi$$
5		nfv	$$⊢Ⅎn\phi$$
6		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(\mathrm{\omega }\setminus 1_{𝑜}\right)$$
7		nfv	$$⊢Ⅎf\phi$$
8		nfvd	$$⊢\phi \to ℲxfFn\mathrm{suc}n$$
9		nfvd	$$⊢\phi \to Ⅎx\left(f\left(\varnothing \right)=y\wedge f\left(n\right)=z\right)$$
10		nfv	$$⊢Ⅎa\phi$$
11		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}xn$$
12		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}xf\left(a\right)$$
13		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}xf\left(\mathrm{suc}a\right)$$
14	12 1 13	nfbrd	$$⊢\phi \to Ⅎxf\left(a\right)Rf\left(\mathrm{suc}a\right)$$
15	10 11 14	nfraldw	$$⊢\phi \to Ⅎx\forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)$$
16	8 9 15	nf3and	$$⊢\phi \to Ⅎx\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=y\wedge f\left(n\right)=z\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)$$
17	7 16	nfexd	$$⊢\phi \to Ⅎx\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=y\wedge f\left(n\right)=z\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)$$
18	5 6 17	nfrexd	$$⊢\phi \to Ⅎx\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=y\wedge f\left(n\right)=z\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)$$
19	3 4 18	nfopabd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{⟨y,z⟩|\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=y\wedge f\left(n\right)=z\right)\wedge \forall a\in nf\left(a\right)Rf\left(\mathrm{suc}a\right)\right)\right\}$$
20	2 19	nfcxfrd	Could not format ( ph -> F/_ x t++ R ) : No typesetting found for |- ( ph -> F/_ x t++ R ) with typecode |-