Theorem nfttrcld

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

	Ref	Expression
Hypothesis	nfttrcld.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝑅 )
Assertion	nfttrcld	⊢ ( 𝜑 → Ⅎ 𝑥 t++ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		nfttrcld.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝑅 )
2		df-ttrcl	⊢ t++ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑧 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
3		nfv	⊢ Ⅎ 𝑦 𝜑
4		nfv	⊢ Ⅎ 𝑧 𝜑
5		nfv	⊢ Ⅎ 𝑛 𝜑
6		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( ω ∖ 1o ) )
7		nfv	⊢ Ⅎ 𝑓 𝜑
8		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑓 Fn suc 𝑛 )
9		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑧 ) )
10		nfv	⊢ Ⅎ 𝑎 𝜑
11		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑛 )
12		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑓 ‘ 𝑎 ) )
13		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑓 ‘ suc 𝑎 ) )
14	12 1 13	nfbrd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
15	10 11 14	nfraldw	⊢ ( 𝜑 → Ⅎ 𝑥 ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
16	8 9 15	nf3and	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑧 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
17	7 16	nfexd	⊢ ( 𝜑 → Ⅎ 𝑥 ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑧 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
18	5 6 17	nfrexdw	⊢ ( 𝜑 → Ⅎ 𝑥 ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑧 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
19	3 4 18	nfopabd	⊢ ( 𝜑 → Ⅎ 𝑥 { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑦 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑧 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) } )
20	2 19	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 t++ 𝑅 )