Theorem prtlem400

Description: Lemma for prter2 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypothesis	prtlem13.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}$$
Assertion	prtlem400	$$⊢\neg \varnothing \in \left(\bigcup A/\underset{\dot{}}{\sim }\right)$$

Proof

Step	Hyp	Ref	Expression
1		prtlem13.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}$$
2		neirr	$$⊢\neg \varnothing \ne \varnothing$$
3	1	prtlem16	$$⊢\mathrm{dom}\underset{\dot{}}{\sim }=\bigcup A$$
4		elqsn0	$$⊢\left(\mathrm{dom}\underset{\dot{}}{\sim }=\bigcup A\wedge \varnothing \in \left(\bigcup A/\underset{\dot{}}{\sim }\right)\right)\to \varnothing \ne \varnothing$$
5	3 4	mpan	$$⊢\varnothing \in \left(\bigcup A/\underset{\dot{}}{\sim }\right)\to \varnothing \ne \varnothing$$
6	2 5	mto	$$⊢\neg \varnothing \in \left(\bigcup A/\underset{\dot{}}{\sim }\right)$$