Theorem nfchnd 18747

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 18742	. 2 ⊢ ( < Chain 𝐴) = {𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)}
2		df-rab 3413	. . 3 ⊢ {𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)} = {𝑧 ∣ (𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))}
3		nfv 1947	. . . 4 ⊢ Ⅎ𝑧𝜑
4		df-word 14627	. . . . . . 7 ⊢ Word 𝐴 = {𝑧 ∣ ∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴}
5		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑛𝜑
6		nfcvd 2923	. . . . . . . . 9 ⊢ (𝜑 → Ⅎ𝑥ℕ0)
7		df-f 6531	. . . . . . . . . 10 ⊢ (𝑧:(0..^𝑛)⟶𝐴 ↔ (𝑧 Fn (0..^𝑛) ∧ ran 𝑧 ⊆ 𝐴))
8		df-fn 6530	. . . . . . . . . . . 12 ⊢ (𝑧 Fn (0..^𝑛) ↔ (Fun 𝑧 ∧ dom 𝑧 = (0..^𝑛)))
9		df-fun 6529	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑧 ↔ (Rel 𝑧 ∧ (𝑧 ∘ ◡𝑧) ⊆ I ))
10		df-rel 5654	. . . . . . . . . . . . . . . 16 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
11		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑧
12		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(V × V)
13	11, 12	dfss3f 3922	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ (V × V) ↔ ∀𝑛 ∈ 𝑧 𝑛 ∈ (V × V))
14		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝑧
15	14	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → Ⅎ𝑥𝑧)
16		nfcvd 2923	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Ⅎ𝑥(V × V))
17	16	nfcrd 2916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → Ⅎ𝑥 𝑛 ∈ (V × V))
18	5, 15, 17	nfraldw 3307	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ 𝑧 𝑛 ∈ (V × V))
19	13, 18	nfxfrd 1887	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Ⅎ𝑥 𝑧 ⊆ (V × V))
20	10, 19	nfxfrd 1887	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Ⅎ𝑥Rel 𝑧)
21		nfvd 1948	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Ⅎ𝑥(𝑧 ∘ ◡𝑧) ⊆ I )
22	20, 21	nfand 1930	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ⅎ𝑥(Rel 𝑧 ∧ (𝑧 ∘ ◡𝑧) ⊆ I ))
23	9, 22	nfxfrd 1887	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥Fun 𝑧)
24		nfvd 1948	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥dom 𝑧 = (0..^𝑛))
25	23, 24	nfand 1930	. . . . . . . . . . . 12 ⊢ (𝜑 → Ⅎ𝑥(Fun 𝑧 ∧ dom 𝑧 = (0..^𝑛)))
26	8, 25	nfxfrd 1887	. . . . . . . . . . 11 ⊢ (𝜑 → Ⅎ𝑥 𝑧 Fn (0..^𝑛))
27		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛ran 𝑧
28		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝐴
29	27, 28	dfss3f 3922	. . . . . . . . . . . 12 ⊢ (ran 𝑧 ⊆ 𝐴 ↔ ∀𝑛 ∈ ran 𝑧 𝑛 ∈ 𝐴)
30		nfcvd 2923	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥ran 𝑧)
31		nfchnd.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ⅎ𝑥𝐴)
32	31	nfcrd 2916	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥 𝑛 ∈ 𝐴)
33	5, 30, 32	nfraldw 3307	. . . . . . . . . . . 12 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ ran 𝑧 𝑛 ∈ 𝐴)
34	29, 33	nfxfrd 1887	. . . . . . . . . . 11 ⊢ (𝜑 → Ⅎ𝑥ran 𝑧 ⊆ 𝐴)
35	26, 34	nfand 1930	. . . . . . . . . 10 ⊢ (𝜑 → Ⅎ𝑥(𝑧 Fn (0..^𝑛) ∧ ran 𝑧 ⊆ 𝐴))
36	7, 35	nfxfrd 1887	. . . . . . . . 9 ⊢ (𝜑 → Ⅎ𝑥 𝑧:(0..^𝑛)⟶𝐴)
37	5, 6, 36	nfrexdw 3308	. . . . . . . 8 ⊢ (𝜑 → Ⅎ𝑥∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴)
38	3, 37	nfabdw 2943	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∣ ∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴})
39	4, 38	nfcxfrd 2921	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥Word 𝐴)
40		nfcr 2912	. . . . . 6 ⊢ (Ⅎ𝑥Word 𝐴 → Ⅎ𝑥 𝑧 ∈ Word 𝐴)
41	39, 40	syl 18	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥 𝑧 ∈ Word 𝐴)
42		nfcvd 2923	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥(dom 𝑧 ∖ {0}))
43		nfcvd 2923	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘(𝑛 − 1)))
44		nfchnd.1	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥 < )
45		nfcvd 2923	. . . . . . 7 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘𝑛))
46	43, 44, 45	nfbrd 5150	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))
47	5, 42, 46	nfraldw 3307	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))
48	41, 47	nfand 1930	. . . 4 ⊢ (𝜑 → Ⅎ𝑥(𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)))
49	3, 48	nfabdw 2943	. . 3 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∣ (𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))})
50	2, 49	nfcxfrd 2921	. 2 ⊢ (𝜑 → Ⅎ𝑥{𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)})
51	1, 50	nfcxfrd 2921	1 ⊢ (𝜑 → Ⅎ𝑥( < Chain 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  {cab 2738  Ⅎwnfc 2907  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ∖ cdif 3895   ⊆ wss 3898  {csn 4583   class class class wbr 5102   I cid 5541   × cxp 5645  ^◡ccnv 5646  dom cdm 5647  ran crn 5648   ∘ ccom 5651  Rel wrel 5652  Fun wfun 6521   Fn wfn 6522  ⟶wf 6523  ‘cfv 6527  (class class class)co 7408  0cc0 11172  1c1 11173   − cmin 11513  ℕ₀cn0 12576  ..^cfzo 13757  Word cword 14626   Chain cchn 18741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rel 5654  df-fun 6529  df-fn 6530  df-f 6531  df-word 14627  df-chn 18742

This theorem is used by: (None)