Theorem erprt

Description: The quotient set of an equivalence relation is a partition. (Contributed by Rodolfo Medina, 13-Oct-2010)

	Ref	Expression
Assertion	erprt	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}X\to \mathrm{Prt}\left(A/\underset{\dot{}}{\sim }\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(\underset{\dot{}}{\sim }\mathrm{Er}X\wedge \left(x\in \left(A/\underset{\dot{}}{\sim }\right)\wedge y\in \left(A/\underset{\dot{}}{\sim }\right)\right)\right)\to \underset{\dot{}}{\sim }\mathrm{Er}X$$
2		simprl	$$⊢\left(\underset{\dot{}}{\sim }\mathrm{Er}X\wedge \left(x\in \left(A/\underset{\dot{}}{\sim }\right)\wedge y\in \left(A/\underset{\dot{}}{\sim }\right)\right)\right)\to x\in \left(A/\underset{\dot{}}{\sim }\right)$$
3		simprr	$$⊢\left(\underset{\dot{}}{\sim }\mathrm{Er}X\wedge \left(x\in \left(A/\underset{\dot{}}{\sim }\right)\wedge y\in \left(A/\underset{\dot{}}{\sim }\right)\right)\right)\to y\in \left(A/\underset{\dot{}}{\sim }\right)$$
4	1 2 3	qsdisj	$$⊢\left(\underset{\dot{}}{\sim }\mathrm{Er}X\wedge \left(x\in \left(A/\underset{\dot{}}{\sim }\right)\wedge y\in \left(A/\underset{\dot{}}{\sim }\right)\right)\right)\to \left(x=y\vee x\cap y=\varnothing \right)$$
5	4	ralrimivva	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}X\to \forall x\in \left(A/\underset{\dot{}}{\sim }\right)\forall y\in \left(A/\underset{\dot{}}{\sim }\right)\left(x=y\vee x\cap y=\varnothing \right)$$
6		df-prt	$$⊢\mathrm{Prt}\left(A/\underset{\dot{}}{\sim }\right)\leftrightarrow \forall x\in \left(A/\underset{\dot{}}{\sim }\right)\forall y\in \left(A/\underset{\dot{}}{\sim }\right)\left(x=y\vee x\cap y=\varnothing \right)$$
7	5 6	sylibr	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}X\to \mathrm{Prt}\left(A/\underset{\dot{}}{\sim }\right)$$