Theorem ixpprc

Description: A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain A , which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015)

	Ref	Expression
Assertion	ixpprc	$$⊢\neg A\in \mathrm{V}\to \underset{x\in A}{⨉}B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		neq0	$$⊢\neg \underset{x\in A}{⨉}B=\varnothing \leftrightarrow \exists ff\in \underset{x\in A}{⨉}B$$
2		ixpfn	$$⊢f\in \underset{x\in A}{⨉}B\to fFnA$$
3		fndm	$$⊢fFnA\to \mathrm{dom}f=A$$
4		vex	$$⊢f\in \mathrm{V}$$
5	4	dmex	$$⊢\mathrm{dom}f\in \mathrm{V}$$
6	3 5	eqeltrrdi	$$⊢fFnA\to A\in \mathrm{V}$$
7	2 6	syl	$$⊢f\in \underset{x\in A}{⨉}B\to A\in \mathrm{V}$$
8	7	exlimiv	$$⊢\exists ff\in \underset{x\in A}{⨉}B\to A\in \mathrm{V}$$
9	1 8	sylbi	$$⊢\neg \underset{x\in A}{⨉}B=\varnothing \to A\in \mathrm{V}$$
10	9	con1i	$$⊢\neg A\in \mathrm{V}\to \underset{x\in A}{⨉}B=\varnothing$$