bnj1318

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj1318	$⊢ 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		hbab1	$⊢ z \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)))\} \to \forall f z \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)))\}$
7		hbab1	$⊢ z \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)))\} \to \forall f z \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)))\}$
8	6 7	bnj1316	$⊢ \{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)))\} \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)$
9	5 8	syl	$⊢ 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)$
10		biid	$⊢ f (\emptyset) = pred (X, A, R) \leftrightarrow f (\emptyset) = pred (X, A, R)$
11		biid	$⊢ \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)) \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
12		eqid	$⊢ ω ∖ \{\emptyset\} = ω ∖ \{\emptyset\}$
13		eqid	$⊢ \{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 (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)))\}$
14	10 11 12 13	bnj882	$⊢ 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)$
15		biid	$⊢ f (\emptyset) = pred (Y, A, R) \leftrightarrow f (\emptyset) = pred (Y, A, R)$
16		eqid	$⊢ \{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)))\} = \{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)))\}$
17	15 11 12 16	bnj882	$⊢ 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)$
18	9 14 17	3eqtr4g	$⊢ X = Y \to trCl (X, A, R) = trCl (Y, A, R)$

Metamath Proof Explorer

Theorem bnj1318

Proof