Theorem bnj1489 29937

Description: Technical lemma for bnj60 29943. 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
bnj1489.1	|- B = { d | ( d C_ A /\ A. x e. d pred ( x , A , R ) C_ d ) }
bnj1489.2	|- Y = <. x , ( f |` pred ( x , A , R ) ) >.
bnj1489.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1489.4	|- ( ta <-> ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) )
bnj1489.5	|- D = { x e. A | -. E. f ta }
bnj1489.6	|- ( ps <-> ( R FrSe A /\ D =/= (/) ) )
bnj1489.7	|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
bnj1489.8	|- ( ta' <-> [. y / x ]. ta )
bnj1489.9	|- H = { f | E. y e. pred ( x , A , R ) ta' }
bnj1489.10	|- P = U. H
bnj1489.11	|- Z = <. x , ( P |` pred ( x , A , R ) ) >.
bnj1489.12	|- Q = ( P u. { <. x , ( G ` Z ) >. } )

Assertion

Ref	Expression
bnj1489	|- ( ch -> Q e. _V )

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

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

Proof of Theorem bnj1489

Step	Hyp	Ref	Expression
1		bnj1489.12	. 2 |- Q = ( P u. { <. x , ( G ` Z ) >. } )
2		bnj1489.10	. . . 4 |- P = U. H
3		bnj1489.7	. . . . . . . 8 |- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
4		bnj1489.6	. . . . . . . . 9 |- ( ps <-> ( R FrSe A /\ D =/= (/) ) )
5		bnj1364 29909	. . . . . . . . . 10 |- ( R FrSe A -> R Se A )
6		df-bnj13 29568	. . . . . . . . . 10 |- ( R Se A <-> A. x e. A pred ( x , A , R ) e. _V )
7	5, 6	sylib 201	. . . . . . . . 9 |- ( R FrSe A -> A. x e. A pred ( x , A , R ) e. _V )
8	4, 7	bnj832 29640	. . . . . . . 8 |- ( ps -> A. x e. A pred ( x , A , R ) e. _V )
9	3, 8	bnj835 29642	. . . . . . 7 |- ( ch -> A. x e. A pred ( x , A , R ) e. _V )
10		bnj1489.5	. . . . . . . 8 |- D = { x e. A | -. E. f ta }
11	10, 3	bnj1212 29683	. . . . . . 7 |- ( ch -> x e. A )
12	9, 11	bnj1294 29701	. . . . . 6 |- ( ch -> pred ( x , A , R ) e. _V )
13		nfv 1769	. . . . . . . . 9 |- F/ y ps
14		nfv 1769	. . . . . . . . 9 |- F/ y x e. D
15		nfra1 2785	. . . . . . . . 9 |- F/ y A. y e. D -. y R x
16	13, 14, 15	nf3an 2033	. . . . . . . 8 |- F/ y ( ps /\ x e. D /\ A. y e. D -. y R x )
17	3, 16	nfxfr 1704	. . . . . . 7 |- F/ y ch
18	4	simplbi 467	. . . . . . . . . . 11 |- ( ps -> R FrSe A )
19	3, 18	bnj835 29642	. . . . . . . . . 10 |- ( ch -> R FrSe A )
20	19	adantr 472	. . . . . . . . 9 |- ( ( ch /\ y e. pred ( x , A , R ) ) -> R FrSe A )
21		bnj1489.1	. . . . . . . . . . 11 |- B = { d | ( d C_ A /\ A. x e. d pred ( x , A , R ) C_ d ) }
22		bnj1489.2	. . . . . . . . . . 11 |- Y = <. x , ( f |` pred ( x , A , R ) ) >.
23		bnj1489.3	. . . . . . . . . . 11 |- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
24		bnj1489.4	. . . . . . . . . . 11 |- ( ta <-> ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) )
25		bnj1489.8	. . . . . . . . . . 11 |- ( ta' <-> [. y / x ]. ta )
26	21, 22, 23, 24, 10, 4, 3, 25	bnj1388 29914	. . . . . . . . . 10 |- ( ch -> A. y e. pred ( x , A , R ) E. f ta' )
27	26	r19.21bi 2776	. . . . . . . . 9 |- ( ( ch /\ y e. pred ( x , A , R ) ) -> E. f ta' )
28		nfv 1769	. . . . . . . . . . . 12 |- F/ x R FrSe A
29		nfsbc1v 3275	. . . . . . . . . . . . . 14 |- F/ x [. y / x ]. ta
30	25, 29	nfxfr 1704	. . . . . . . . . . . . 13 |- F/ x ta'
31	30	nfex 2050	. . . . . . . . . . . 12 |- F/ x E. f ta'
32	28, 31	nfan 2031	. . . . . . . . . . 11 |- F/ x ( R FrSe A /\ E. f ta' )
33	30	nfeu 2335	. . . . . . . . . . 11 |- F/ x E! f ta'
34	32, 33	nfim 2023	. . . . . . . . . 10 |- F/ x ( ( R FrSe A /\ E. f ta' ) -> E! f ta' )
35		sneq 3969	. . . . . . . . . . . . . . . . 17 |- ( x = y -> { x } = { y } )
36		bnj1318 29906	. . . . . . . . . . . . . . . . 17 |- ( x = y -> trCl ( x , A , R ) = trCl ( y , A , R ) )
37	35, 36	uneq12d 3580	. . . . . . . . . . . . . . . 16 |- ( x = y -> ( { x } u. trCl ( x , A , R ) ) = ( { y } u. trCl ( y , A , R ) ) )
38	37	eqeq2d 2481	. . . . . . . . . . . . . . 15 |- ( x = y -> ( dom f = ( { x } u. trCl ( x , A , R ) ) <-> dom f = ( { y } u. trCl ( y , A , R ) ) ) )
39	38	anbi2d 718	. . . . . . . . . . . . . 14 |- ( x = y -> ( ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) <-> ( f e. C /\ dom f = ( { y } u. trCl ( y , A , R ) ) ) ) )
40	21, 22, 23, 24, 25	bnj1373 29911	. . . . . . . . . . . . . 14 |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. trCl ( y , A , R ) ) ) )
41	39, 40	syl6bbr 271	. . . . . . . . . . . . 13 |- ( x = y -> ( ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) <-> ta' ) )
42	41	exbidv 1776	. . . . . . . . . . . 12 |- ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) <-> E. f ta' ) )
43	42	anbi2d 718	. . . . . . . . . . 11 |- ( x = y -> ( ( R FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) ) <-> ( R FrSe A /\ E. f ta' ) ) )
44	41	eubidv 2339	. . . . . . . . . . 11 |- ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) <-> E! f ta' ) )
45	43, 44	imbi12d 327	. . . . . . . . . 10 |- ( x = y -> ( ( ( R FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) ) <-> ( ( R FrSe A /\ E. f ta' ) -> E! f ta' ) ) )
46		biid 244	. . . . . . . . . . 11 |- ( ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) <-> ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) )
47	21, 22, 23, 46	bnj1321 29908	. . . . . . . . . 10 |- ( ( R FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. trCl ( x , A , R ) ) ) )
48	34, 45, 47	chvar 2119	. . . . . . . . 9 |- ( ( R FrSe A /\ E. f ta' ) -> E! f ta' )
49	20, 27, 48	syl2anc 673	. . . . . . . 8 |- ( ( ch /\ y e. pred ( x , A , R ) ) -> E! f ta' )
50	49	ex 441	. . . . . . 7 |- ( ch -> ( y e. pred ( x , A , R ) -> E! f ta' ) )
51	17, 50	ralrimi 2800	. . . . . 6 |- ( ch -> A. y e. pred ( x , A , R ) E! f ta' )
52		bnj1489.9	. . . . . . 7 |- H = { f | E. y e. pred ( x , A , R ) ta' }
53	52	a1i 11	. . . . . 6 |- ( ch -> H = { f | E. y e. pred ( x , A , R ) ta' } )
54		biid 244	. . . . . . 7 |- ( ( pred ( x , A , R ) e. _V /\ A. y e. pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. pred ( x , A , R ) ta' } ) <-> ( pred ( x , A , R ) e. _V /\ A. y e. pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. pred ( x , A , R ) ta' } ) )
55	54	bnj1366 29713	. . . . . 6 |- ( ( pred ( x , A , R ) e. _V /\ A. y e. pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. pred ( x , A , R ) ta' } ) -> H e. _V )
56	12, 51, 53, 55	syl3anc 1292	. . . . 5 |- ( ch -> H e. _V )
57		uniexg 6607	. . . . 5 |- ( H e. _V -> U. H e. _V )
58	56, 57	syl 17	. . . 4 |- ( ch -> U. H e. _V )
59	2, 58	syl5eqel 2553	. . 3 |- ( ch -> P e. _V )
60		snex 4641	. . . 4 |- { <. x , ( G ` Z ) >. } e. _V
61	60	a1i 11	. . 3 |- ( ch -> { <. x , ( G ` Z ) >. } e. _V )
62	59, 61	bnj1149 29676	. 2 |- ( ch -> ( P u. { <. x , ( G ` Z ) >. } ) e. _V )
63	1, 62	syl5eqel 2553	1 |- ( ch -> Q e. _V )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   /\ w3a 1007   = wceq 1452   E.wex 1671   e. wcel 1904   E!weu 2319   {cab 2457   =/= wne 2641   A.wral 2756   E.wrex 2757   {crab 2760   _Vcvv 3031   [.wsbc 3255   u. cun 3388   C_ wss 3390   (/)c0 3722   {csn 3959   <.cop 3965   U.cuni 4190   class class class wbr 4395   dom cdm 4839   |` cres 4841   Fn wfn 5584   ` cfv 5589   predc-bnj14 29565   Se w-bnj13 29567   FrSe w-bnj15 29569   trClc-bnj18 29571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-reg 8125  ax-inf2 8164

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-om 6712  df-1o 7200  df-bnj17 29564  df-bnj14 29566  df-bnj13 29568  df-bnj15 29570  df-bnj18 29572  df-bnj19 29574

This theorem is referenced by:  bnj1312  29939