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

Metamath Proof Explorer

Theorem brxrn2

Description: A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020)

		Ref	Expression
	Assertion	brxrn2	\|- ( A e. V -> ( A ( R \|X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrnss3v	\|- ( R \|X. S ) C_ ( _V X. ( _V X. _V ) )
2	1	brel	\|- ( A ( R \|X. S ) B -> ( A e. _V /\ B e. ( _V X. _V ) ) )
3	2	simprd	\|- ( A ( R \|X. S ) B -> B e. ( _V X. _V ) )
4		elvv	\|- ( B e. ( _V X. _V ) <-> E. x E. y B = <. x , y >. )
5	3 4	sylib	\|- ( A ( R \|X. S ) B -> E. x E. y B = <. x , y >. )
6	5	pm4.71ri	\|- ( A ( R \|X. S ) B <-> ( E. x E. y B = <. x , y >. /\ A ( R \|X. S ) B ) )
7		19.41vv	\|- ( E. x E. y ( B = <. x , y >. /\ A ( R \|X. S ) B ) <-> ( E. x E. y B = <. x , y >. /\ A ( R \|X. S ) B ) )
8		breq2	\|- ( B = <. x , y >. -> ( A ( R \|X. S ) B <-> A ( R \|X. S ) <. x , y >. ) )
9	8	pm5.32i	\|- ( ( B = <. x , y >. /\ A ( R \|X. S ) B ) <-> ( B = <. x , y >. /\ A ( R \|X. S ) <. x , y >. ) )
10	9	2exbii	\|- ( E. x E. y ( B = <. x , y >. /\ A ( R \|X. S ) B ) <-> E. x E. y ( B = <. x , y >. /\ A ( R \|X. S ) <. x , y >. ) )
11	6 7 10	3bitr2i	\|- ( A ( R \|X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A ( R \|X. S ) <. x , y >. ) )
12		brxrn	\|- ( ( A e. V /\ x e. _V /\ y e. _V ) -> ( A ( R \|X. S ) <. x , y >. <-> ( A R x /\ A S y ) ) )
13	12	el3v23	\|- ( A e. V -> ( A ( R \|X. S ) <. x , y >. <-> ( A R x /\ A S y ) ) )
14	13	anbi2d	\|- ( A e. V -> ( ( B = <. x , y >. /\ A ( R \|X. S ) <. x , y >. ) <-> ( B = <. x , y >. /\ ( A R x /\ A S y ) ) ) )
15		3anass	\|- ( ( B = <. x , y >. /\ A R x /\ A S y ) <-> ( B = <. x , y >. /\ ( A R x /\ A S y ) ) )
16	14 15	bitr4di	\|- ( A e. V -> ( ( B = <. x , y >. /\ A ( R \|X. S ) <. x , y >. ) <-> ( B = <. x , y >. /\ A R x /\ A S y ) ) )
17	16	2exbidv	\|- ( A e. V -> ( E. x E. y ( B = <. x , y >. /\ A ( R \|X. S ) <. x , y >. ) <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )
18	11 17	bitrid	\|- ( A e. V -> ( A ( R \|X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) )