Theorem elrnmpt2res 6424

Description: Membership in the range of a restricted operation class abstraction. (Contributed by Thierry Arnoux, 25-May-2019.)

Hypothesis

Ref	Expression
rngop.1	|- F = ( x e. A , y e. B |-> C )

Assertion

Ref	Expression
elrnmpt2res	|- ( D e. V -> ( D e. ran ( F |` R ) <-> E. x e. A E. y e. B ( D = C /\ x R y ) ) )

Distinct variable groups:   y, A   x, y, D   x, R, y

Allowed substitution hints:   A( x)   B( x, y)   C( x, y)   F( x, y)   V( x, y)

Proof of Theorem elrnmpt2res

Dummy variables z p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2433	. . . . . 6 |- ( z = D -> ( z = C <-> D = C ) )
2	1	anbi1d 709	. . . . 5 |- ( z = D -> ( ( z = C /\ x R y ) <-> ( D = C /\ x R y ) ) )
3	2	anbi2d 708	. . . 4 |- ( z = D -> ( ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) <-> ( ( x e. A /\ y e. B ) /\ ( D = C /\ x R y ) ) ) )
4	3	2exbidv 1763	. . 3 |- ( z = D -> ( E. x E. y ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ( D = C /\ x R y ) ) ) )
5		an12 804	. . . . . . . . . 10 |- ( ( p e. R /\ ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) <-> ( p = <. x , y >. /\ ( p e. R /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) )
6		an12 804	. . . . . . . . . . . 12 |- ( ( p e. R /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) <-> ( ( x e. A /\ y e. B ) /\ ( p e. R /\ z = C ) ) )
7		ancom 451	. . . . . . . . . . . . . 14 |- ( ( z = C /\ p e. R ) <-> ( p e. R /\ z = C ) )
8		eleq1 2501	. . . . . . . . . . . . . . . 16 |- ( p = <. x , y >. -> ( p e. R <-> <. x , y >. e. R ) )
9		df-br 4427	. . . . . . . . . . . . . . . 16 |- ( x R y <-> <. x , y >. e. R )
10	8, 9	syl6bbr 266	. . . . . . . . . . . . . . 15 |- ( p = <. x , y >. -> ( p e. R <-> x R y ) )
11	10	anbi2d 708	. . . . . . . . . . . . . 14 |- ( p = <. x , y >. -> ( ( z = C /\ p e. R ) <-> ( z = C /\ x R y ) ) )
12	7, 11	syl5bbr 262	. . . . . . . . . . . . 13 |- ( p = <. x , y >. -> ( ( p e. R /\ z = C ) <-> ( z = C /\ x R y ) ) )
13	12	anbi2d 708	. . . . . . . . . . . 12 |- ( p = <. x , y >. -> ( ( ( x e. A /\ y e. B ) /\ ( p e. R /\ z = C ) ) <-> ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) ) )
14	6, 13	syl5bb 260	. . . . . . . . . . 11 |- ( p = <. x , y >. -> ( ( p e. R /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) <-> ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) ) )
15	14	pm5.32i 641	. . . . . . . . . 10 |- ( ( p = <. x , y >. /\ ( p e. R /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) <-> ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) ) )
16	5, 15	bitri 252	. . . . . . . . 9 |- ( ( p e. R /\ ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) <-> ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) ) )
17	16	2exbii 1715	. . . . . . . 8 |- ( E. x E. y ( p e. R /\ ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) <-> E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) ) )
18		19.42vv 1828	. . . . . . . 8 |- ( E. x E. y ( p e. R /\ ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) <-> ( p e. R /\ E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) )
19	17, 18	bitr3i 254	. . . . . . 7 |- ( E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) ) <-> ( p e. R /\ E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) )
20	19	opabbii 4490	. . . . . 6 |- { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) ) } = { <. p , z >. | ( p e. R /\ E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) }
21		dfoprab2 6351	. . . . . 6 |- { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) } = { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) ) }
22		rngop.1	. . . . . . . . 9 |- F = ( x e. A , y e. B |-> C )
23		df-mpt2 6310	. . . . . . . . 9 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
24		dfoprab2 6351	. . . . . . . . 9 |- { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) }
25	22, 23, 24	3eqtri 2462	. . . . . . . 8 |- F = { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) }
26	25	reseq1i 5121	. . . . . . 7 |- ( F |` R ) = ( { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) } |` R )
27		resopab 5171	. . . . . . 7 |- ( { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) } |` R ) = { <. p , z >. | ( p e. R /\ E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) }
28	26, 27	eqtri 2458	. . . . . 6 |- ( F |` R ) = { <. p , z >. | ( p e. R /\ E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) }
29	20, 21, 28	3eqtr4ri 2469	. . . . 5 |- ( F |` R ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
30	29	rneqi 5081	. . . 4 |- ran ( F |` R ) = ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
31		rnoprab 6393	. . . 4 |- ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) } = { z | E. x E. y ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
32	30, 31	eqtri 2458	. . 3 |- ran ( F |` R ) = { z | E. x E. y ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
33	4, 32	elab2g 3226	. 2 |- ( D e. V -> ( D e. ran ( F |` R ) <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ( D = C /\ x R y ) ) ) )
34		r2ex 2958	. 2 |- ( E. x e. A E. y e. B ( D = C /\ x R y ) <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ( D = C /\ x R y ) ) )
35	33, 34	syl6bbr 266	1 |- ( D e. V -> ( D e. ran ( F |` R ) <-> E. x e. A E. y e. B ( D = C /\ x R y ) ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1870   {cab 2414   E.wrex 2783   <.cop 4008   class class class wbr 4426   {copab 4483   ran crn 4855   |` cres 4856   {coprab 6306   |-> cmpt2 6307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-xp 4860  df-rel 4861  df-cnv 4862  df-dm 4864  df-rn 4865  df-res 4866  df-oprab 6309  df-mpt2 6310

This theorem is referenced by: (None)