Theorem nfchnd 18546

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

Hypotheses

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

Assertion

Ref	Expression
nfchnd	⊢ (𝜑 → Ⅎ𝑥( < Chain 𝐴))

Proof of Theorem nfchnd

Dummy variables 𝑧 𝑛 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  Ⅎwnf 1785   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ∖ cdif 3900   ⊆ wss 3903  {csn 4582   class class class wbr 5100   I cid 5526   × cxp 5630  ^◡ccnv 5631  dom cdm 5632  ran crn 5633   ∘ ccom 5636  Rel wrel 5637  Fun wfun 6494   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  0cc0 11038  1c1 11039   − cmin 11376  ℕ₀cn0 12413  ..^cfzo 13582  Word cword 14448   Chain cchn 18540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-rel 5639  df-fun 6502  df-fn 6503  df-f 6504  df-word 14449  df-chn 18541

This theorem is referenced by: (None)