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

Metamath Proof Explorer

Theorem qsdisj2

Description: A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016)

Ref Expression
Assertion qsdisj2 ( 𝑅 Er 𝑋 → Disj 𝑥 ∈ ( 𝐴 / 𝑅 ) 𝑥 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑅 Er 𝑋 ∧ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ∧ 𝑦 ∈ ( 𝐴 / 𝑅 ) ) ) → 𝑅 Er 𝑋 )
2 simprl ⊢ ( ( 𝑅 Er 𝑋 ∧ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ∧ 𝑦 ∈ ( 𝐴 / 𝑅 ) ) ) → 𝑥 ∈ ( 𝐴 / 𝑅 ) )
3 simprr ⊢ ( ( 𝑅 Er 𝑋 ∧ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ∧ 𝑦 ∈ ( 𝐴 / 𝑅 ) ) ) → 𝑦 ∈ ( 𝐴 / 𝑅 ) )
4 1 2 3 qsdisj ⊢ ( ( 𝑅 Er 𝑋 ∧ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ∧ 𝑦 ∈ ( 𝐴 / 𝑅 ) ) ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
5 4 ralrimivva ⊢ ( 𝑅 Er 𝑋 → ∀ 𝑥 ∈ ( 𝐴 / 𝑅 ) ∀ 𝑦 ∈ ( 𝐴 / 𝑅 ) ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
6 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
7 6 disjor ⊢ ( Disj 𝑥 ∈ ( 𝐴 / 𝑅 ) 𝑥 ↔ ∀ 𝑥 ∈ ( 𝐴 / 𝑅 ) ∀ 𝑦 ∈ ( 𝐴 / 𝑅 ) ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
8 5 7 sylibr ⊢ ( 𝑅 Er 𝑋 → Disj 𝑥 ∈ ( 𝐴 / 𝑅 ) 𝑥 )