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 𝑅 )
qsdisjALTV.2 ( 𝜑𝐵 ∈ ( 𝐴 / 𝑅 ) )
qsdisjALTV.3 ( 𝜑𝐶 ∈ ( 𝐴 / 𝑅 ) )
Assertion qsdisjALTV ( 𝜑 → ( 𝐵 = 𝐶 ∨ ( 𝐵𝐶 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 qsdisjALTV.1 ( 𝜑 → EqvRel 𝑅 )
2 qsdisjALTV.2 ( 𝜑𝐵 ∈ ( 𝐴 / 𝑅 ) )
3 qsdisjALTV.3 ( 𝜑𝐶 ∈ ( 𝐴 / 𝑅 ) )
4 eqid ( 𝐴 / 𝑅 ) = ( 𝐴 / 𝑅 )
5 eqeq1 ( [ 𝑥 ] 𝑅 = 𝐵 → ( [ 𝑥 ] 𝑅 = 𝐶𝐵 = 𝐶 ) )
6 ineq1 ( [ 𝑥 ] 𝑅 = 𝐵 → ( [ 𝑥 ] 𝑅𝐶 ) = ( 𝐵𝐶 ) )
7 6 eqeq1d ( [ 𝑥 ] 𝑅 = 𝐵 → ( ( [ 𝑥 ] 𝑅𝐶 ) = ∅ ↔ ( 𝐵𝐶 ) = ∅ ) )
8 5 7 orbi12d ( [ 𝑥 ] 𝑅 = 𝐵 → ( ( [ 𝑥 ] 𝑅 = 𝐶 ∨ ( [ 𝑥 ] 𝑅𝐶 ) = ∅ ) ↔ ( 𝐵 = 𝐶 ∨ ( 𝐵𝐶 ) = ∅ ) ) )
9 eqeq2 ( [ 𝑦 ] 𝑅 = 𝐶 → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ↔ [ 𝑥 ] 𝑅 = 𝐶 ) )
10 ineq2 ( [ 𝑦 ] 𝑅 = 𝐶 → ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ( [ 𝑥 ] 𝑅𝐶 ) )
11 10 eqeq1d ( [ 𝑦 ] 𝑅 = 𝐶 → ( ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ↔ ( [ 𝑥 ] 𝑅𝐶 ) = ∅ ) )
12 9 11 orbi12d ( [ 𝑦 ] 𝑅 = 𝐶 → ( ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) ↔ ( [ 𝑥 ] 𝑅 = 𝐶 ∨ ( [ 𝑥 ] 𝑅𝐶 ) = ∅ ) ) )
13 1 ad2antrr ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦𝐴 ) → EqvRel 𝑅 )
14 eqvreldisj ( EqvRel 𝑅 → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) )
15 13 14 syl ( ( ( 𝜑𝑥𝐴 ) ∧ 𝑦𝐴 ) → ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ∨ ( [ 𝑥 ] 𝑅 ∩ [ 𝑦 ] 𝑅 ) = ∅ ) )
16 4 12 15 ectocld ( ( ( 𝜑𝑥𝐴 ) ∧ 𝐶 ∈ ( 𝐴 / 𝑅 ) ) → ( [ 𝑥 ] 𝑅 = 𝐶 ∨ ( [ 𝑥 ] 𝑅𝐶 ) = ∅ ) )
17 3 16 mpidan ( ( 𝜑𝑥𝐴 ) → ( [ 𝑥 ] 𝑅 = 𝐶 ∨ ( [ 𝑥 ] 𝑅𝐶 ) = ∅ ) )
18 4 8 17 ectocld ( ( 𝜑𝐵 ∈ ( 𝐴 / 𝑅 ) ) → ( 𝐵 = 𝐶 ∨ ( 𝐵𝐶 ) = ∅ ) )
19 2 18 mpdan ( 𝜑 → ( 𝐵 = 𝐶 ∨ ( 𝐵𝐶 ) = ∅ ) )