Metamath Proof Explorer


Theorem opth

Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of TakeutiZaring p. 16. Note that C and D are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995)

Ref Expression
Hypotheses opth1.1
|- A e. _V
opth1.2
|- B e. _V
Assertion opth
|- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 opth1.1
 |-  A e. _V
2 opth1.2
 |-  B e. _V
3 1 2 opth1
 |-  ( <. A , B >. = <. C , D >. -> A = C )
4 1 2 opi1
 |-  { A } e. <. A , B >.
5 id
 |-  ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
6 4 5 eleqtrid
 |-  ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
7 oprcl
 |-  ( { A } e. <. C , D >. -> ( C e. _V /\ D e. _V ) )
8 6 7 syl
 |-  ( <. A , B >. = <. C , D >. -> ( C e. _V /\ D e. _V ) )
9 8 simprd
 |-  ( <. A , B >. = <. C , D >. -> D e. _V )
10 3 opeq1d
 |-  ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )
11 10 5 eqtr3d
 |-  ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )
12 8 simpld
 |-  ( <. A , B >. = <. C , D >. -> C e. _V )
13 dfopg
 |-  ( ( C e. _V /\ B e. _V ) -> <. C , B >. = { { C } , { C , B } } )
14 12 2 13 sylancl
 |-  ( <. A , B >. = <. C , D >. -> <. C , B >. = { { C } , { C , B } } )
15 11 14 eqtr3d
 |-  ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )
16 dfopg
 |-  ( ( C e. _V /\ D e. _V ) -> <. C , D >. = { { C } , { C , D } } )
17 8 16 syl
 |-  ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , D } } )
18 15 17 eqtr3d
 |-  ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )
19 prex
 |-  { C , B } e. _V
20 prex
 |-  { C , D } e. _V
21 19 20 preqr2
 |-  ( { { C } , { C , B } } = { { C } , { C , D } } -> { C , B } = { C , D } )
22 18 21 syl
 |-  ( <. A , B >. = <. C , D >. -> { C , B } = { C , D } )
23 preq2
 |-  ( x = D -> { C , x } = { C , D } )
24 23 eqeq2d
 |-  ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )
25 eqeq2
 |-  ( x = D -> ( B = x <-> B = D ) )
26 24 25 imbi12d
 |-  ( x = D -> ( ( { C , B } = { C , x } -> B = x ) <-> ( { C , B } = { C , D } -> B = D ) ) )
27 vex
 |-  x e. _V
28 2 27 preqr2
 |-  ( { C , B } = { C , x } -> B = x )
29 26 28 vtoclg
 |-  ( D e. _V -> ( { C , B } = { C , D } -> B = D ) )
30 9 22 29 sylc
 |-  ( <. A , B >. = <. C , D >. -> B = D )
31 3 30 jca
 |-  ( <. A , B >. = <. C , D >. -> ( A = C /\ B = D ) )
32 opeq12
 |-  ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )
33 31 32 impbii
 |-  ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )