Theorem nfchnd 18619

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 18614	. 2 ⊢ ( < Chain 𝐴) = {𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)}
2		df-rab 3409	. . 3 ⊢ {𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)} = {𝑧 ∣ (𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))}
3		nfv 1928	. . . 4 ⊢ Ⅎ𝑧𝜑
4		df-word 14517	. . . . . . 7 ⊢ Word 𝐴 = {𝑧 ∣ ∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴}
5		nfv 1928	. . . . . . . . 9 ⊢ Ⅎ𝑛𝜑
6		nfcvd 2919	. . . . . . . . 9 ⊢ (𝜑 → Ⅎ𝑥ℕ0)
7		df-f 6514	. . . . . . . . . 10 ⊢ (𝑧:(0..^𝑛)⟶𝐴 ↔ (𝑧 Fn (0..^𝑛) ∧ ran 𝑧 ⊆ 𝐴))
8		df-fn 6513	. . . . . . . . . . . 12 ⊢ (𝑧 Fn (0..^𝑛) ↔ (Fun 𝑧 ∧ dom 𝑧 = (0..^𝑛)))
9		df-fun 6512	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑧 ↔ (Rel 𝑧 ∧ (𝑧 ∘ ◡𝑧) ⊆ I ))
10		df-rel 5647	. . . . . . . . . . . . . . . 16 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
11		nfcv 2918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑧
12		nfcv 2918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(V × V)
13	11, 12	dfss3f 3923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ (V × V) ↔ ∀𝑛 ∈ 𝑧 𝑛 ∈ (V × V))
14		nfcv 2918	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝑧
15	14	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → Ⅎ𝑥𝑧)
16		nfcvd 2919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Ⅎ𝑥(V × V))
17	16	nfcrd 2912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → Ⅎ𝑥 𝑛 ∈ (V × V))
18	5, 15, 17	nfraldw 3301	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ 𝑧 𝑛 ∈ (V × V))
19	13, 18	nfxfrd 1868	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Ⅎ𝑥 𝑧 ⊆ (V × V))
20	10, 19	nfxfrd 1868	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Ⅎ𝑥Rel 𝑧)
21		nfvd 1929	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Ⅎ𝑥(𝑧 ∘ ◡𝑧) ⊆ I )
22	20, 21	nfand 1911	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ⅎ𝑥(Rel 𝑧 ∧ (𝑧 ∘ ◡𝑧) ⊆ I ))
23	9, 22	nfxfrd 1868	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥Fun 𝑧)
24		nfvd 1929	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥dom 𝑧 = (0..^𝑛))
25	23, 24	nfand 1911	. . . . . . . . . . . 12 ⊢ (𝜑 → Ⅎ𝑥(Fun 𝑧 ∧ dom 𝑧 = (0..^𝑛)))
26	8, 25	nfxfrd 1868	. . . . . . . . . . 11 ⊢ (𝜑 → Ⅎ𝑥 𝑧 Fn (0..^𝑛))
27		nfcv 2918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛ran 𝑧
28		nfcv 2918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝐴
29	27, 28	dfss3f 3923	. . . . . . . . . . . 12 ⊢ (ran 𝑧 ⊆ 𝐴 ↔ ∀𝑛 ∈ ran 𝑧 𝑛 ∈ 𝐴)
30		nfcvd 2919	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥ran 𝑧)
31		nfchnd.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ⅎ𝑥𝐴)
32	31	nfcrd 2912	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥 𝑛 ∈ 𝐴)
33	5, 30, 32	nfraldw 3301	. . . . . . . . . . . 12 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ ran 𝑧 𝑛 ∈ 𝐴)
34	29, 33	nfxfrd 1868	. . . . . . . . . . 11 ⊢ (𝜑 → Ⅎ𝑥ran 𝑧 ⊆ 𝐴)
35	26, 34	nfand 1911	. . . . . . . . . 10 ⊢ (𝜑 → Ⅎ𝑥(𝑧 Fn (0..^𝑛) ∧ ran 𝑧 ⊆ 𝐴))
36	7, 35	nfxfrd 1868	. . . . . . . . 9 ⊢ (𝜑 → Ⅎ𝑥 𝑧:(0..^𝑛)⟶𝐴)
37	5, 6, 36	nfrexdw 3302	. . . . . . . 8 ⊢ (𝜑 → Ⅎ𝑥∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴)
38	3, 37	nfabdw 2939	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∣ ∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴})
39	4, 38	nfcxfrd 2917	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥Word 𝐴)
40		nfcr 2908	. . . . . 6 ⊢ (Ⅎ𝑥Word 𝐴 → Ⅎ𝑥 𝑧 ∈ Word 𝐴)
41	39, 40	syl 17	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥 𝑧 ∈ Word 𝐴)
42		nfcvd 2919	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥(dom 𝑧 ∖ {0}))
43		nfcvd 2919	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘(𝑛 − 1)))
44		nfchnd.1	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥 < )
45		nfcvd 2919	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘𝑛))
46	43, 44, 45	nfbrd 5140	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))
47	5, 42, 46	nfraldw 3301	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))
48	41, 47	nfand 1911	. . . 4 ⊢ (𝜑 → Ⅎ𝑥(𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)))
49	3, 48	nfabdw 2939	. . 3 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∣ (𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))})
50	2, 49	nfcxfrd 2917	. 2 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)})
51	1, 50	nfcxfrd 2917	1 ⊢ (𝜑 → Ⅎ𝑥( < Chain 𝐴))

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1554  Ⅎwnf 1797   ∈ wcel 2136  {cab 2734  Ⅎwnfc 2903  ∀wral 3070  ∃wrex 3080  {crab 3408  Vcvv 3448   ∖ cdif 3896   ⊆ wss 3899  {csn 4576   class class class wbr 5094   I cid 5534   × cxp 5638  ^◡ccnv 5639  dom cdm 5640  ran crn 5641   ∘ ccom 5644  Rel wrel 5645  Fun wfun 6504   Fn wfn 6505  ⟶wf 6506  ‘cfv 6510  (class class class)co 7385  0cc0 11063  1c1 11064   − cmin 11404  ℕ₀cn0 12471  ..^cfzo 13649  Word cword 14516   Chain cchn 18613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-br 5095  df-rel 5647  df-fun 6512  df-fn 6513  df-f 6514  df-word 14517  df-chn 18614

This theorem is referenced by: (None)