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

Metamath Proof Explorer

Theorem qsdisjALTV

Description: Elements of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010) (Revised by Mario Carneiro, 11-Jul-2014) (Revised by Peter Mazsa, 3-Jun-2019)

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

Proof

Step Hyp Ref Expression
1 qsdisjALTV.1 ⊢ φ → EqvRel R
2 qsdisjALTV.2 ⊢ φ → B ∈ A / R
3 qsdisjALTV.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 → EqvRel R
14 eqvreldisj ⊢ EqvRel R → 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 = ∅