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 i^i B ) = (/) ) -> ( ( F u. G ) |` B ) = G )

Proof

Step	Hyp	Ref	Expression
1		uncom	|- ( F u. G ) = ( G u. F )
2	1	reseq1i	|- ( ( F u. G ) |` B ) = ( ( G u. F ) |` B )
3		simp2	|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> G Fn B )
4		simp1	|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> F Fn A )
5		incom	|- ( A i^i B ) = ( B i^i A )
6		simp3	|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( A i^i B ) = (/) )
7	5 6	eqtr3id	|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( B i^i A ) = (/) )
8		fnunres1	|- ( ( G Fn B /\ F Fn A /\ ( B i^i A ) = (/) ) -> ( ( G u. F ) |` B ) = G )
9	3 4 7 8	syl3anc	|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( G u. F ) |` B ) = G )
10	2 9	syl5eq	|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` B ) = G )