Metamath Proof Explorer

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 syl5ib 
 |-  ( 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 ) )