Theorem funresdm1

Description: Restriction of a disjoint union to the domain of the first term. (Contributed by Thierry Arnoux, 9-Dec-2021)

	Ref	Expression
Assertion	funresdm1	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) ↾ dom 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		resundir	⊢ ( ( 𝐴 ∪ 𝐵 ) ↾ dom 𝐴 ) = ( ( 𝐴 ↾ dom 𝐴 ) ∪ ( 𝐵 ↾ dom 𝐴 ) )
2		resdm	⊢ ( Rel 𝐴 → ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )
3	2	adantr	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )
4		dmres	⊢ dom ( 𝐵 ↾ dom 𝐴 ) = ( dom 𝐴 ∩ dom 𝐵 )
5		simpr	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → ( dom 𝐴 ∩ dom 𝐵 ) = ∅ )
6	4 5	syl5eq	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → dom ( 𝐵 ↾ dom 𝐴 ) = ∅ )
7		relres	⊢ Rel ( 𝐵 ↾ dom 𝐴 )
8		reldm0	⊢ ( Rel ( 𝐵 ↾ dom 𝐴 ) → ( ( 𝐵 ↾ dom 𝐴 ) = ∅ ↔ dom ( 𝐵 ↾ dom 𝐴 ) = ∅ ) )
9	7 8	ax-mp	⊢ ( ( 𝐵 ↾ dom 𝐴 ) = ∅ ↔ dom ( 𝐵 ↾ dom 𝐴 ) = ∅ )
10	6 9	sylibr	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → ( 𝐵 ↾ dom 𝐴 ) = ∅ )
11	3 10	uneq12d	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → ( ( 𝐴 ↾ dom 𝐴 ) ∪ ( 𝐵 ↾ dom 𝐴 ) ) = ( 𝐴 ∪ ∅ ) )
12		un0	⊢ ( 𝐴 ∪ ∅ ) = 𝐴
13	11 12	eqtrdi	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → ( ( 𝐴 ↾ dom 𝐴 ) ∪ ( 𝐵 ↾ dom 𝐴 ) ) = 𝐴 )
14	1 13	syl5eq	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) ↾ dom 𝐴 ) = 𝐴 )