Metamath Proof Explorer

Theorem ttrcleq

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

		Ref	Expression
	Assertion	ttrcleq	$⊢ R = S \to t++ R = t++ S$

Proof

Step	Hyp	Ref	Expression
1		breq	$⊢ R = S \to (f (m) R f (suc m) \leftrightarrow f (m) S f (suc m))$
2	1	ralbidv	$⊢ R = S \to (\forall m \in n f (m) R f (suc m) \leftrightarrow \forall m \in n f (m) S f (suc m))$
3	2	3anbi3d	$⊢ R = S \to ((f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m)) \leftrightarrow (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) S f (suc m)))$
4	3	exbidv	$⊢ R = S \to (\exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m)) \leftrightarrow \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) S f (suc m)))$
5	4	rexbidv	$⊢ R = S \to (\exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m)) \leftrightarrow \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) S f (suc m)))$
6	5	opabbidv	$⊢ R = S \to \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m))\} = \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) S f (suc m))\}$
7		df-ttrcl	$⊢ t++ R = \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) R f (suc m))\}$
8		df-ttrcl	$⊢ t++ S = \{⟨x, y⟩ \| \exists n \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc n \land (f (\emptyset) = x \land f (n) = y) \land \forall m \in n f (m) S f (suc m))\}$
9	6 7 8	3eqtr4g	$⊢ R = S \to t++ R = t++ S$