Theorem nfchnd

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

	Ref	Expression
Hypotheses	nfchnd.1	⊢ ( 𝜑 → Ⅎ 𝑥 < )
	nfchnd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nfchnd	⊢ ( 𝜑 → Ⅎ 𝑥 ( < Chain 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nfchnd.1	⊢ ( 𝜑 → Ⅎ 𝑥 < )
2		nfchnd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
3		df-chn	⊢ ( < Chain 𝐴 ) = { 𝑧 ∈ Word 𝐴 ∣ ∀ 𝑛 ∈ ( dom 𝑧 ∖ { 0 } ) ( 𝑧 ‘ ( 𝑛 − 1 ) ) < ( 𝑧 ‘ 𝑛 ) }
4		df-rab	⊢ { 𝑧 ∈ Word 𝐴 ∣ ∀ 𝑛 ∈ ( dom 𝑧 ∖ { 0 } ) ( 𝑧 ‘ ( 𝑛 − 1 ) ) < ( 𝑧 ‘ 𝑛 ) } = { 𝑧 ∣ ( 𝑧 ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom 𝑧 ∖ { 0 } ) ( 𝑧 ‘ ( 𝑛 − 1 ) ) < ( 𝑧 ‘ 𝑛 ) ) }
5		nfv	⊢ Ⅎ 𝑧 𝜑
6		df-word	⊢ Word 𝐴 = { 𝑧 ∣ ∃ 𝑛 ∈ ℕ0 𝑧 : ( 0 ..^ 𝑛 ) ⟶ 𝐴 }
7		nfv	⊢ Ⅎ 𝑛 𝜑
8		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ℕ0 )
9		df-f	⊢ ( 𝑧 : ( 0 ..^ 𝑛 ) ⟶ 𝐴 ↔ ( 𝑧 Fn ( 0 ..^ 𝑛 ) ∧ ran 𝑧 ⊆ 𝐴 ) )
10		df-fn	⊢ ( 𝑧 Fn ( 0 ..^ 𝑛 ) ↔ ( Fun 𝑧 ∧ dom 𝑧 = ( 0 ..^ 𝑛 ) ) )
11		df-fun	⊢ ( Fun 𝑧 ↔ ( Rel 𝑧 ∧ ( 𝑧 ∘ ◡ 𝑧 ) ⊆ I ) )
12		df-rel	⊢ ( Rel 𝑧 ↔ 𝑧 ⊆ ( V × V ) )
13		nfcv	⊢ Ⅎ 𝑛 𝑧
14		nfcv	⊢ Ⅎ 𝑛 ( V × V )
15	13 14	dfss3f	⊢ ( 𝑧 ⊆ ( V × V ) ↔ ∀ 𝑛 ∈ 𝑧 𝑛 ∈ ( V × V ) )
16		nfcv	⊢ Ⅎ 𝑥 𝑧
17	16	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 )
18		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( V × V ) )
19	18	nfcrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑛 ∈ ( V × V ) )
20	7 17 19	nfraldw	⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑛 ∈ 𝑧 𝑛 ∈ ( V × V ) )
21	15 20	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 ⊆ ( V × V ) )
22	12 21	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 Rel 𝑧 )
23		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑧 ∘ ◡ 𝑧 ) ⊆ I )
24	22 23	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( Rel 𝑧 ∧ ( 𝑧 ∘ ◡ 𝑧 ) ⊆ I ) )
25	11 24	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 Fun 𝑧 )
26		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 dom 𝑧 = ( 0 ..^ 𝑛 ) )
27	25 26	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( Fun 𝑧 ∧ dom 𝑧 = ( 0 ..^ 𝑛 ) ) )
28	10 27	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 Fn ( 0 ..^ 𝑛 ) )
29		nfcv	⊢ Ⅎ 𝑛 ran 𝑧
30		nfcv	⊢ Ⅎ 𝑛 𝐴
31	29 30	dfss3f	⊢ ( ran 𝑧 ⊆ 𝐴 ↔ ∀ 𝑛 ∈ ran 𝑧 𝑛 ∈ 𝐴 )
32		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ran 𝑧 )
33	2	nfcrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑛 ∈ 𝐴 )
34	7 32 33	nfraldw	⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑛 ∈ ran 𝑧 𝑛 ∈ 𝐴 )
35	31 34	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ran 𝑧 ⊆ 𝐴 )
36	28 35	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑧 Fn ( 0 ..^ 𝑛 ) ∧ ran 𝑧 ⊆ 𝐴 ) )
37	9 36	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 : ( 0 ..^ 𝑛 ) ⟶ 𝐴 )
38	7 8 37	nfrexdw	⊢ ( 𝜑 → Ⅎ 𝑥 ∃ 𝑛 ∈ ℕ0 𝑧 : ( 0 ..^ 𝑛 ) ⟶ 𝐴 )
39	5 38	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑧 ∣ ∃ 𝑛 ∈ ℕ0 𝑧 : ( 0 ..^ 𝑛 ) ⟶ 𝐴 } )
40	6 39	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 Word 𝐴 )
41		nfcr	⊢ ( Ⅎ 𝑥 Word 𝐴 → Ⅎ 𝑥 𝑧 ∈ Word 𝐴 )
42	40 41	syl	⊢ ( 𝜑 → Ⅎ 𝑥 𝑧 ∈ Word 𝐴 )
43		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( dom 𝑧 ∖ { 0 } ) )
44		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑧 ‘ ( 𝑛 − 1 ) ) )
45		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑧 ‘ 𝑛 ) )
46	44 1 45	nfbrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑧 ‘ ( 𝑛 − 1 ) ) < ( 𝑧 ‘ 𝑛 ) )
47	7 43 46	nfraldw	⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑛 ∈ ( dom 𝑧 ∖ { 0 } ) ( 𝑧 ‘ ( 𝑛 − 1 ) ) < ( 𝑧 ‘ 𝑛 ) )
48	42 47	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑧 ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom 𝑧 ∖ { 0 } ) ( 𝑧 ‘ ( 𝑛 − 1 ) ) < ( 𝑧 ‘ 𝑛 ) ) )
49	5 48	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑧 ∣ ( 𝑧 ∈ Word 𝐴 ∧ ∀ 𝑛 ∈ ( dom 𝑧 ∖ { 0 } ) ( 𝑧 ‘ ( 𝑛 − 1 ) ) < ( 𝑧 ‘ 𝑛 ) ) } )
50	4 49	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑧 ∈ Word 𝐴 ∣ ∀ 𝑛 ∈ ( dom 𝑧 ∖ { 0 } ) ( 𝑧 ‘ ( 𝑛 − 1 ) ) < ( 𝑧 ‘ 𝑛 ) } )
51	3 50	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( < Chain 𝐴 ) )