This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) }