Metamath Proof Explorer

Theorem funresdm1

Description: Restriction of a disjoint union to the domain of the first term. (Contributed by Thierry Arnoux, 9-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 resundir 
 |-  ( ( A u. B ) |` dom A ) = ( ( A |` dom A ) u. ( B |` dom A ) )
2 resdm 
 |-  ( Rel A -> ( A |` dom A ) = A )
3 2 adantr 
 |-  ( ( Rel A /\ ( dom A i^i dom B ) = (/) ) -> ( A |` dom A ) = A )
4 dmres 
 |-  dom ( B |` dom A ) = ( dom A i^i dom B )
5 simpr 
 |-  ( ( Rel A /\ ( dom A i^i dom B ) = (/) ) -> ( dom A i^i dom B ) = (/) )
6 4 5 eqtrid 
 |-  ( ( Rel A /\ ( dom A i^i dom B ) = (/) ) -> dom ( B |` dom A ) = (/) )
7 relres 
 |-  Rel ( B |` dom A )
8 reldm0 
 |-  ( Rel ( B |` dom A ) -> ( ( B |` dom A ) = (/) <-> dom ( B |` dom A ) = (/) ) )
9 7 8 ax-mp 
 |-  ( ( B |` dom A ) = (/) <-> dom ( B |` dom A ) = (/) )
10 6 9 sylibr 
 |-  ( ( Rel A /\ ( dom A i^i dom B ) = (/) ) -> ( B |` dom A ) = (/) )
11 3 10 uneq12d 
 |-  ( ( Rel A /\ ( dom A i^i dom B ) = (/) ) -> ( ( A |` dom A ) u. ( B |` dom A ) ) = ( A u. (/) ) )
12 un0 
 |-  ( A u. (/) ) = A
13 11 12 eqtrdi 
 |-  ( ( Rel A /\ ( dom A i^i dom B ) = (/) ) -> ( ( A |` dom A ) u. ( B |` dom A ) ) = A )
14 1 13 eqtrid 
 |-  ( ( Rel A /\ ( dom A i^i dom B ) = (/) ) -> ( ( A u. B ) |` dom A ) = A )