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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		uncom	⊢ ( 𝐹 ∪ 𝐺 ) = ( 𝐺 ∪ 𝐹 )
2	1	reseq1i	⊢ ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐵 )
3		ineqcom	⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐵 ∩ 𝐴 ) = ∅ )
4		fnunres1	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐹 Fn 𝐴 ∧ ( 𝐵 ∩ 𝐴 ) = ∅ ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐵 ) = 𝐺 )
5	3 4	syl3an3b	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐹 Fn 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐵 ) = 𝐺 )
6	5	3com12	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐵 ) = 𝐺 )
7	2 6	eqtrid	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 )