Theorem bnj1415 29895

Description: Technical lemma for bnj60 29919. 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.)

Hypotheses

Ref	Expression
bnj1415.1	|- B = { d | ( d C_ A /\ A. x e. d pred ( x , A , R ) C_ d ) }
bnj1415.2	|- Y = <. x , ( f |` pred ( x , A , R ) ) >.
bnj1415.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1415.4	|- ( ta <-> ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) )
bnj1415.5	|- D = { x e. A | -. E. f ta }
bnj1415.6	|- ( ps <-> ( R FrSe A /\ D =/= (/) ) )
bnj1415.7	|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
bnj1415.8	|- ( ta' <-> [. y / x ]. ta )
bnj1415.9	|- H = { f | E. y e. pred ( x , A , R ) ta' }
bnj1415.10	|- P = U. H

Assertion

Ref	Expression
bnj1415	|- ( ch -> dom P = trCl ( x , A , R ) )

Distinct variable groups:   A, f, x, y   B, f   y, C   y, D   R, f, x, y   f, d, x   ps, y   ta, y

Allowed substitution hints:   ps( x, f, d)   ch( x, y, f, d)   ta( x, f, d)   A( d)   B( x, y, d)   C( x, f, d)   D( x, f, d)   P( x, y, f, d)   R( d)   G( x, y, f, d)   H( x, y, f, d)   Y( x, y, f, d)   ta'( x, y, f, d)

Proof of Theorem bnj1415

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bnj1415.7	. . . 4 |- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
2		bnj1415.6	. . . . 5 |- ( ps <-> ( R FrSe A /\ D =/= (/) ) )
3	2	simplbi 466	. . . 4 |- ( ps -> R FrSe A )
4	1, 3	bnj835 29618	. . 3 |- ( ch -> R FrSe A )
5		bnj1415.5	. . . 4 |- D = { x e. A | -. E. f ta }
6	5, 1	bnj1212 29659	. . 3 |- ( ch -> x e. A )
7		eqid 2461	. . . 4 |- ( pred ( x , A , R ) u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) ) = ( pred ( x , A , R ) u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) )
8	7	bnj1414 29894	. . 3 |- ( ( R FrSe A /\ x e. A ) -> trCl ( x , A , R ) = ( pred ( x , A , R ) u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) ) )
9	4, 6, 8	syl2anc 671	. 2 |- ( ch -> trCl ( x , A , R ) = ( pred ( x , A , R ) u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) ) )
10		iunun 4375	. . . 4 |- U_ y e. pred ( x , A , R ) ( { y } u. trCl ( y , A , R ) ) = ( U_ y e. pred ( x , A , R ) { y } u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) )
11		iunid 4346	. . . . 5 |- U_ y e. pred ( x , A , R ) { y } = pred ( x , A , R )
12	11	uneq1i 3595	. . . 4 |- ( U_ y e. pred ( x , A , R ) { y } u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) ) = ( pred ( x , A , R ) u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) )
13	10, 12	eqtri 2483	. . 3 |- U_ y e. pred ( x , A , R ) ( { y } u. trCl ( y , A , R ) ) = ( pred ( x , A , R ) u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) )
14		bnj1415.1	. . . 4 |- B = { d | ( d C_ A /\ A. x e. d pred ( x , A , R ) C_ d ) }
15		bnj1415.2	. . . 4 |- Y = <. x , ( f |` pred ( x , A , R ) ) >.
16		bnj1415.3	. . . 4 |- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
17		bnj1415.4	. . . 4 |- ( ta <-> ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) )
18		bnj1415.8	. . . 4 |- ( ta' <-> [. y / x ]. ta )
19		bnj1415.9	. . . 4 |- H = { f | E. y e. pred ( x , A , R ) ta' }
20		bnj1415.10	. . . 4 |- P = U. H
21		biid 244	. . . 4 |- ( ( ch /\ z e. U_ y e. pred ( x , A , R ) ( { y } u. trCl ( y , A , R ) ) ) <-> ( ch /\ z e. U_ y e. pred ( x , A , R ) ( { y } u. trCl ( y , A , R ) ) ) )
22		biid 244	. . . 4 |- ( ( ( ch /\ z e. U_ y e. pred ( x , A , R ) ( { y } u. trCl ( y , A , R ) ) ) /\ y e. pred ( x , A , R ) /\ z e. ( { y } u. trCl ( y , A , R ) ) ) <-> ( ( ch /\ z e. U_ y e. pred ( x , A , R ) ( { y } u. trCl ( y , A , R ) ) ) /\ y e. pred ( x , A , R ) /\ z e. ( { y } u. trCl ( y , A , R ) ) ) )
23	14, 15, 16, 17, 5, 2, 1, 18, 19, 20, 21, 22	bnj1398 29891	. . 3 |- ( ch -> U_ y e. pred ( x , A , R ) ( { y } u. trCl ( y , A , R ) ) = dom P )
24	13, 23	syl5eqr 2509	. 2 |- ( ch -> ( pred ( x , A , R ) u. U_ y e. pred ( x , A , R ) trCl ( y , A , R ) ) = dom P )
25	9, 24	eqtr2d 2496	1 |- ( ch -> dom P = trCl ( x , A , R ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1454   E.wex 1673   e. wcel 1897   {cab 2447   =/= wne 2632   A.wral 2748   E.wrex 2749   {crab 2752   [.wsbc 3278   u. cun 3413   C_ wss 3415   (/)c0 3742   {csn 3979   <.cop 3985   U.cuni 4211   U_ciun 4291   class class class wbr 4415   dom cdm 4852   |` cres 4854   Fn wfn 5595   ` cfv 5600   predc-bnj14 29541   FrSe w-bnj15 29545   trClc-bnj18 29547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-reg 8132  ax-inf2 8171

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-fal 1460  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-om 6719  df-1o 7207  df-bnj17 29540  df-bnj14 29542  df-bnj13 29544  df-bnj15 29546  df-bnj18 29548  df-bnj19 29550

This theorem is referenced by:  bnj1312  29915