Metamath Proof Explorer

Theorem disjsuc

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

Ref Expression
Assertion disjsuc ⊢ A ∈ V → Disj R ⋉ E -1 ↾ suc ⁡ A ↔ Disj R ⋉ E -1 ↾ A ∧ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅

Proof

Step Hyp Ref Expression
1 disjsuc2 ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ∧ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅
2 df-suc ⊢ suc ⁡ A = A ∪ A
3 2 reseq2i ⊢ E -1 ↾ suc ⁡ A = E -1 ↾ A ∪ A
4 3 xrneq2i ⊢ R ⋉ E -1 ↾ suc ⁡ A = R ⋉ E -1 ↾ A ∪ A
5 4 disjeqi ⊢ Disj R ⋉ E -1 ↾ suc ⁡ A ↔ Disj R ⋉ E -1 ↾ A ∪ A
6 disjxrnres5 ⊢ Disj R ⋉ E -1 ↾ A ∪ A ↔ ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅
7 5 6 bitri ⊢ Disj R ⋉ E -1 ↾ suc ⁡ A ↔ ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅
8 disjxrnres5 ⊢ Disj R ⋉ E -1 ↾ A ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅
9 8 anbi1i ⊢ Disj R ⋉ E -1 ↾ A ∧ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ⋉ E -1 ∩ v R ⋉ E -1 = ∅ ∧ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅
10 1 7 9 3bitr4g ⊢ A ∈ V → Disj R ⋉ E -1 ↾ suc ⁡ A ↔ Disj R ⋉ E -1 ↾ A ∧ ∀ u ∈ A u ∩ A = ∅ ∨ u R ∩ A R = ∅