Theorem ttrcleq

Description: Equality theorem for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Assertion	ttrcleq	⊢ ( 𝑅 = 𝑆 → t++ 𝑅 = t++ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		breq	⊢ ( 𝑅 = 𝑆 → ( ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ↔ ( 𝑓 ‘ 𝑚 ) 𝑆 ( 𝑓 ‘ suc 𝑚 ) ) )
2	1	ralbidv	⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ↔ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑆 ( 𝑓 ‘ suc 𝑚 ) ) )
3	2	3anbi3d	⊢ ( 𝑅 = 𝑆 → ( ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) ↔ ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑆 ( 𝑓 ‘ suc 𝑚 ) ) ) )
4	3	exbidv	⊢ ( 𝑅 = 𝑆 → ( ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑆 ( 𝑓 ‘ suc 𝑚 ) ) ) )
5	4	rexbidv	⊢ ( 𝑅 = 𝑆 → ( ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) ↔ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑆 ( 𝑓 ‘ suc 𝑚 ) ) ) )
6	5	opabbidv	⊢ ( 𝑅 = 𝑆 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑆 ( 𝑓 ‘ suc 𝑚 ) ) } )
7		df-ttrcl	⊢ t++ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑅 ( 𝑓 ‘ suc 𝑚 ) ) }
8		df-ttrcl	⊢ t++ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ( ω ∖ 1o ) ∃ 𝑓 ( 𝑓 Fn suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑥 ∧ ( 𝑓 ‘ 𝑛 ) = 𝑦 ) ∧ ∀ 𝑚 ∈ 𝑛 ( 𝑓 ‘ 𝑚 ) 𝑆 ( 𝑓 ‘ suc 𝑚 ) ) }
9	6 7 8	3eqtr4g	⊢ ( 𝑅 = 𝑆 → t++ 𝑅 = t++ 𝑆 )