Metamath Proof Explorer

Theorem ttrclresv

Description: The transitive closure of R restricted to _V is the same as the transitive closure of R itself. (Contributed by Scott Fenton, 20-Oct-2024)

Ref Expression
Assertion ttrclresv ⊢ t++ R ↾ V = t++ R

Proof

Step Hyp Ref Expression
1 fvex ⊢ f ⁡ a ∈ V
2 fvex ⊢ f ⁡ suc ⁡ a ∈ V
3 2 brresi ⊢ f ⁡ a R ↾ V f ⁡ suc ⁡ a ↔ f ⁡ a ∈ V ∧ f ⁡ a R f ⁡ suc ⁡ a
4 1 3 mpbiran ⊢ f ⁡ a R ↾ V f ⁡ suc ⁡ a ↔ f ⁡ a R f ⁡ suc ⁡ a
5 4 ralbii ⊢ ∀ a ∈ n f ⁡ a R ↾ V f ⁡ suc ⁡ a ↔ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
6 5 3anbi3i ⊢ f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R ↾ V f ⁡ suc ⁡ a ↔ f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
7 6 exbii ⊢ ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R ↾ V f ⁡ suc ⁡ a ↔ ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
8 7 rexbii ⊢ ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R ↾ V f ⁡ suc ⁡ a ↔ ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
9 8 opabbii ⊢ x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R ↾ V f ⁡ suc ⁡ a = x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
10 df-ttrcl ⊢ t++ R ↾ V = x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R ↾ V f ⁡ suc ⁡ a
11 df-ttrcl ⊢ t++ R = x y | ∃ n ∈ ω ∖ 1 𝑜 ∃ f f Fn suc ⁡ n ∧ f ⁡ ∅ = x ∧ f ⁡ n = y ∧ ∀ a ∈ n f ⁡ a R f ⁡ suc ⁡ a
12 9 10 11 3eqtr4i ⊢ t++ R ↾ V = t++ R