Metamath Proof Explorer

Theorem omopthi

Description: An ordered pair theorem for _om . Theorem 17.3 of Quine p. 124. This proof is adapted from nn0opthi . (Contributed by Scott Fenton, 16-Apr-2012) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses omopth.1 
|- A e. _om
omopth.2 
|- B e. _om
omopth.3 
|- C e. _om
omopth.4 
|- D e. _om
Assertion omopthi 
|- ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) )

Proof

Step Hyp Ref Expression
1 omopth.1 
 |-  A e. _om
2 omopth.2 
 |-  B e. _om
3 omopth.3 
 |-  C e. _om
4 omopth.4 
 |-  D e. _om
5 1 2 nnacli 
 |-  ( A +o B ) e. _om
6 5 nnoni 
 |-  ( A +o B ) e. On
7 6 onordi 
 |-  Ord ( A +o B )
8 3 4 nnacli 
 |-  ( C +o D ) e. _om
9 8 nnoni 
 |-  ( C +o D ) e. On
10 9 onordi 
 |-  Ord ( C +o D )
11 ordtri3 
 |-  ( ( Ord ( A +o B ) /\ Ord ( C +o D ) ) -> ( ( A +o B ) = ( C +o D ) <-> -. ( ( A +o B ) e. ( C +o D ) \/ ( C +o D ) e. ( A +o B ) ) ) )
12 7 10 11 mp2an 
 |-  ( ( A +o B ) = ( C +o D ) <-> -. ( ( A +o B ) e. ( C +o D ) \/ ( C +o D ) e. ( A +o B ) ) )
13 12 con2bii 
 |-  ( ( ( A +o B ) e. ( C +o D ) \/ ( C +o D ) e. ( A +o B ) ) <-> -. ( A +o B ) = ( C +o D ) )
14 1 2 8 4 omopthlem2 
 |-  ( ( A +o B ) e. ( C +o D ) -> -. ( ( ( C +o D ) .o ( C +o D ) ) +o D ) = ( ( ( A +o B ) .o ( A +o B ) ) +o B ) )
15 eqcom 
 |-  ( ( ( ( C +o D ) .o ( C +o D ) ) +o D ) = ( ( ( A +o B ) .o ( A +o B ) ) +o B ) <-> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) )
16 14 15 sylnib 
 |-  ( ( A +o B ) e. ( C +o D ) -> -. ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) )
17 3 4 5 2 omopthlem2 
 |-  ( ( C +o D ) e. ( A +o B ) -> -. ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) )
18 16 17 jaoi 
 |-  ( ( ( A +o B ) e. ( C +o D ) \/ ( C +o D ) e. ( A +o B ) ) -> -. ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) )
19 13 18 sylbir 
 |-  ( -. ( A +o B ) = ( C +o D ) -> -. ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) )
20 19 con4i 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( A +o B ) = ( C +o D ) )
21 id 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) )
22 20 20 oveq12d 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( ( A +o B ) .o ( A +o B ) ) = ( ( C +o D ) .o ( C +o D ) ) )
23 22 oveq1d 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o D ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) )
24 21 23 eqtr4d 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( A +o B ) .o ( A +o B ) ) +o D ) )
25 5 5 nnmcli 
 |-  ( ( A +o B ) .o ( A +o B ) ) e. _om
26 nnacan 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) e. _om /\ B e. _om /\ D e. _om ) -> ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( A +o B ) .o ( A +o B ) ) +o D ) <-> B = D ) )
27 25 2 4 26 mp3an 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( A +o B ) .o ( A +o B ) ) +o D ) <-> B = D )
28 24 27 sylib 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> B = D )
29 28 oveq2d 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( C +o B ) = ( C +o D ) )
30 20 29 eqtr4d 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( A +o B ) = ( C +o B ) )
31 nnacom 
 |-  ( ( B e. _om /\ A e. _om ) -> ( B +o A ) = ( A +o B ) )
32 2 1 31 mp2an 
 |-  ( B +o A ) = ( A +o B )
33 nnacom 
 |-  ( ( B e. _om /\ C e. _om ) -> ( B +o C ) = ( C +o B ) )
34 2 3 33 mp2an 
 |-  ( B +o C ) = ( C +o B )
35 30 32 34 3eqtr4g 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( B +o A ) = ( B +o C ) )
36 nnacan 
 |-  ( ( B e. _om /\ A e. _om /\ C e. _om ) -> ( ( B +o A ) = ( B +o C ) <-> A = C ) )
37 2 1 3 36 mp3an 
 |-  ( ( B +o A ) = ( B +o C ) <-> A = C )
38 35 37 sylib 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> A = C )
39 38 28 jca 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) -> ( A = C /\ B = D ) )
40 oveq12 
 |-  ( ( A = C /\ B = D ) -> ( A +o B ) = ( C +o D ) )
41 40 40 oveq12d 
 |-  ( ( A = C /\ B = D ) -> ( ( A +o B ) .o ( A +o B ) ) = ( ( C +o D ) .o ( C +o D ) ) )
42 simpr 
 |-  ( ( A = C /\ B = D ) -> B = D )
43 41 42 oveq12d 
 |-  ( ( A = C /\ B = D ) -> ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) )
44 39 43 impbii 
 |-  ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) )