Metamath Proof Explorer

Theorem nfchnd

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

Ref Expression
Hypotheses nfchnd.1 
|- ( ph -> F/_ x .< )
nfchnd.2 
|- ( ph -> F/_ x A )
Assertion nfchnd 
|- ( ph -> F/_ x ( .< Chain A ) )

Proof

Step Hyp Ref Expression
1 nfchnd.1 
 |-  ( ph -> F/_ x .< )
2 nfchnd.2 
 |-  ( ph -> F/_ x A )
3 df-chn 
 |-  ( .< Chain A ) = { z e. Word A | A. n e. ( dom z \ { 0 } ) ( z ` ( n - 1 ) ) .< ( z ` n ) }
4 df-rab 
 |-  { z e. Word A | A. n e. ( dom z \ { 0 } ) ( z ` ( n - 1 ) ) .< ( z ` n ) } = { z | ( z e. Word A /\ A. n e. ( dom z \ { 0 } ) ( z ` ( n - 1 ) ) .< ( z ` n ) ) }
5 nfv 
 |-  F/ z ph
6 df-word 
 |-  Word A = { z | E. n e. NN0 z : ( 0 ..^ n ) --> A }
7 nfv 
 |-  F/ n ph
8 nfcvd 
 |-  ( ph -> F/_ x NN0 )
9 df-f 
 |-  ( z : ( 0 ..^ n ) --> A <-> ( z Fn ( 0 ..^ n ) /\ ran z C_ A ) )
10 df-fn 
 |-  ( z Fn ( 0 ..^ n ) <-> ( Fun z /\ dom z = ( 0 ..^ n ) ) )
11 df-fun 
 |-  ( Fun z <-> ( Rel z /\ ( z o. `' z ) C_ _I ) )
12 df-rel 
 |-  ( Rel z <-> z C_ ( _V X. _V ) )
13 nfcv 
 |-  F/_ n z
14 nfcv 
 |-  F/_ n ( _V X. _V )
15 13 14 dfss3f 
 |-  ( z C_ ( _V X. _V ) <-> A. n e. z n e. ( _V X. _V ) )
16 nfcv 
 |-  F/_ x z
17 16 a1i 
 |-  ( ph -> F/_ x z )
18 nfcvd 
 |-  ( ph -> F/_ x ( _V X. _V ) )
19 18 nfcrd 
 |-  ( ph -> F/ x n e. ( _V X. _V ) )
20 7 17 19 nfraldw 
 |-  ( ph -> F/ x A. n e. z n e. ( _V X. _V ) )
21 15 20 nfxfrd 
 |-  ( ph -> F/ x z C_ ( _V X. _V ) )
22 12 21 nfxfrd 
 |-  ( ph -> F/ x Rel z )
23 nfvd 
 |-  ( ph -> F/ x ( z o. `' z ) C_ _I )
24 22 23 nfand 
 |-  ( ph -> F/ x ( Rel z /\ ( z o. `' z ) C_ _I ) )
25 11 24 nfxfrd 
 |-  ( ph -> F/ x Fun z )
26 nfvd 
 |-  ( ph -> F/ x dom z = ( 0 ..^ n ) )
27 25 26 nfand 
 |-  ( ph -> F/ x ( Fun z /\ dom z = ( 0 ..^ n ) ) )
28 10 27 nfxfrd 
 |-  ( ph -> F/ x z Fn ( 0 ..^ n ) )
29 nfcv 
 |-  F/_ n ran z
30 nfcv 
 |-  F/_ n A
31 29 30 dfss3f 
 |-  ( ran z C_ A <-> A. n e. ran z n e. A )
32 nfcvd 
 |-  ( ph -> F/_ x ran z )
33 2 nfcrd 
 |-  ( ph -> F/ x n e. A )
34 7 32 33 nfraldw 
 |-  ( ph -> F/ x A. n e. ran z n e. A )
35 31 34 nfxfrd 
 |-  ( ph -> F/ x ran z C_ A )
36 28 35 nfand 
 |-  ( ph -> F/ x ( z Fn ( 0 ..^ n ) /\ ran z C_ A ) )
37 9 36 nfxfrd 
 |-  ( ph -> F/ x z : ( 0 ..^ n ) --> A )
38 7 8 37 nfrexdw 
 |-  ( ph -> F/ x E. n e. NN0 z : ( 0 ..^ n ) --> A )
39 5 38 nfabdw 
 |-  ( ph -> F/_ x { z | E. n e. NN0 z : ( 0 ..^ n ) --> A } )
40 6 39 nfcxfrd 
 |-  ( ph -> F/_ x Word A )
41 nfcr 
 |-  ( F/_ x Word A -> F/ x z e. Word A )
42 40 41 syl 
 |-  ( ph -> F/ x z e. Word A )
43 nfcvd 
 |-  ( ph -> F/_ x ( dom z \ { 0 } ) )
44 nfcvd 
 |-  ( ph -> F/_ x ( z ` ( n - 1 ) ) )
45 nfcvd 
 |-  ( ph -> F/_ x ( z ` n ) )
46 44 1 45 nfbrd 
 |-  ( ph -> F/ x ( z ` ( n - 1 ) ) .< ( z ` n ) )
47 7 43 46 nfraldw 
 |-  ( ph -> F/ x A. n e. ( dom z \ { 0 } ) ( z ` ( n - 1 ) ) .< ( z ` n ) )
48 42 47 nfand 
 |-  ( ph -> F/ x ( z e. Word A /\ A. n e. ( dom z \ { 0 } ) ( z ` ( n - 1 ) ) .< ( z ` n ) ) )
49 5 48 nfabdw 
 |-  ( ph -> F/_ x { z | ( z e. Word A /\ A. n e. ( dom z \ { 0 } ) ( z ` ( n - 1 ) ) .< ( z ` n ) ) } )
50 4 49 nfcxfrd 
 |-  ( ph -> F/_ x { z e. Word A | A. n e. ( dom z \ { 0 } ) ( z ` ( n - 1 ) ) .< ( z ` n ) } )
51 3 50 nfcxfrd 
 |-  ( ph -> F/_ x ( .< Chain A ) )