# 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 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to {\left({F}\cup {G}\right)↾}_{{A}}={F}$

### Proof

Step Hyp Ref Expression
1 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
2 1 3ad2ant1 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to \mathrm{dom}{F}={A}$
3 2 reseq2d ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to {\left({F}\cup {G}\right)↾}_{\mathrm{dom}{F}}={\left({F}\cup {G}\right)↾}_{{A}}$
4 fnrel ${⊢}{F}Fn{A}\to \mathrm{Rel}{F}$
5 4 3ad2ant1 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to \mathrm{Rel}{F}$
6 fndm ${⊢}{G}Fn{B}\to \mathrm{dom}{G}={B}$
7 6 3ad2ant2 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to \mathrm{dom}{G}={B}$
8 2 7 ineq12d ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to \mathrm{dom}{F}\cap \mathrm{dom}{G}={A}\cap {B}$
9 simp3 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to {A}\cap {B}=\varnothing$
10 8 9 eqtrd ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing$
11 funresdm1 ${⊢}\left(\mathrm{Rel}{F}\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to {\left({F}\cup {G}\right)↾}_{\mathrm{dom}{F}}={F}$
12 5 10 11 syl2anc ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to {\left({F}\cup {G}\right)↾}_{\mathrm{dom}{F}}={F}$
13 3 12 eqtr3d ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge {A}\cap {B}=\varnothing \right)\to {\left({F}\cup {G}\right)↾}_{{A}}={F}$