Metamath Proof Explorer


Theorem rnxrn

Description: Range of the range Cartesian product of classes. (Contributed by Peter Mazsa, 1-Jun-2020)

Ref Expression
Assertion rnxrn
|- ran ( R |X. S ) = { <. x , y >. | E. u ( u R x /\ u S y ) }

Proof

Step Hyp Ref Expression
1 3anass
 |-  ( ( w = <. x , y >. /\ u R x /\ u S y ) <-> ( w = <. x , y >. /\ ( u R x /\ u S y ) ) )
2 1 3exbii
 |-  ( E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) <-> E. u E. x E. y ( w = <. x , y >. /\ ( u R x /\ u S y ) ) )
3 exrot3
 |-  ( E. u E. x E. y ( w = <. x , y >. /\ ( u R x /\ u S y ) ) <-> E. x E. y E. u ( w = <. x , y >. /\ ( u R x /\ u S y ) ) )
4 19.42v
 |-  ( E. u ( w = <. x , y >. /\ ( u R x /\ u S y ) ) <-> ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) )
5 4 2exbii
 |-  ( E. x E. y E. u ( w = <. x , y >. /\ ( u R x /\ u S y ) ) <-> E. x E. y ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) )
6 2 3 5 3bitri
 |-  ( E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) <-> E. x E. y ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) )
7 6 abbii
 |-  { w | E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) } = { w | E. x E. y ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) }
8 dfrn6
 |-  ran ( R |X. S ) = { w | [ w ] `' ( R |X. S ) =/= (/) }
9 n0
 |-  ( [ w ] `' ( R |X. S ) =/= (/) <-> E. u u e. [ w ] `' ( R |X. S ) )
10 elec1cnvxrn2
 |-  ( u e. _V -> ( u e. [ w ] `' ( R |X. S ) <-> E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) ) )
11 10 elv
 |-  ( u e. [ w ] `' ( R |X. S ) <-> E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) )
12 11 exbii
 |-  ( E. u u e. [ w ] `' ( R |X. S ) <-> E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) )
13 9 12 bitri
 |-  ( [ w ] `' ( R |X. S ) =/= (/) <-> E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) )
14 13 abbii
 |-  { w | [ w ] `' ( R |X. S ) =/= (/) } = { w | E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) }
15 8 14 eqtri
 |-  ran ( R |X. S ) = { w | E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) }
16 df-opab
 |-  { <. x , y >. | E. u ( u R x /\ u S y ) } = { w | E. x E. y ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) }
17 7 15 16 3eqtr4i
 |-  ran ( R |X. S ) = { <. x , y >. | E. u ( u R x /\ u S y ) }