This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xp11

Description: The Cartesian product of nonempty classes is a one-to-one "function" of its two "arguments". In other words, two Cartesian products, at least one with nonempty factors, are equal if and only if their respective factors are equal. (Contributed by NM, 31-May-2008)

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

Proof

Step Hyp Ref Expression
1 xpnz 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
2 anidm 
 |-  ( ( ( A X. B ) =/= (/) /\ ( A X. B ) =/= (/) ) <-> ( A X. B ) =/= (/) )
3 neeq1 
 |-  ( ( A X. B ) = ( C X. D ) -> ( ( A X. B ) =/= (/) <-> ( C X. D ) =/= (/) ) )
4 3 anbi2d 
 |-  ( ( A X. B ) = ( C X. D ) -> ( ( ( A X. B ) =/= (/) /\ ( A X. B ) =/= (/) ) <-> ( ( A X. B ) =/= (/) /\ ( C X. D ) =/= (/) ) ) )
5 2 4 bitr3id 
 |-  ( ( A X. B ) = ( C X. D ) -> ( ( A X. B ) =/= (/) <-> ( ( A X. B ) =/= (/) /\ ( C X. D ) =/= (/) ) ) )
6 eqimss 
 |-  ( ( A X. B ) = ( C X. D ) -> ( A X. B ) C_ ( C X. D ) )
7 ssxpb 
 |-  ( ( A X. B ) =/= (/) -> ( ( A X. B ) C_ ( C X. D ) <-> ( A C_ C /\ B C_ D ) ) )
8 6 7 syl5ibcom 
 |-  ( ( A X. B ) = ( C X. D ) -> ( ( A X. B ) =/= (/) -> ( A C_ C /\ B C_ D ) ) )
9 eqimss2 
 |-  ( ( A X. B ) = ( C X. D ) -> ( C X. D ) C_ ( A X. B ) )
10 ssxpb 
 |-  ( ( C X. D ) =/= (/) -> ( ( C X. D ) C_ ( A X. B ) <-> ( C C_ A /\ D C_ B ) ) )
11 9 10 syl5ibcom 
 |-  ( ( A X. B ) = ( C X. D ) -> ( ( C X. D ) =/= (/) -> ( C C_ A /\ D C_ B ) ) )
12 8 11 anim12d 
 |-  ( ( A X. B ) = ( C X. D ) -> ( ( ( A X. B ) =/= (/) /\ ( C X. D ) =/= (/) ) -> ( ( A C_ C /\ B C_ D ) /\ ( C C_ A /\ D C_ B ) ) ) )
13 an4 
 |-  ( ( ( A C_ C /\ B C_ D ) /\ ( C C_ A /\ D C_ B ) ) <-> ( ( A C_ C /\ C C_ A ) /\ ( B C_ D /\ D C_ B ) ) )
14 eqss 
 |-  ( A = C <-> ( A C_ C /\ C C_ A ) )
15 eqss 
 |-  ( B = D <-> ( B C_ D /\ D C_ B ) )
16 14 15 anbi12i 
 |-  ( ( A = C /\ B = D ) <-> ( ( A C_ C /\ C C_ A ) /\ ( B C_ D /\ D C_ B ) ) )
17 13 16 bitr4i 
 |-  ( ( ( A C_ C /\ B C_ D ) /\ ( C C_ A /\ D C_ B ) ) <-> ( A = C /\ B = D ) )
18 12 17 imbitrdi 
 |-  ( ( A X. B ) = ( C X. D ) -> ( ( ( A X. B ) =/= (/) /\ ( C X. D ) =/= (/) ) -> ( A = C /\ B = D ) ) )
19 5 18 sylbid 
 |-  ( ( A X. B ) = ( C X. D ) -> ( ( A X. B ) =/= (/) -> ( A = C /\ B = D ) ) )
20 19 com12 
 |-  ( ( A X. B ) =/= (/) -> ( ( A X. B ) = ( C X. D ) -> ( A = C /\ B = D ) ) )
21 1 20 sylbi 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A X. B ) = ( C X. D ) -> ( A = C /\ B = D ) ) )
22 xpeq12 
 |-  ( ( A = C /\ B = D ) -> ( A X. B ) = ( C X. D ) )
23 21 22 impbid1 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( ( A X. B ) = ( C X. D ) <-> ( A = C /\ B = D ) ) )