Definition df-bnj18 33615

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 33852. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Assertion

Ref	Expression
df-bnj18	|- trCl ( X , A , R ) = U_ f e. { f | E. n e. ( om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i )

Distinct variable groups:   f, X, n, i, y   A, f, n, i, y   R, f, n, i, y

Detailed syntax breakdown of Definition df-bnj18

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3		cX	. . 3 class X
4	1, 2, 3	c-bnj18 33614	. 2 class trCl ( X , A , R )
5		vf	. . 3 setvar f
6	5	cv 1382	. . . . . . 7 class f
7		vn	. . . . . . . 8 setvar n
8	7	cv 1382	. . . . . . 7 class n
9	6, 8	wfn 5573	. . . . . 6 wff f Fn n
10		c0 3770	. . . . . . . 8 class (/)
11	10, 6	cfv 5578	. . . . . . 7 class ( f ` (/) )
12	1, 2, 3	c-bnj14 33608	. . . . . . 7 class pred ( X , A , R )
13	11, 12	wceq 1383	. . . . . 6 wff ( f ` (/) ) = pred ( X , A , R )
14		vi	. . . . . . . . . . 11 setvar i
15	14	cv 1382	. . . . . . . . . 10 class i
16	15	csuc 4870	. . . . . . . . 9 class suc i
17	16, 8	wcel 1804	. . . . . . . 8 wff suc i e. n
18	16, 6	cfv 5578	. . . . . . . . 9 class ( f ` suc i )
19		vy	. . . . . . . . . 10 setvar y
20	15, 6	cfv 5578	. . . . . . . . . 10 class ( f ` i )
21	19	cv 1382	. . . . . . . . . . 11 class y
22	1, 2, 21	c-bnj14 33608	. . . . . . . . . 10 class pred ( y , A , R )
23	19, 20, 22	ciun 4315	. . . . . . . . 9 class U_ y e. ( f ` i ) pred ( y , A , R )
24	18, 23	wceq 1383	. . . . . . . 8 wff ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R )
25	17, 24	wi 4	. . . . . . 7 wff ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) )
26		com 6685	. . . . . . 7 class om
27	25, 14, 26	wral 2793	. . . . . 6 wff A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) )
28	9, 13, 27	w3a 974	. . . . 5 wff ( f Fn n /\ ( f ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
29	10	csn 4014	. . . . . 6 class { (/) }
30	26, 29	cdif 3458	. . . . 5 class ( om \ { (/) } )
31	28, 7, 30	wrex 2794	. . . 4 wff E. n e. ( om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
32	31, 5	cab 2428	. . 3 class { f | E. n e. ( om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) ) }
33	6	cdm 4989	. . . 4 class dom f
34	14, 33, 20	ciun 4315	. . 3 class U_ i e. dom f ( f ` i )
35	5, 32, 34	ciun 4315	. 2 class U_ f e. { f | E. n e. ( om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i )
36	4, 35	wceq 1383	1 wff trCl ( X , A , R ) = U_ f e. { f | E. n e. ( om \ { (/) } ) ( f Fn n /\ ( f ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i )

This definition is referenced by:  bnj882  33852  bnj18eq1  33853