Metamath Proof Explorer

Theorem reldisjun

Description: Split a relation into two disjoint parts based on its domain. (Contributed by Thierry Arnoux, 9-Oct-2023)

Ref Expression
Assertion reldisjun 
|- ( ( Rel R /\ dom R = ( A u. B ) /\ ( A i^i B ) = (/) ) -> R = ( ( R |` A ) u. ( R |` B ) ) )

Proof

Step Hyp Ref Expression
1 reseq2 
 |-  ( dom R = ( A u. B ) -> ( R |` dom R ) = ( R |` ( A u. B ) ) )
2 1 3ad2ant2 
 |-  ( ( Rel R /\ dom R = ( A u. B ) /\ ( A i^i B ) = (/) ) -> ( R |` dom R ) = ( R |` ( A u. B ) ) )
3 resdm 
 |-  ( Rel R -> ( R |` dom R ) = R )
4 3 3ad2ant1 
 |-  ( ( Rel R /\ dom R = ( A u. B ) /\ ( A i^i B ) = (/) ) -> ( R |` dom R ) = R )
5 resundi 
 |-  ( R |` ( A u. B ) ) = ( ( R |` A ) u. ( R |` B ) )
6 5 a1i 
 |-  ( ( Rel R /\ dom R = ( A u. B ) /\ ( A i^i B ) = (/) ) -> ( R |` ( A u. B ) ) = ( ( R |` A ) u. ( R |` B ) ) )
7 2 4 6 3eqtr3d 
 |-  ( ( Rel R /\ dom R = ( A u. B ) /\ ( A i^i B ) = (/) ) -> R = ( ( R |` A ) u. ( R |` B ) ) )