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

Metamath Proof Explorer

Theorem reldisjun

Description: Split a relation into two disjoint parts based on its domain. (Contributed by Thierry Arnoux, 9-Oct-2023)

Ref Expression
Assertion reldisjun ⊢ Rel ⁡ R ∧ dom ⁡ R = A ∪ B ∧ A ∩ B = ∅ → R = R ↾ A ∪ R ↾ B

Proof

Step Hyp Ref Expression
1 reseq2 ⊢ dom ⁡ R = A ∪ B → R ↾ dom ⁡ R = R ↾ A ∪ B
2 1 3ad2ant2 ⊢ Rel ⁡ R ∧ dom ⁡ R = A ∪ B ∧ A ∩ B = ∅ → R ↾ dom ⁡ R = R ↾ A ∪ B
3 resdm ⊢ Rel ⁡ R → R ↾ dom ⁡ R = R
4 3 3ad2ant1 ⊢ Rel ⁡ R ∧ dom ⁡ R = A ∪ B ∧ A ∩ B = ∅ → R ↾ dom ⁡ R = R
5 resundi ⊢ R ↾ A ∪ B = R ↾ A ∪ R ↾ B
6 5 a1i ⊢ Rel ⁡ R ∧ dom ⁡ R = A ∪ B ∧ A ∩ B = ∅ → R ↾ A ∪ B = R ↾ A ∪ R ↾ B
7 2 4 6 3eqtr3d ⊢ Rel ⁡ R ∧ dom ⁡ R = A ∪ B ∧ A ∩ B = ∅ → R = R ↾ A ∪ R ↾ B