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

Metamath Proof Explorer

Theorem relresdm1

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

Ref Expression
Assertion relresdm1 ( ( 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 eqtrid ⊢ ( ( 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 eqtrid ⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∩ dom 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) ↾ dom 𝐴 ) = 𝐴 )