Metamath Proof Explorer


Theorem fnunres2

Description: Restriction of a disjoint union to the domain of the second function. (Contributed by Thierry Arnoux, 12-Oct-2023)

Ref Expression
Assertion fnunres2 F Fn A G Fn B A B = F G B = G

Proof

Step Hyp Ref Expression
1 uncom F G = G F
2 1 reseq1i F G B = G F B
3 simp2 F Fn A G Fn B A B = G Fn B
4 simp1 F Fn A G Fn B A B = F Fn A
5 incom A B = B A
6 simp3 F Fn A G Fn B A B = A B =
7 5 6 eqtr3id F Fn A G Fn B A B = B A =
8 fnunres1 G Fn B F Fn A B A = G F B = G
9 3 4 7 8 syl3anc F Fn A G Fn B A B = G F B = G
10 2 9 syl5eq F Fn A G Fn B A B = F G B = G