Theorem bj-xpnzex

Description: If the first factor of a product is nonempty, and the product is a set, then the second factor is a set. UPDATE: this is actually the curried (exported) form of xpexcnv (up to commutation in the product). (Contributed by BJ, 6-Oct-2018) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-xpnzex	$$⊢A\ne \varnothing \to \left(A\times B\in V\to B\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		eleq1a	$$⊢\varnothing \in \mathrm{V}\to \left(B=\varnothing \to B\in \mathrm{V}\right)$$
3	1 2	ax-mp	$$⊢B=\varnothing \to B\in \mathrm{V}$$
4	3	a1d	$$⊢B=\varnothing \to \left(A\times B\in V\to B\in \mathrm{V}\right)$$
5	4	a1d	$$⊢B=\varnothing \to \left(A\ne \varnothing \to \left(A\times B\in V\to B\in \mathrm{V}\right)\right)$$
6		xpnz	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\leftrightarrow A\times B\ne \varnothing$$
7		xpexr2	$$⊢\left(A\times B\in V\wedge A\times B\ne \varnothing \right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
8	7	simprd	$$⊢\left(A\times B\in V\wedge A\times B\ne \varnothing \right)\to B\in \mathrm{V}$$
9	8	expcom	$$⊢A\times B\ne \varnothing \to \left(A\times B\in V\to B\in \mathrm{V}\right)$$
10	6 9	sylbi	$$⊢\left(A\ne \varnothing \wedge B\ne \varnothing \right)\to \left(A\times B\in V\to B\in \mathrm{V}\right)$$
11	10	expcom	$$⊢B\ne \varnothing \to \left(A\ne \varnothing \to \left(A\times B\in V\to B\in \mathrm{V}\right)\right)$$
12	5 11	pm2.61ine	$$⊢A\ne \varnothing \to \left(A\times B\in V\to B\in \mathrm{V}\right)$$