df-bnj18

Description: Define the function giving: the transitive closure of X in A by R . This definition has been designed for facilitating verification that it is eliminable and that the $d restrictions are sound and complete. For a more readable definition see bnj882 . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	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)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cX	$class X$
1		cA	$class A$
2		cR	$class R$
3	1 2 0	c-bnj18	$class trCl (X, A, R)$
4		vf	$setvar f$
5		vn	$setvar n$
6		com	$class ω$
7		c0	$class \emptyset$
8	7	csn	$class \{\emptyset\}$
9	6 8	cdif	$class (ω ∖ \{\emptyset\})$
10	4	cv	$setvar f$
11	5	cv	$setvar n$
12	10 11	wfn	$wff f Fn n$
13	7 10	cfv	$class f (\emptyset)$
14	1 2 0	c-bnj14	$class pred (X, A, R)$
15	13 14	wceq	$wff f (\emptyset) = pred (X, A, R)$
16		vi	$setvar i$
17	16	cv	$setvar i$
18	17	csuc	$class suc i$
19	18 11	wcel	$wff suc i \in n$
20	18 10	cfv	$class f (suc i)$
21		vy	$setvar y$
22	17 10	cfv	$class f (i)$
23	21	cv	$setvar y$
24	1 2 23	c-bnj14	$class pred (y, A, R)$
25	21 22 24	ciun	$class ⋃_{y \in f (i)} pred (y, A, R)$
26	20 25	wceq	$wff f (suc i) = ⋃_{y \in f (i)} pred (y, A, R)$
27	19 26	wi	$wff (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
28	27 16 6	wral	$wff \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
29	12 15 28	w3a	$wff (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)))$
30	29 5 9	wrex	$wff \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)))$
31	30 4	cab	$class \{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)))\}$
32	10	cdm	$class dom f$
33	16 32 22	ciun	$class ⋃_{i \in dom f} f (i)$
34	4 31 33	ciun	$class ⋃_{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)$
35	3 34	wceq	$wff 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)$

Metamath Proof Explorer

Definition df-bnj18

Detailed syntax breakdown