This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ineqcom 
 |-  ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
4 fnunres1 
 |-  ( ( G Fn B /\ F Fn A /\ ( B i^i A ) = (/) ) -> ( ( G u. F ) |` B ) = G )
5 3 4 syl3an3b 
 |-  ( ( G Fn B /\ F Fn A /\ ( A i^i B ) = (/) ) -> ( ( G u. F ) |` B ) = G )
6 5 3com12 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( G u. F ) |` B ) = G )
7 2 6 eqtrid 
 |-  ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` B ) = G )