Theorem bnj893 29748

Description: Property of trCl. Under certain conditions, the transitive closure of X in A by R is a set. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Assertion

Ref	Expression
bnj893	|- ( ( R FrSe A /\ X e. A ) -> trCl ( X , A , R ) e. _V )

Proof of Theorem bnj893

Dummy variables f g i n y w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		biid 239	. . 3 |- ( ( f ` (/) ) = pred ( X , A , R ) <-> ( f ` (/) ) = pred ( X , A , R ) )
2		biid 239	. . 3 |- ( A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) <-> A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
3		eqid 2422	. . 3 |- ( om \ { (/) } ) = ( om \ { (/) } )
4		eqid 2422	. . 3 |- { 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 ) ) ) } = { 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 ) ) ) }
5	1, 2, 3, 4	bnj882 29746	. 2 |- 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 )
6		vex 3083	. . . . . . . . . . 11 |- g e. _V
7		fveq1 5881	. . . . . . . . . . . 12 |- ( f = g -> ( f ` (/) ) = ( g ` (/) ) )
8	7	eqeq1d 2424	. . . . . . . . . . 11 |- ( f = g -> ( ( f ` (/) ) = pred ( X , A , R ) <-> ( g ` (/) ) = pred ( X , A , R ) ) )
9	6, 8	sbcie 3334	. . . . . . . . . 10 |- ( [. g / f ]. ( f ` (/) ) = pred ( X , A , R ) <-> ( g ` (/) ) = pred ( X , A , R ) )
10	9	bicomi 205	. . . . . . . . 9 |- ( ( g ` (/) ) = pred ( X , A , R ) <-> [. g / f ]. ( f ` (/) ) = pred ( X , A , R ) )
11		fveq1 5881	. . . . . . . . . . . . . 14 |- ( f = g -> ( f ` suc i ) = ( g ` suc i ) )
12		fveq1 5881	. . . . . . . . . . . . . . 15 |- ( f = g -> ( f ` i ) = ( g ` i ) )
13	12	iuneq1d 4324	. . . . . . . . . . . . . 14 |- ( f = g -> U_ y e. ( f ` i ) pred ( y , A , R ) = U_ y e. ( g ` i ) pred ( y , A , R ) )
14	11, 13	eqeq12d 2444	. . . . . . . . . . . . 13 |- ( f = g -> ( ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) <-> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) )
15	14	imbi2d 317	. . . . . . . . . . . 12 |- ( f = g -> ( ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) <-> ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) )
16	15	ralbidv 2861	. . . . . . . . . . 11 |- ( f = g -> ( A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) <-> A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) )
17	6, 16	sbcie 3334	. . . . . . . . . 10 |- ( [. g / f ]. A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) <-> A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) )
18	17	bicomi 205	. . . . . . . . 9 |- ( A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) <-> [. g / f ]. A. i e. om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) pred ( y , A , R ) ) )
19	4, 10, 18	bnj873 29744	. . . . . . . 8 |- { 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 ) ) ) } = { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) }
20	19	eleq2i 2499	. . . . . . 7 |- ( 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 ) ) ) } <-> f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } )
21	20	anbi1i 699	. . . . . 6 |- ( ( 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 ) ) ) } /\ w e. U_ i e. dom f ( f ` i ) ) <-> ( f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } /\ w e. U_ i e. dom f ( f ` i ) ) )
22	21	rexbii2 2922	. . . . 5 |- ( E. 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 ) ) ) } w e. U_ i e. dom f ( f ` i ) <-> E. f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } w e. U_ i e. dom f ( f ` i ) )
23	22	abbii 2551	. . . 4 |- { w | E. 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 ) ) ) } w e. U_ i e. dom f ( f ` i ) } = { w | E. f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } w e. U_ i e. dom f ( f ` i ) }
24		df-iun 4301	. . . 4 |- 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 ) = { w | E. 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 ) ) ) } w e. U_ i e. dom f ( f ` i ) }
25		df-iun 4301	. . . 4 |- U_ f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) = { w | E. f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } w e. U_ i e. dom f ( f ` i ) }
26	23, 24, 25	3eqtr4i 2461	. . 3 |- 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 ) = U_ f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i )
27		biid 239	. . . . 5 |- ( ( g ` (/) ) = pred ( X , A , R ) <-> ( g ` (/) ) = pred ( X , A , R ) )
28		biid 239	. . . . 5 |- ( A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) <-> A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) )
29		eqid 2422	. . . . 5 |- { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } = { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) }
30		biid 239	. . . . 5 |- ( ( R FrSe A /\ X e. A /\ n e. ( om \ { (/) } ) ) <-> ( R FrSe A /\ X e. A /\ n e. ( om \ { (/) } ) ) )
31		biid 239	. . . . 5 |- ( ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) <-> ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) )
32		biid 239	. . . . 5 |- ( [. z / g ]. ( g ` (/) ) = pred ( X , A , R ) <-> [. z / g ]. ( g ` (/) ) = pred ( X , A , R ) )
33		biid 239	. . . . 5 |- ( [. z / g ]. A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) <-> [. z / g ]. A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) )
34		biid 239	. . . . 5 |- ( [. z / g ]. ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) <-> [. z / g ]. ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) )
35		biid 239	. . . . 5 |- ( ( R FrSe A /\ X e. A ) <-> ( R FrSe A /\ X e. A ) )
36	27, 28, 3, 29, 30, 31, 32, 33, 34, 35	bnj849 29745	. . . 4 |- ( ( R FrSe A /\ X e. A ) -> { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } e. _V )
37		vex 3083	. . . . . . 7 |- f e. _V
38	37	dmex 6741	. . . . . 6 |- dom f e. _V
39		fvex 5892	. . . . . 6 |- ( f ` i ) e. _V
40	38, 39	iunex 6788	. . . . 5 |- U_ i e. dom f ( f ` i ) e. _V
41	40	rgenw 2783	. . . 4 |- A. f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) e. _V
42		iunexg 6784	. . . 4 |- ( ( { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } e. _V /\ A. f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) e. _V ) -> U_ f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) e. _V )
43	36, 41, 42	sylancl 666	. . 3 |- ( ( R FrSe A /\ X e. A ) -> U_ f e. { g | E. n e. ( om \ { (/) } ) ( g Fn n /\ ( g ` (/) ) = pred ( X , A , R ) /\ A. i e. om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) pred ( y , A , R ) ) ) } U_ i e. dom f ( f ` i ) e. _V )
44	26, 43	syl5eqel 2511	. 2 |- ( ( R FrSe A /\ X e. A ) -> 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 ) e. _V )
45	5, 44	syl5eqel 2511	1 |- ( ( R FrSe A /\ X e. A ) -> trCl ( X , A , R ) e. _V )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1872   {cab 2407   A.wral 2771   E.wrex 2772   _Vcvv 3080   [.wsbc 3299   \ cdif 3433   (/)c0 3761   {csn 3998   U_ciun 4299   dom cdm 4853   suc csuc 5444   Fn wfn 5596   ` cfv 5601   omcom 6707   predc-bnj14 29502   FrSe w-bnj15 29506   trClc-bnj18 29508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-reg 8117  ax-inf2 8156

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-om 6708  df-1o 7194  df-bnj17 29501  df-bnj14 29503  df-bnj13 29505  df-bnj15 29507  df-bnj18 29509

This theorem is referenced by:  bnj1125  29810  bnj1136  29815  bnj1177  29824  bnj1413  29853  bnj1452  29870