Metamath Proof Explorer

Theorem ssxpb

Description: A Cartesian product subclass relationship is equivalent to the conjunction of the analogous relationships for the factors. (Contributed by NM, 17-Dec-2008)

Ref Expression
Assertion ssxpb 
|- ( ( A X. B ) =/= (/) -> ( ( A X. B ) C_ ( C X. D ) <-> ( A C_ C /\ B C_ D ) ) )

Proof

Step Hyp Ref Expression
1 xpnz 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
2 dmxp 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
3 2 adantl 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> dom ( A X. B ) = A )
4 1 3 sylbir 
 |-  ( ( A X. B ) =/= (/) -> dom ( A X. B ) = A )
5 4 adantr 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> dom ( A X. B ) = A )
6 dmss 
 |-  ( ( A X. B ) C_ ( C X. D ) -> dom ( A X. B ) C_ dom ( C X. D ) )
7 6 adantl 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> dom ( A X. B ) C_ dom ( C X. D ) )
8 5 7 eqsstrrd 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> A C_ dom ( C X. D ) )
9 dmxpss 
 |-  dom ( C X. D ) C_ C
10 8 9 sstrdi 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> A C_ C )
11 rnxp 
 |-  ( A =/= (/) -> ran ( A X. B ) = B )
12 11 adantr 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ran ( A X. B ) = B )
13 1 12 sylbir 
 |-  ( ( A X. B ) =/= (/) -> ran ( A X. B ) = B )
14 13 adantr 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> ran ( A X. B ) = B )
15 rnss 
 |-  ( ( A X. B ) C_ ( C X. D ) -> ran ( A X. B ) C_ ran ( C X. D ) )
16 15 adantl 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> ran ( A X. B ) C_ ran ( C X. D ) )
17 14 16 eqsstrrd 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> B C_ ran ( C X. D ) )
18 rnxpss 
 |-  ran ( C X. D ) C_ D
19 17 18 sstrdi 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> B C_ D )
20 10 19 jca 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) C_ ( C X. D ) ) -> ( A C_ C /\ B C_ D ) )
21 20 ex 
 |-  ( ( A X. B ) =/= (/) -> ( ( A X. B ) C_ ( C X. D ) -> ( A C_ C /\ B C_ D ) ) )
22 xpss12 
 |-  ( ( A C_ C /\ B C_ D ) -> ( A X. B ) C_ ( C X. D ) )
23 21 22 impbid1 
 |-  ( ( A X. B ) =/= (/) -> ( ( A X. B ) C_ ( C X. D ) <-> ( A C_ C /\ B C_ D ) ) )