Theorem xpexr

Description: If a Cartesian product is a set, one of its components must be a set. (Contributed by NM, 27-Aug-2006)

	Ref	Expression
Assertion	xpexr	|- ( ( A X. B ) e. C -> ( A e. _V \/ B e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		eleq1	|- ( A = (/) -> ( A e. _V <-> (/) e. _V ) )
3	1 2	mpbiri	|- ( A = (/) -> A e. _V )
4	3	pm2.24d	|- ( A = (/) -> ( -. A e. _V -> B e. _V ) )
5	4	a1d	|- ( A = (/) -> ( ( A X. B ) e. C -> ( -. A e. _V -> B e. _V ) ) )
6		rnexg	|- ( ( A X. B ) e. C -> ran ( A X. B ) e. _V )
7		rnxp	|- ( A =/= (/) -> ran ( A X. B ) = B )
8	7	eleq1d	|- ( A =/= (/) -> ( ran ( A X. B ) e. _V <-> B e. _V ) )
9	6 8	imbitrid	|- ( A =/= (/) -> ( ( A X. B ) e. C -> B e. _V ) )
10	9	a1dd	|- ( A =/= (/) -> ( ( A X. B ) e. C -> ( -. A e. _V -> B e. _V ) ) )
11	5 10	pm2.61ine	|- ( ( A X. B ) e. C -> ( -. A e. _V -> B e. _V ) )
12	11	orrd	|- ( ( A X. B ) e. C -> ( A e. _V \/ B e. _V ) )