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++ ( 𝑅 ↾ V ) = t++ 𝑅

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 𝑓 ‘ 𝑎 ) ∈ V
2		fvex	⊢ ( 𝑓 ‘ suc 𝑎 ) ∈ V
3	2	brresi	⊢ ( ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ V ) ( 𝑓 ‘ suc 𝑎 ) ↔ ( ( 𝑓 ‘ 𝑎 ) ∈ V ∧ ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
4	1 3	mpbiran	⊢ ( ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ V ) ( 𝑓 ‘ suc 𝑎 ) ↔ ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
5	4	ralbii	⊢ ( ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ V ) ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) )
6	5	3anbi3i	⊢ ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ V ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
7	6	exbii	⊢ ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ V ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
8	7	rexbii	⊢ ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ V ) ( 𝑓 ‘ suc 𝑎 ) ) ↔ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
9	8	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ V ) ( 𝑓 ‘ suc 𝑎 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
10		df-ttrcl	⊢ t++ ( 𝑅 ↾ V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) ( 𝑅 ↾ V ) ( 𝑓 ‘ suc 𝑎 ) ) }
11		df-ttrcl	⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑎 ∈ 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) }
12	9 10 11	3eqtr4i	⊢ t++ ( 𝑅 ↾ V ) = t++ 𝑅