Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 xpnz 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
2 dmxp 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
3 2 adantl 
 |-  ( ( ( A X. B ) e. C /\ B =/= (/) ) -> dom ( A X. B ) = A )
4 dmexg 
 |-  ( ( A X. B ) e. C -> dom ( A X. B ) e. _V )
5 4 adantr 
 |-  ( ( ( A X. B ) e. C /\ B =/= (/) ) -> dom ( A X. B ) e. _V )
6 3 5 eqeltrrd 
 |-  ( ( ( A X. B ) e. C /\ B =/= (/) ) -> A e. _V )
7 rnxp 
 |-  ( A =/= (/) -> ran ( A X. B ) = B )
8 7 adantl 
 |-  ( ( ( A X. B ) e. C /\ A =/= (/) ) -> ran ( A X. B ) = B )
9 rnexg 
 |-  ( ( A X. B ) e. C -> ran ( A X. B ) e. _V )
10 9 adantr 
 |-  ( ( ( A X. B ) e. C /\ A =/= (/) ) -> ran ( A X. B ) e. _V )
11 8 10 eqeltrrd 
 |-  ( ( ( A X. B ) e. C /\ A =/= (/) ) -> B e. _V )
12 6 11 anim12dan 
 |-  ( ( ( A X. B ) e. C /\ ( B =/= (/) /\ A =/= (/) ) ) -> ( A e. _V /\ B e. _V ) )
13 12 ancom2s 
 |-  ( ( ( A X. B ) e. C /\ ( A =/= (/) /\ B =/= (/) ) ) -> ( A e. _V /\ B e. _V ) )
14 1 13 sylan2br 
 |-  ( ( ( A X. B ) e. C /\ ( A X. B ) =/= (/) ) -> ( A e. _V /\ B e. _V ) )