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 𝑅 )
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 ⊢ ( 𝜑 → ( 𝐵 = 𝐶 ∨ ( 𝐵 ∩ 𝐶 ) = ∅ ) )