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 ⊢ ( 𝜑 → Ⅎ 𝑥 𝑅 )
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++ 𝑅 )