Theorem elrnmpt2res 6437

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 2466	. . . . . 6 |- ( z = D -> ( z = C <-> D = C ) )
2	1	anbi1d 716	. . . . 5 |- ( z = D -> ( ( z = C /\ x R y ) <-> ( D = C /\ x R y ) ) )
3	2	anbi2d 715	. . . 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 1781	. . 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 811	. . . . . . . . . 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 811	. . . . . . . . . . . 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 456	. . . . . . . . . . . . . 14 |- ( ( z = C /\ p e. R ) <-> ( p e. R /\ z = C ) )
8		eleq1 2528	. . . . . . . . . . . . . . . 16 |- ( p = <. x , y >. -> ( p e. R <-> <. x , y >. e. R ) )
9		df-br 4417	. . . . . . . . . . . . . . . 16 |- ( x R y <-> <. x , y >. e. R )
10	8, 9	syl6bbr 271	. . . . . . . . . . . . . . 15 |- ( p = <. x , y >. -> ( p e. R <-> x R y ) )
11	10	anbi2d 715	. . . . . . . . . . . . . 14 |- ( p = <. x , y >. -> ( ( z = C /\ p e. R ) <-> ( z = C /\ x R y ) ) )
12	7, 11	syl5bbr 267	. . . . . . . . . . . . 13 |- ( p = <. x , y >. -> ( ( p e. R /\ z = C ) <-> ( z = C /\ x R y ) ) )
13	12	anbi2d 715	. . . . . . . . . . . 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 265	. . . . . . . . . . 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 647	. . . . . . . . . 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 257	. . . . . . . . 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 1730	. . . . . . . 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 1847	. . . . . . . 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 259	. . . . . . 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 4481	. . . . . 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 6364	. . . . . 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 6320	. . . . . . . . 9 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
24		dfoprab2 6364	. . . . . . . . 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 2488	. . . . . . . 8 |- F = { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) }
26	25	reseq1i 5120	. . . . . . 7 |- ( F |` R ) = ( { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) } |` R )
27		resopab 5170	. . . . . . 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 2484	. . . . . 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 2495	. . . . 5 |- ( F |` R ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
30	29	rneqi 5080	. . . 4 |- ran ( F |` R ) = ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
31		rnoprab 6406	. . . 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 2484	. . 3 |- ran ( F |` R ) = { z | E. x E. y ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
33	4, 32	elab2g 3199	. 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 2925	. 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 271	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 189   /\ wa 375   = wceq 1455   E.wex 1674   e. wcel 1898   {cab 2448   E.wrex 2750   <.cop 3986   class class class wbr 4416   {copab 4474   ran crn 4854   |` cres 4855   {coprab 6316   |-> cmpt2 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-xp 4859  df-rel 4860  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-oprab 6319  df-mpt2 6320

This theorem is referenced by: (None)