Metamath Proof Explorer

Theorem disjxrnres5

Description: Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023)

Ref Expression
Assertion disjxrnres5 ⊢ Disj R ⋉ S ↾ A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ S ∩ v R ⋉ S = ∅

Proof

Step Hyp Ref Expression
1 xrnres2 ⊢ R ⋉ S ↾ A = R ⋉ S ↾ A
2 1 disjeqi ⊢ Disj R ⋉ S ↾ A ↔ Disj R ⋉ S ↾ A
3 xrnrel ⊢ Rel ⁡ R ⋉ S
4 disjres ⊢ Rel ⁡ R ⋉ S → Disj R ⋉ S ↾ A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ S ∩ v R ⋉ S = ∅
5 3 4 ax-mp ⊢ Disj R ⋉ S ↾ A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ S ∩ v R ⋉ S = ∅
6 2 5 bitr3i ⊢ Disj R ⋉ S ↾ A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ S ∩ v R ⋉ S = ∅