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 =/= (/) -> ( ( A X. B ) e. V -> B e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		eleq1a	|- ( (/) e. _V -> ( B = (/) -> B e. _V ) )
3	1 2	ax-mp	|- ( B = (/) -> B e. _V )
4	3	a1d	|- ( B = (/) -> ( ( A X. B ) e. V -> B e. _V ) )
5	4	a1d	|- ( B = (/) -> ( A =/= (/) -> ( ( A X. B ) e. V -> B e. _V ) ) )
6		xpnz	|- ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
7		xpexr2	|- ( ( ( A X. B ) e. V /\ ( A X. B ) =/= (/) ) -> ( A e. _V /\ B e. _V ) )
8	7	simprd	|- ( ( ( A X. B ) e. V /\ ( A X. B ) =/= (/) ) -> B e. _V )
9	8	expcom	|- ( ( A X. B ) =/= (/) -> ( ( A X. B ) e. V -> B e. _V ) )
10	6 9	sylbi	|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A X. B ) e. V -> B e. _V ) )
11	10	expcom	|- ( B =/= (/) -> ( A =/= (/) -> ( ( A X. B ) e. V -> B e. _V ) ) )
12	5 11	pm2.61ine	|- ( A =/= (/) -> ( ( A X. B ) e. V -> B e. _V ) )