Theorem nfchnd

Description: Bound-variable hypothesis builder for chain collection constructor. (Contributed by Ender Ting, 20-Jan-2026)

	Ref	Expression
Hypotheses	nfchnd.1	$$⊢\phi \to \underset{\_}{Ⅎ}x\underset{\dot{}}{<}$$
	nfchnd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
Assertion	nfchnd	$$⊢\phi \to \underset{\_}{Ⅎ}x{\mathrm{Chain}}_A\underset{\dot{}}{<}$$

Proof

Step	Hyp	Ref	Expression
1		nfchnd.1	$$⊢\phi \to \underset{\_}{Ⅎ}x\underset{\dot{}}{<}$$
2		nfchnd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
3		df-chn	$$⊢{\mathrm{Chain}}_A\underset{\dot{}}{<}=\left\{z\in \mathrm{Word}A|\forall n\in \left(\mathrm{dom}z\setminus \left\{0\right\}\right)z\left(n-1\right)\underset{\dot{}}{<}z\left(n\right)\right\}$$
4		df-rab	$$⊢\left\{z\in \mathrm{Word}A|\forall n\in \left(\mathrm{dom}z\setminus \left\{0\right\}\right)z\left(n-1\right)\underset{\dot{}}{<}z\left(n\right)\right\}=\left\{z|\left(z\in \mathrm{Word}A\wedge \forall n\in \left(\mathrm{dom}z\setminus \left\{0\right\}\right)z\left(n-1\right)\underset{\dot{}}{<}z\left(n\right)\right)\right\}$$
5		nfv	$$⊢Ⅎz\phi$$
6		df-word	$$⊢\mathrm{Word}A=\left\{z|\exists n\in {\mathbb{N}}_{0}z:\left(0..^n\right)⟶A\right\}$$
7		nfv	$$⊢Ⅎn\phi$$
8		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}x{\mathbb{N}}_0$$
9		df-f	$$⊢z:\left(0..^n\right)⟶A\leftrightarrow \left(zFn\left(0..^n\right)\wedge \mathrm{ran}z\subseteq A\right)$$
10		df-fn	$$⊢zFn\left(0..^n\right)\leftrightarrow \left(\mathrm{Fun}z\wedge \mathrm{dom}z=\left(0..^n\right)\right)$$
11		df-fun	$$⊢\mathrm{Fun}z\leftrightarrow \left(\mathrm{Rel}z\wedge z\circ z^{-1}\subseteq \mathrm{I}\right)$$
12		df-rel	$$⊢\mathrm{Rel}z\leftrightarrow z\subseteq \mathrm{V}\times \mathrm{V}$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}nz$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}n\left(\mathrm{V}\times \mathrm{V}\right)$$
15	13 14	dfss3f	$$⊢z\subseteq \mathrm{V}\times \mathrm{V}\leftrightarrow \forall n\in zn\in \left(\mathrm{V}\times \mathrm{V}\right)$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
17	16	a1i	$$⊢\phi \to \underset{\_}{Ⅎ}xz$$
18		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(\mathrm{V}\times \mathrm{V}\right)$$
19	18	nfcrd	$$⊢\phi \to Ⅎxn\in \left(\mathrm{V}\times \mathrm{V}\right)$$
20	7 17 19	nfraldw	$$⊢\phi \to Ⅎx\forall n\in zn\in \left(\mathrm{V}\times \mathrm{V}\right)$$
21	15 20	nfxfrd	$$⊢\phi \to Ⅎxz\subseteq \mathrm{V}\times \mathrm{V}$$
22	12 21	nfxfrd	$$⊢\phi \to Ⅎx\mathrm{Rel}z$$
23		nfvd	$$⊢\phi \to Ⅎxz\circ z^{-1}\subseteq \mathrm{I}$$
24	22 23	nfand	$$⊢\phi \to Ⅎx\left(\mathrm{Rel}z\wedge z\circ z^{-1}\subseteq \mathrm{I}\right)$$
25	11 24	nfxfrd	$$⊢\phi \to Ⅎx\mathrm{Fun}z$$
26		nfvd	$$⊢\phi \to Ⅎx\mathrm{dom}z=\left(0..^n\right)$$
27	25 26	nfand	$$⊢\phi \to Ⅎx\left(\mathrm{Fun}z\wedge \mathrm{dom}z=\left(0..^n\right)\right)$$
28	10 27	nfxfrd	$$⊢\phi \to ℲxzFn\left(0..^n\right)$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}n\mathrm{ran}z$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}nA$$
31	29 30	dfss3f	$$⊢\mathrm{ran}z\subseteq A\leftrightarrow \forall n\in \mathrm{ran}zn\in A$$
32		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}x\mathrm{ran}z$$
33	2	nfcrd	$$⊢\phi \to Ⅎxn\in A$$
34	7 32 33	nfraldw	$$⊢\phi \to Ⅎx\forall n\in \mathrm{ran}zn\in A$$
35	31 34	nfxfrd	$$⊢\phi \to Ⅎx\mathrm{ran}z\subseteq A$$
36	28 35	nfand	$$⊢\phi \to Ⅎx\left(zFn\left(0..^n\right)\wedge \mathrm{ran}z\subseteq A\right)$$
37	9 36	nfxfrd	$$⊢\phi \to Ⅎxz:\left(0..^n\right)⟶A$$
38	7 8 37	nfrexdw	$$⊢\phi \to Ⅎx\exists n\in {\mathbb{N}}_{0}z:\left(0..^n\right)⟶A$$
39	5 38	nfabdw	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{z|\exists n\in {\mathbb{N}}_{0}z:\left(0..^n\right)⟶A\right\}$$
40	6 39	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}x\mathrm{Word}A$$
41		nfcr	$$⊢\underset{\_}{Ⅎ}x\mathrm{Word}A\to Ⅎxz\in \mathrm{Word}A$$
42	40 41	syl	$$⊢\phi \to Ⅎxz\in \mathrm{Word}A$$
43		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(\mathrm{dom}z\setminus \left\{0\right\}\right)$$
44		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}xz\left(n-1\right)$$
45		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}xz\left(n\right)$$
46	44 1 45	nfbrd	$$⊢\phi \to Ⅎxz\left(n-1\right)\underset{\dot{}}{<}z\left(n\right)$$
47	7 43 46	nfraldw	$$⊢\phi \to Ⅎx\forall n\in \left(\mathrm{dom}z\setminus \left\{0\right\}\right)z\left(n-1\right)\underset{\dot{}}{<}z\left(n\right)$$
48	42 47	nfand	$$⊢\phi \to Ⅎx\left(z\in \mathrm{Word}A\wedge \forall n\in \left(\mathrm{dom}z\setminus \left\{0\right\}\right)z\left(n-1\right)\underset{\dot{}}{<}z\left(n\right)\right)$$
49	5 48	nfabdw	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{z|\left(z\in \mathrm{Word}A\wedge \forall n\in \left(\mathrm{dom}z\setminus \left\{0\right\}\right)z\left(n-1\right)\underset{\dot{}}{<}z\left(n\right)\right)\right\}$$
50	4 49	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left\{z\in \mathrm{Word}A|\forall n\in \left(\mathrm{dom}z\setminus \left\{0\right\}\right)z\left(n-1\right)\underset{\dot{}}{<}z\left(n\right)\right\}$$
51	3 50	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}x{\mathrm{Chain}}_A\underset{\dot{}}{<}$$