This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfttrcld

Description: Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024)

Ref Expression
Hypothesis nfttrcld.1 
|- ( ph -> F/_ x R )
Assertion nfttrcld 
|- ( ph -> F/_ x t++ R )

Proof

Step Hyp Ref Expression
1 nfttrcld.1 
 |-  ( ph -> F/_ x R )
2 df-ttrcl 
 |-  t++ R = { <. y , z >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = y /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) }
3 nfv 
 |-  F/ y ph
4 nfv 
 |-  F/ z ph
5 nfv 
 |-  F/ n ph
6 nfcvd 
 |-  ( ph -> F/_ x ( _om \ 1o ) )
7 nfv 
 |-  F/ f ph
8 nfvd 
 |-  ( ph -> F/ x f Fn suc n )
9 nfvd 
 |-  ( ph -> F/ x ( ( f ` (/) ) = y /\ ( f ` n ) = z ) )
10 nfv 
 |-  F/ a ph
11 nfcvd 
 |-  ( ph -> F/_ x n )
12 nfcvd 
 |-  ( ph -> F/_ x ( f ` a ) )
13 nfcvd 
 |-  ( ph -> F/_ x ( f ` suc a ) )
14 12 1 13 nfbrd 
 |-  ( ph -> F/ x ( f ` a ) R ( f ` suc a ) )
15 10 11 14 nfraldw 
 |-  ( ph -> F/ x A. a e. n ( f ` a ) R ( f ` suc a ) )
16 8 9 15 nf3and 
 |-  ( ph -> F/ x ( f Fn suc n /\ ( ( f ` (/) ) = y /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )
17 7 16 nfexd 
 |-  ( ph -> F/ x E. f ( f Fn suc n /\ ( ( f ` (/) ) = y /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )
18 5 6 17 nfrexdw 
 |-  ( ph -> F/ x E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = y /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) )
19 3 4 18 nfopabd 
 |-  ( ph -> F/_ x { <. y , z >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = y /\ ( f ` n ) = z ) /\ A. a e. n ( f ` a ) R ( f ` suc a ) ) } )
20 2 19 nfcxfrd 
 |-  ( ph -> F/_ x t++ R )