Theorem xpexr2

Description: If a nonempty Cartesian product is a set, so are both of its components. (Contributed by NM, 27-Aug-2006)

	Ref	Expression
Assertion	xpexr2	$$⊢\left(A\times B\in C\wedge A\times B\ne \varnothing \right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpnz	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow A\times B\ne \varnothing$$
2		dmxp	$$⊢B\ne \varnothing \to \mathrm{dom}\left(A\times B\right)=A$$
3	2	adantl	$$⊢\left(A\times B\in C\wedge B\ne \varnothing \right)\to \mathrm{dom}\left(A\times B\right)=A$$
4		dmexg	$$⊢A\times B\in C\to \mathrm{dom}\left(A\times B\right)\in \mathrm{V}$$
5	4	adantr	$$⊢\left(A\times B\in C\wedge B\ne \varnothing \right)\to \mathrm{dom}\left(A\times B\right)\in \mathrm{V}$$
6	3 5	eqeltrrd	$$⊢\left(A\times B\in C\wedge B\ne \varnothing \right)\to A\in \mathrm{V}$$
7		rnxp	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times B\right)=B$$
8	7	adantl	$$⊢\left(A\times B\in C\wedge A\ne \varnothing \right)\to \mathrm{ran}\left(A\times B\right)=B$$
9		rnexg	$$⊢A\times B\in C\to \mathrm{ran}\left(A\times B\right)\in \mathrm{V}$$
10	9	adantr	$$⊢\left(A\times B\in C\wedge A\ne \varnothing \right)\to \mathrm{ran}\left(A\times B\right)\in \mathrm{V}$$
11	8 10	eqeltrrd	$$⊢\left(A\times B\in C\wedge A\ne \varnothing \right)\to B\in \mathrm{V}$$
12	6 11	anim12dan	$$⊢\left(A\times B\in C\wedge \left(B\ne \varnothing \wedge A\ne \varnothing \right)\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
13	12	ancom2s	$$⊢\left(A\times B\in C\wedge \left(A\ne \varnothing \wedge B\ne \varnothing \right)\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
14	1 13	sylan2br	$$⊢\left(A\times B\in C\wedge A\times B\ne \varnothing \right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$