bnj882

Description: Definition (using hypotheses for readability) of the function giving the transitive closure of X in A by R . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj882.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj882.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj882.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj882.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
Assertion	bnj882	$⊢ trCl (X, A, R) = ⋃_{f \in B} ⋃_{i \in dom f} f (i)$

Proof

Step	Hyp	Ref	Expression
1		bnj882.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj882.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj882.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj882.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		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)$
6		df-iun	$⊢ ⋃_{f \in B} ⋃_{i \in dom f} f (i) = \{w \| \exists f \in B w \in ⋃_{i \in dom f} f (i)\}$
7		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) = \{w \| \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)))\} w \in ⋃_{i \in dom f} f (i)\}$
8	1 2	anbi12i	$⊢ (φ \land ψ) \leftrightarrow (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)))$
9	8	anbi2i	$⊢ (f Fn n \land (φ \land ψ)) \leftrightarrow (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))))$
10		3anass	$⊢ (f Fn n \land φ \land ψ) \leftrightarrow (f Fn n \land (φ \land ψ))$
11		3anass	$⊢ (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 (X, A, R) \land \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))))$
12	9 10 11	3bitr4i	$⊢ (f Fn n \land φ \land ψ) \leftrightarrow (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)))$
13	3 12	rexeqbii	$⊢ \exists n \in D (f Fn n \land φ \land ψ) \leftrightarrow \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	13	abbii	$⊢ \{f \| \exists n \in D (f Fn n \land φ \land ψ)\} = \{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)))\}$
15	4 14	eqtri	$⊢ B = \{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)))\}$
16	15	eleq2i	$⊢ f \in B \leftrightarrow 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)))\}$
17	16	anbi1i	$⊢ (f \in B \land w \in ⋃_{i \in dom f} f (i)) \leftrightarrow (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 w \in ⋃_{i \in dom f} f (i))$
18	17	rexbii2	$⊢ \exists f \in B w \in ⋃_{i \in dom f} f (i) \leftrightarrow \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)))\} w \in ⋃_{i \in dom f} f (i)$
19	18	abbii	$⊢ \{w \| \exists f \in B w \in ⋃_{i \in dom f} f (i)\} = \{w \| \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)))\} w \in ⋃_{i \in dom f} f (i)\}$
20	7 19	eqtr4i	$⊢ ⋃_{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) = \{w \| \exists f \in B w \in ⋃_{i \in dom f} f (i)\}$
21	6 20	eqtr4i	$⊢ ⋃_{f \in B} ⋃_{i \in dom f} f (i) = ⋃_{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)$
22	5 21	eqtr4i	$⊢ trCl (X, A, R) = ⋃_{f \in B} ⋃_{i \in dom f} f (i)$

Metamath Proof Explorer

Theorem bnj882

Proof