Theorem nfchnd 18657

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 18652	. 2 ⊢ ( < Chain 𝐴) = {𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)}
2		df-rab 3418	. . 3 ⊢ {𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)} = {𝑧 ∣ (𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))}
3		nfv 1937	. . . 4 ⊢ Ⅎ𝑧𝜑
4		df-word 14541	. . . . . . 7 ⊢ Word 𝐴 = {𝑧 ∣ ∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴}
5		nfv 1937	. . . . . . . . 9 ⊢ Ⅎ𝑛𝜑
6		nfcvd 2928	. . . . . . . . 9 ⊢ (𝜑 → Ⅎ𝑥ℕ0)
7		df-f 6529	. . . . . . . . . 10 ⊢ (𝑧:(0..^𝑛)⟶𝐴 ↔ (𝑧 Fn (0..^𝑛) ∧ ran 𝑧 ⊆ 𝐴))
8		df-fn 6528	. . . . . . . . . . . 12 ⊢ (𝑧 Fn (0..^𝑛) ↔ (Fun 𝑧 ∧ dom 𝑧 = (0..^𝑛)))
9		df-fun 6527	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑧 ↔ (Rel 𝑧 ∧ (𝑧 ∘ ◡𝑧) ⊆ I ))
10		df-rel 5659	. . . . . . . . . . . . . . . 16 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
11		nfcv 2927	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑧
12		nfcv 2927	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(V × V)
13	11, 12	dfss3f 3931	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ (V × V) ↔ ∀𝑛 ∈ 𝑧 𝑛 ∈ (V × V))
14		nfcv 2927	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝑧
15	14	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → Ⅎ𝑥𝑧)
16		nfcvd 2928	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Ⅎ𝑥(V × V))
17	16	nfcrd 2921	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → Ⅎ𝑥 𝑛 ∈ (V × V))
18	5, 15, 17	nfraldw 3310	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ 𝑧 𝑛 ∈ (V × V))
19	13, 18	nfxfrd 1877	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Ⅎ𝑥 𝑧 ⊆ (V × V))
20	10, 19	nfxfrd 1877	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Ⅎ𝑥Rel 𝑧)
21		nfvd 1938	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Ⅎ𝑥(𝑧 ∘ ◡𝑧) ⊆ I )
22	20, 21	nfand 1920	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ⅎ𝑥(Rel 𝑧 ∧ (𝑧 ∘ ◡𝑧) ⊆ I ))
23	9, 22	nfxfrd 1877	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥Fun 𝑧)
24		nfvd 1938	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥dom 𝑧 = (0..^𝑛))
25	23, 24	nfand 1920	. . . . . . . . . . . 12 ⊢ (𝜑 → Ⅎ𝑥(Fun 𝑧 ∧ dom 𝑧 = (0..^𝑛)))
26	8, 25	nfxfrd 1877	. . . . . . . . . . 11 ⊢ (𝜑 → Ⅎ𝑥 𝑧 Fn (0..^𝑛))
27		nfcv 2927	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛ran 𝑧
28		nfcv 2927	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝐴
29	27, 28	dfss3f 3931	. . . . . . . . . . . 12 ⊢ (ran 𝑧 ⊆ 𝐴 ↔ ∀𝑛 ∈ ran 𝑧 𝑛 ∈ 𝐴)
30		nfcvd 2928	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥ran 𝑧)
31		nfchnd.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ⅎ𝑥𝐴)
32	31	nfcrd 2921	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥 𝑛 ∈ 𝐴)
33	5, 30, 32	nfraldw 3310	. . . . . . . . . . . 12 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ ran 𝑧 𝑛 ∈ 𝐴)
34	29, 33	nfxfrd 1877	. . . . . . . . . . 11 ⊢ (𝜑 → Ⅎ𝑥ran 𝑧 ⊆ 𝐴)
35	26, 34	nfand 1920	. . . . . . . . . 10 ⊢ (𝜑 → Ⅎ𝑥(𝑧 Fn (0..^𝑛) ∧ ran 𝑧 ⊆ 𝐴))
36	7, 35	nfxfrd 1877	. . . . . . . . 9 ⊢ (𝜑 → Ⅎ𝑥 𝑧:(0..^𝑛)⟶𝐴)
37	5, 6, 36	nfrexdw 3311	. . . . . . . 8 ⊢ (𝜑 → Ⅎ𝑥∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴)
38	3, 37	nfabdw 2948	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∣ ∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴})
39	4, 38	nfcxfrd 2926	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥Word 𝐴)
40		nfcr 2917	. . . . . 6 ⊢ (Ⅎ𝑥Word 𝐴 → Ⅎ𝑥 𝑧 ∈ Word 𝐴)
41	39, 40	syl 18	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥 𝑧 ∈ Word 𝐴)
42		nfcvd 2928	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥(dom 𝑧 ∖ {0}))
43		nfcvd 2928	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘(𝑛 − 1)))
44		nfchnd.1	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥 < )
45		nfcvd 2928	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘𝑛))
46	43, 44, 45	nfbrd 5151	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))
47	5, 42, 46	nfraldw 3310	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))
48	41, 47	nfand 1920	. . . 4 ⊢ (𝜑 → Ⅎ𝑥(𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)))
49	3, 48	nfabdw 2948	. . 3 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∣ (𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))})
50	2, 49	nfcxfrd 2926	. 2 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)})
51	1, 50	nfcxfrd 2926	1 ⊢ (𝜑 → Ⅎ𝑥( < Chain 𝐴))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563  Ⅎwnf 1806   ∈ wcel 2145  {cab 2743  Ⅎwnfc 2912  ∀wral 3079  ∃wrex 3089  {crab 3417  Vcvv 3457   ∖ cdif 3904   ⊆ wss 3907  {csn 4585   class class class wbr 5105   I cid 5546   × cxp 5650  ^◡ccnv 5651  dom cdm 5652  ran crn 5653   ∘ ccom 5656  Rel wrel 5657  Fun wfun 6519   Fn wfn 6520  ⟶wf 6521  ‘cfv 6525  (class class class)co 7400  0cc0 11088  1c1 11089   − cmin 11429  ℕ₀cn0 12495  ..^cfzo 13673  Word cword 14540   Chain cchn 18651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-rel 5659  df-fun 6527  df-fn 6528  df-f 6529  df-word 14541  df-chn 18652

This theorem is referenced by: (None)