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 B = F 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 B = dom F = A
3 2 reseq2d F Fn A G Fn B A B = F G dom F = F G A
4 fnrel F Fn A Rel F
5 4 3ad2ant1 F Fn A G Fn B A B = Rel F
6 fndm G Fn B dom G = B
7 6 3ad2ant2 F Fn A G Fn B A B = dom G = B
8 2 7 ineq12d F Fn A G Fn B A B = dom F dom G = A B
9 simp3 F Fn A G Fn B A B = A B =
10 8 9 eqtrd F Fn A G Fn B A B = dom F dom G =
11 funresdm1 Rel F dom F dom G = F G dom F = F
12 5 10 11 syl2anc F Fn A G Fn B A B = F G dom F = F
13 3 12 eqtr3d F Fn A G Fn B A B = F G A = F