Description: Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfttrcld.1 | |
|
Assertion | nfttrcld | Could not format assertion : No typesetting found for |- ( ph -> F/_ x t++ R ) with typecode |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfttrcld.1 | |
|
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 | |
|
4 | nfv | |
|
5 | nfv | |
|
6 | nfcvd | |
|
7 | nfv | |
|
8 | nfvd | |
|
9 | nfvd | |
|
10 | nfv | |
|
11 | nfcvd | |
|
12 | nfcvd | |
|
13 | nfcvd | |
|
14 | 12 1 13 | nfbrd | |
15 | 10 11 14 | nfraldw | |
16 | 8 9 15 | nf3and | |
17 | 7 16 | nfexd | |
18 | 5 6 17 | nfrexd | |
19 | 3 4 18 | nfopabd | |
20 | 2 19 | nfcxfrd | Could not format ( ph -> F/_ x t++ R ) : No typesetting found for |- ( ph -> F/_ x t++ R ) with typecode |- |