Metamath Proof Explorer

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 ⁡ A ∧ dom ⁡ A ∩ dom ⁡ B = ∅ → A ∪ B ↾ dom ⁡ A = A

Proof

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