Theorem qsdisj2

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

	Ref	Expression
Assertion	qsdisj2	$$⊢R\mathrm{Er}X\to \underset{x\in A/R}{Disj}x$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(R\mathrm{Er}X\wedge \left(x\in \left(A/R\right)\wedge y\in \left(A/R\right)\right)\right)\to R\mathrm{Er}X$$
2		simprl	$$⊢\left(R\mathrm{Er}X\wedge \left(x\in \left(A/R\right)\wedge y\in \left(A/R\right)\right)\right)\to x\in \left(A/R\right)$$
3		simprr	$$⊢\left(R\mathrm{Er}X\wedge \left(x\in \left(A/R\right)\wedge y\in \left(A/R\right)\right)\right)\to y\in \left(A/R\right)$$
4	1 2 3	qsdisj	$$⊢\left(R\mathrm{Er}X\wedge \left(x\in \left(A/R\right)\wedge y\in \left(A/R\right)\right)\right)\to \left(x=y\vee x\cap y=\varnothing \right)$$
5	4	ralrimivva	$$⊢R\mathrm{Er}X\to \forall x\in \left(A/R\right)\forall y\in \left(A/R\right)\left(x=y\vee x\cap y=\varnothing \right)$$
6		id	$$⊢x=y\to x=y$$
7	6	disjor	$$⊢\underset{x\in A/R}{Disj}x\leftrightarrow \forall x\in \left(A/R\right)\forall y\in \left(A/R\right)\left(x=y\vee x\cap y=\varnothing \right)$$
8	5 7	sylibr	$$⊢R\mathrm{Er}X\to \underset{x\in A/R}{Disj}x$$