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 φ_xR
Assertion nfttrcld Could not format assertion : No typesetting found for |- ( ph -> F/_ x t++ R ) with typecode |-

Proof

Step Hyp Ref Expression
1 nfttrcld.1 φ_xR
2 df-ttrcl Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
3 nfv yφ
4 nfv zφ
5 nfv nφ
6 nfcvd φ_xω1𝑜
7 nfv fφ
8 nfvd φxfFnsucn
9 nfvd φxf=yfn=z
10 nfv aφ
11 nfcvd φ_xn
12 nfcvd φ_xfa
13 nfcvd φ_xfsuca
14 12 1 13 nfbrd φxfaRfsuca
15 10 11 14 nfraldw φxanfaRfsuca
16 8 9 15 nf3and φxfFnsucnf=yfn=zanfaRfsuca
17 7 16 nfexd φxffFnsucnf=yfn=zanfaRfsuca
18 5 6 17 nfrexd φxnω1𝑜ffFnsucnf=yfn=zanfaRfsuca
19 3 4 18 nfopabd φ_xyz|nω1𝑜ffFnsucnf=yfn=zanfaRfsuca
20 2 19 nfcxfrd Could not format ( ph -> F/_ x t++ R ) : No typesetting found for |- ( ph -> F/_ x t++ R ) with typecode |-