Metamath Proof Explorer

Theorem disjres

Description: Disjoint restriction. (Contributed by Peter Mazsa, 25-Aug-2023)

Ref Expression
Assertion disjres ⊢ Rel ⁡ R → Disj R ↾ A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ R ↾ A
2 dfdisjALTV4 ⊢ Disj R ↾ A ↔ ∀ x ∃* u u R ↾ A x ∧ Rel ⁡ R ↾ A
3 1 2 mpbiran2 ⊢ Disj R ↾ A ↔ ∀ x ∃* u u R ↾ A x
4 brres ⊢ x ∈ V → u R ↾ A x ↔ u ∈ A ∧ u R x
5 4 elv ⊢ u R ↾ A x ↔ u ∈ A ∧ u R x
6 5 mobii ⊢ ∃* u u R ↾ A x ↔ ∃* u u ∈ A ∧ u R x
7 df-rmo ⊢ ∃* u ∈ A u R x ↔ ∃* u u ∈ A ∧ u R x
8 6 7 bitr4i ⊢ ∃* u u R ↾ A x ↔ ∃* u ∈ A u R x
9 8 albii ⊢ ∀ x ∃* u u R ↾ A x ↔ ∀ x ∃* u ∈ A u R x
10 3 9 bitri ⊢ Disj R ↾ A ↔ ∀ x ∃* u ∈ A u R x
11 id ⊢ u = v → u = v
12 11 inecmo ⊢ Rel ⁡ R → ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ↔ ∀ x ∃* u ∈ A u R x
13 10 12 bitr4id ⊢ Rel ⁡ R → Disj R ↾ A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅