Metamath Proof Explorer

Theorem disjxrnres5

Description: Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023)

Ref Expression
Assertion disjxrnres5 
|- ( Disj ( R |X. ( S |` A ) ) <-> A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. S ) i^i [ v ] ( R |X. S ) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 xrnres2 
 |-  ( ( R |X. S ) |` A ) = ( R |X. ( S |` A ) )
2 1 disjeqi 
 |-  ( Disj ( ( R |X. S ) |` A ) <-> Disj ( R |X. ( S |` A ) ) )
3 xrnrel 
 |-  Rel ( R |X. S )
4 disjres 
 |-  ( Rel ( R |X. S ) -> ( Disj ( ( R |X. S ) |` A ) <-> A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. S ) i^i [ v ] ( R |X. S ) ) = (/) ) ) )
5 3 4 ax-mp 
 |-  ( Disj ( ( R |X. S ) |` A ) <-> A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. S ) i^i [ v ] ( R |X. S ) ) = (/) ) )
6 2 5 bitr3i 
 |-  ( Disj ( R |X. ( S |` A ) ) <-> A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. S ) i^i [ v ] ( R |X. S ) ) = (/) ) )