Theorem nfchnd 18786

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 18781	. 2 ⊢ ( < Chain 𝐴) = {𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)}
2		df-rab 3413	. . 3 ⊢ {𝑧 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛)} = {𝑧 ∣ (𝑧 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝑧 ∖ {0})(𝑧‘(𝑛 − 1)) < (𝑧‘𝑛))}
3		nfv 1946	. . . 4 ⊢ Ⅎ𝑧𝜑
4		df-word 14660	. . . . . . 7 ⊢ Word 𝐴 = {𝑧 ∣ ∃𝑛 ∈ ℕ0 𝑧:(0..^𝑛)⟶𝐴}
5		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑛𝜑
6		nfcvd 2923	. . . . . . . . 9 ⊢ (𝜑 → Ⅎ𝑥ℕ0)
7		df-f 6542	. . . . . . . . . 10 ⊢ (𝑧:(0..^𝑛)⟶𝐴 ↔ (𝑧 Fn (0..^𝑛) ∧ ran 𝑧 ⊆ 𝐴))
8		df-fn 6541	. . . . . . . . . . . 12 ⊢ (𝑧 Fn (0..^𝑛) ↔ (Fun 𝑧 ∧ dom 𝑧 = (0..^𝑛)))
9		df-fun 6540	. . . . . . . . . . . . . 14 ⊢ (Fun 𝑧 ↔ (Rel 𝑧 ∧ (𝑧 ∘ ◡𝑧) ⊆ I ))
10		df-rel 5657	. . . . . . . . . . . . . . . 16 ⊢ (Rel 𝑧 ↔ 𝑧 ⊆ (V × V))
11		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛𝑧
12		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑛(V × V)
13	11, 12	dfss3f 3900	. . . . . . . . . . . . . . . . 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 1886	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Ⅎ𝑥 𝑧 ⊆ (V × V))
20	10, 19	nfxfrd 1886	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Ⅎ𝑥Rel 𝑧)
21		nfvd 1947	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Ⅎ𝑥(𝑧 ∘ ◡𝑧) ⊆ I )
22	20, 21	nfand 1929	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ⅎ𝑥(Rel 𝑧 ∧ (𝑧 ∘ ◡𝑧) ⊆ I ))
23	9, 22	nfxfrd 1886	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥Fun 𝑧)
24		nfvd 1947	. . . . . . . . . . . . 13 ⊢ (𝜑 → Ⅎ𝑥dom 𝑧 = (0..^𝑛))
25	23, 24	nfand 1929	. . . . . . . . . . . 12 ⊢ (𝜑 → Ⅎ𝑥(Fun 𝑧 ∧ dom 𝑧 = (0..^𝑛)))
26	8, 25	nfxfrd 1886	. . . . . . . . . . 11 ⊢ (𝜑 → Ⅎ𝑥 𝑧 Fn (0..^𝑛))
27		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛ran 𝑧
28		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝐴
29	27, 28	dfss3f 3900	. . . . . . . . . . . 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 1886	. . . . . . . . . . 11 ⊢ (𝜑 → Ⅎ𝑥ran 𝑧 ⊆ 𝐴)
35	26, 34	nfand 1929	. . . . . . . . . 10 ⊢ (𝜑 → Ⅎ𝑥(𝑧 Fn (0..^𝑛) ∧ ran 𝑧 ⊆ 𝐴))
36	7, 35	nfxfrd 1886	. . . . . . . . 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 1929	. . . 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 1569  Ⅎwnf 1815   ∈ wcel 2144  {cab 2738  Ⅎwnfc 2907  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3895   ∖ cdif 4045  {csn 4583   class class class wbr 5102   I cid 5544   × cxp 5648  ^◡ccnv 5649  dom cdm 5650  ran crn 5651   ∘ ccom 5654  Rel wrel 5655  Fun wfun 6532   Fn wfn 6533  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420  0cc0 11201  1c1 11202   − cmin 11542  ℕ₀cn0 12607  ..^cfzo 13789  Word cword 14659   Chain cchn 18780

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-rel 5657  df-fun 6540  df-fn 6541  df-f 6542  df-word 14660  df-chn 18781

This theorem is used by: (None)