Metamath Proof Explorer

Theorem bnj18eq1

Description: Equality theorem for transitive closure. (Contributed by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj18eq1	$⊢ X = Y \to trCl (X, A, R) = trCl (Y, A, R)$

Proof

Step	Hyp	Ref	Expression
1		bnj602	$⊢ X = Y \to pred (X, A, R) = pred (Y, A, R)$
2	1	eqeq2d	$⊢ X = Y \to (f (\emptyset) = pred (X, A, R) \leftrightarrow f (\emptyset) = pred (Y, A, R))$
3	2	3anbi2d	$⊢ X = Y \to ((f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))) \leftrightarrow (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))))$
4	3	rexbidv	$⊢ X = Y \to (\exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))) \leftrightarrow \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))))$
5	4	abbidv	$⊢ X = Y \to \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} = \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}$
6	5	eleq2d	$⊢ X = Y \to (f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} \leftrightarrow f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\})$
7	6	anbi1d	$⊢ X = Y \to ((f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} \land x \in ⋃_{i \in dom f} f (i)) \leftrightarrow (f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} \land x \in ⋃_{i \in dom f} f (i)))$
8	7	rexbidv2	$⊢ X = Y \to (\exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} x \in ⋃_{i \in dom f} f (i) \leftrightarrow \exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} x \in ⋃_{i \in dom f} f (i))$
9	8	abbidv	$⊢ X = Y \to \{x \| \exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} x \in ⋃_{i \in dom f} f (i)\} = \{x \| \exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} x \in ⋃_{i \in dom f} f (i)\}$
10		df-iun	$⊢ ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) = \{x \| \exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} x \in ⋃_{i \in dom f} f (i)\}$
11		df-iun	$⊢ ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) = \{x \| \exists f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\} x \in ⋃_{i \in dom f} f (i)\}$
12	9 10 11	3eqtr4g	$⊢ X = Y \to ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i) = ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i)$
13		df-bnj18	$⊢ trCl (X, A, R) = ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i)$
14		df-bnj18	$⊢ trCl (Y, A, R) = ⋃_{f \in \{f \| \exists n \in (ω ∖ \{\emptyset\}) (f Fn n \land f (\emptyset) = pred (Y, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}} ⋃_{i \in dom f} f (i)$
15	12 13 14	3eqtr4g	$⊢ X = Y \to trCl (X, A, R) = trCl (Y, A, R)$