Metamath Proof Explorer

Theorem qsdisj

Description: Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010) (Revised by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypotheses qsdisj.1 ⊢ φ → R Er X
qsdisj.2 ⊢ φ → B ∈ A / R
qsdisj.3 ⊢ φ → C ∈ A / R
Assertion qsdisj ⊢ φ → B = C ∨ B ∩ C = ∅

Proof

Step Hyp Ref Expression
1 qsdisj.1 ⊢ φ → R Er X
2 qsdisj.2 ⊢ φ → B ∈ A / R
3 qsdisj.3 ⊢ φ → C ∈ A / R
4 eqid ⊢ A / R = A / R
5 eqeq1 ⊢ x R = B → x R = C ↔ B = C
6 ineq1 ⊢ x R = B → x R ∩ C = B ∩ C
7 6 eqeq1d ⊢ x R = B → x R ∩ C = ∅ ↔ B ∩ C = ∅
8 5 7 orbi12d ⊢ x R = B → x R = C ∨ x R ∩ C = ∅ ↔ B = C ∨ B ∩ C = ∅
9 eqeq2 ⊢ y R = C → x R = y R ↔ x R = C
10 ineq2 ⊢ y R = C → x R ∩ y R = x R ∩ C
11 10 eqeq1d ⊢ y R = C → x R ∩ y R = ∅ ↔ x R ∩ C = ∅
12 9 11 orbi12d ⊢ y R = C → x R = y R ∨ x R ∩ y R = ∅ ↔ x R = C ∨ x R ∩ C = ∅
13 1 ad2antrr ⊢ φ ∧ x ∈ A ∧ y ∈ A → R Er X
14 erdisj ⊢ R Er X → x R = y R ∨ x R ∩ y R = ∅
15 13 14 syl ⊢ φ ∧ x ∈ A ∧ y ∈ A → x R = y R ∨ x R ∩ y R = ∅
16 4 12 15 ectocld ⊢ φ ∧ x ∈ A ∧ C ∈ A / R → x R = C ∨ x R ∩ C = ∅
17 3 16 mpidan ⊢ φ ∧ x ∈ A → x R = C ∨ x R ∩ C = ∅
18 4 8 17 ectocld ⊢ φ ∧ B ∈ A / R → B = C ∨ B ∩ C = ∅
19 2 18 mpdan ⊢ φ → B = C ∨ B ∩ C = ∅