Metamath Proof Explorer

Theorem elrnmpores

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

Ref Expression
Hypothesis rngop.1 
|- F = ( x e. A , y e. B |-> C )
Assertion elrnmpores 
|- ( D e. V -> ( D e. ran ( F |` R ) <-> E. x e. A E. y e. B ( D = C /\ x R y ) ) )

Proof

Step Hyp Ref Expression
1 rngop.1 
 |-  F = ( x e. A , y e. B |-> C )
2 eqeq1 
 |-  ( z = D -> ( z = C <-> D = C ) )
3 2 anbi1d 
 |-  ( z = D -> ( ( z = C /\ x R y ) <-> ( D = C /\ x R y ) ) )
4 3 anbi2d 
 |-  ( z = D -> ( ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) <-> ( ( x e. A /\ y e. B ) /\ ( D = C /\ x R y ) ) ) )
5 4 2exbidv 
 |-  ( 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 ) ) ) )
6 an12 
 |-  ( ( 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 ) ) ) )
7 an12 
 |-  ( ( p e. R /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) <-> ( ( x e. A /\ y e. B ) /\ ( p e. R /\ z = C ) ) )
8 ancom 
 |-  ( ( z = C /\ p e. R ) <-> ( p e. R /\ z = C ) )
9 eleq1 
 |-  ( p = <. x , y >. -> ( p e. R <-> <. x , y >. e. R ) )
10 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
11 9 10 bitr4di 
 |-  ( p = <. x , y >. -> ( p e. R <-> x R y ) )
12 11 anbi2d 
 |-  ( p = <. x , y >. -> ( ( z = C /\ p e. R ) <-> ( z = C /\ x R y ) ) )
13 8 12 bitr3id 
 |-  ( p = <. x , y >. -> ( ( p e. R /\ z = C ) <-> ( z = C /\ x R y ) ) )
14 13 anbi2d 
 |-  ( 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 ) ) ) )
15 7 14 bitrid 
 |-  ( 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 ) ) ) )
16 15 pm5.32i 
 |-  ( ( 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 ) ) ) )
17 6 16 bitri 
 |-  ( ( 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 ) ) ) )
18 17 2exbii 
 |-  ( 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 ) ) ) )
19 19.42vv 
 |-  ( 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 ) ) ) )
20 18 19 bitr3i 
 |-  ( 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 ) ) ) )
21 20 opabbii 
 |-  { <. 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 ) ) ) }
22 dfoprab2 
 |-  { <. <. 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 ) ) ) }
23 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
24 dfoprab2 
 |-  { <. <. 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 1 23 24 3eqtri 
 |-  F = { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) }
26 25 reseq1i 
 |-  ( F |` R ) = ( { <. p , z >. | E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) } |` R )
27 resopab 
 |-  ( { <. 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 
 |-  ( F |` R ) = { <. p , z >. | ( p e. R /\ E. x E. y ( p = <. x , y >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) ) }
29 21 22 28 3eqtr4ri 
 |-  ( F |` R ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
30 29 rneqi 
 |-  ran ( F |` R ) = ran { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
31 rnoprab 
 |-  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 
 |-  ran ( F |` R ) = { z | E. x E. y ( ( x e. A /\ y e. B ) /\ ( z = C /\ x R y ) ) }
33 5 32 elab2g 
 |-  ( 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 
 |-  ( 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 bitr4di 
 |-  ( D e. V -> ( D e. ran ( F |` R ) <-> E. x e. A E. y e. B ( D = C /\ x R y ) ) )