Theorem prtex

Description: The equivalence relation generated by a partition is a set if and only if the partition itself is a set. (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypothesis	prtlem18.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}$$
Assertion	prtex	$$⊢\mathrm{Prt}A\to \left(\underset{\dot{}}{\sim }\in \mathrm{V}\leftrightarrow A\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		prtlem18.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}$$
2	1	prter1	$$⊢\mathrm{Prt}A\to \underset{\dot{}}{\sim }\mathrm{Er}\bigcup A$$
3		erexb	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}\bigcup A\to \left(\underset{\dot{}}{\sim }\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}\right)$$
4	2 3	syl	$$⊢\mathrm{Prt}A\to \left(\underset{\dot{}}{\sim }\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}\right)$$
5		uniexb	$$⊢A\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}$$
6	4 5	bitr4di	$$⊢\mathrm{Prt}A\to \left(\underset{\dot{}}{\sim }\in \mathrm{V}\leftrightarrow A\in \mathrm{V}\right)$$