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 ⊢ φ → Ⅎ _ x R
Assertion nfttrcld ⊢ φ → Ⅎ _ x t++ R

Proof

Step Hyp Ref Expression
1 nfttrcld.1 ⊢ φ → Ⅎ _ x R
2 df-ttrcl ⊢ t++ R = y z | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = y ∧ f ⁡ n = z ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
3 nfv ⊢ Ⅎ y φ
4 nfv ⊢ Ⅎ z φ
5 nfv ⊢ Ⅎ n φ
6 nfcvd ⊢ φ → Ⅎ _ x ω ∖ 1 𝑜
7 nfv ⊢ Ⅎ f φ
8 nfvd ⊢ φ → Ⅎ x f Fn suc ⁡ n
9 nfvd ⊢ φ → Ⅎ x f ⁡ ∅ = y ∧ f ⁡ n = z
10 nfv ⊢ Ⅎ a φ
11 nfcvd ⊢ φ → Ⅎ _ x n
12 nfcvd ⊢ φ → Ⅎ _ x f ⁡ a
13 nfcvd ⊢ φ → Ⅎ _ x f ⁡ suc ⁡ a
14 12 1 13 nfbrd ⊢ φ → Ⅎ x f ⁡ a R f ⁡ suc ⁡ a
15 10 11 14 nfraldw ⊢ φ → Ⅎ x ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
16 8 9 15 nf3and ⊢ φ → Ⅎ x f Fn suc ⁡ n ∧ f ⁡ ∅ = y ∧ f ⁡ n = z ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
17 7 16 nfexd ⊢ φ → Ⅎ x ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = y ∧ f ⁡ n = z ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
18 5 6 17 nfrexdw ⊢ φ → Ⅎ x ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = y ∧ f ⁡ n = z ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
19 3 4 18 nfopabd ⊢ φ → Ⅎ _ x y z | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = y ∧ f ⁡ n = z ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
20 2 19 nfcxfrd ⊢ φ → Ⅎ _ x t++ R