Metamath Proof Explorer

Theorem fnunres1

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

Ref Expression
Assertion fnunres1 
|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` A ) = F )

Proof

Step Hyp Ref Expression
1 fndm 
 |-  ( F Fn A -> dom F = A )
2 1 3ad2ant1 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> dom F = A )
3 2 reseq2d 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` dom F ) = ( ( F u. G ) |` A ) )
4 fnrel 
 |-  ( F Fn A -> Rel F )
5 4 3ad2ant1 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> Rel F )
6 fndm 
 |-  ( G Fn B -> dom G = B )
7 6 3ad2ant2 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> dom G = B )
8 2 7 ineq12d 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( dom F i^i dom G ) = ( A i^i B ) )
9 simp3 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( A i^i B ) = (/) )
10 8 9 eqtrd 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( dom F i^i dom G ) = (/) )
11 funresdm1 
 |-  ( ( Rel F /\ ( dom F i^i dom G ) = (/) ) -> ( ( F u. G ) |` dom F ) = F )
12 5 10 11 syl2anc 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` dom F ) = F )
13 3 12 eqtr3d 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` A ) = F )