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		simp2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐺 Fn 𝐵 )
4		simp1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐹 Fn 𝐴 )
5		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
6		simp3	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
7	5 6	eqtr3id	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐵 ∩ 𝐴 ) = ∅ )
8		fnunres1	⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐹 Fn 𝐴 ∧ ( 𝐵 ∩ 𝐴 ) = ∅ ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐵 ) = 𝐺 )
9	3 4 7 8	syl3anc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐵 ) = 𝐺 )
10	2 9	syl5eq	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 )