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 ) )