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	|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
Assertion	prtlem400	|- -. (/) e. ( U. A /. .~ )

Proof

Step	Hyp	Ref	Expression
1		prtlem13.1	|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2		neirr	|- -. (/) =/= (/)
3	1	prtlem16	|- dom .~ = U. A
4		elqsn0	|- ( ( dom .~ = U. A /\ (/) e. ( U. A /. .~ ) ) -> (/) =/= (/) )
5	3 4	mpan	|- ( (/) e. ( U. A /. .~ ) -> (/) =/= (/) )
6	2 5	mto	|- -. (/) e. ( U. A /. .~ )