Metamath Proof Explorer

Theorem xppss12

Description: Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022)

Ref Expression
Assertion xppss12 
|- ( ( A C. B /\ C C. D ) -> ( A X. C ) C. ( B X. D ) )

Proof

Step Hyp Ref Expression
1 pssss 
 |-  ( A C. B -> A C_ B )
2 pssss 
 |-  ( C C. D -> C C_ D )
3 xpss12 
 |-  ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )
4 1 2 3 syl2an 
 |-  ( ( A C. B /\ C C. D ) -> ( A X. C ) C_ ( B X. D ) )
5 simpl 
 |-  ( ( A C. B /\ C C. D ) -> A C. B )
6 pssne 
 |-  ( A C. B -> A =/= B )
7 6 necomd 
 |-  ( A C. B -> B =/= A )
8 neneq 
 |-  ( B =/= A -> -. B = A )
9 8 intnanrd 
 |-  ( B =/= A -> -. ( B = A /\ D = C ) )
10 5 7 9 3syl 
 |-  ( ( A C. B /\ C C. D ) -> -. ( B = A /\ D = C ) )
11 pssn0 
 |-  ( A C. B -> B =/= (/) )
12 pssn0 
 |-  ( C C. D -> D =/= (/) )
13 xp11 
 |-  ( ( B =/= (/) /\ D =/= (/) ) -> ( ( B X. D ) = ( A X. C ) <-> ( B = A /\ D = C ) ) )
14 11 12 13 syl2an 
 |-  ( ( A C. B /\ C C. D ) -> ( ( B X. D ) = ( A X. C ) <-> ( B = A /\ D = C ) ) )
15 10 14 mtbird 
 |-  ( ( A C. B /\ C C. D ) -> -. ( B X. D ) = ( A X. C ) )
16 neqne 
 |-  ( -. ( B X. D ) = ( A X. C ) -> ( B X. D ) =/= ( A X. C ) )
17 16 necomd 
 |-  ( -. ( B X. D ) = ( A X. C ) -> ( A X. C ) =/= ( B X. D ) )
18 15 17 syl 
 |-  ( ( A C. B /\ C C. D ) -> ( A X. C ) =/= ( B X. D ) )
19 df-pss 
 |-  ( ( A X. C ) C. ( B X. D ) <-> ( ( A X. C ) C_ ( B X. D ) /\ ( A X. C ) =/= ( B X. D ) ) )
20 4 18 19 sylanbrc 
 |-  ( ( A C. B /\ C C. D ) -> ( A X. C ) C. ( B X. D ) )