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

Metamath Proof Explorer

Theorem nnaordex

Description: Equivalence for ordering. Compare Exercise 23 of Enderton p. 88. (Contributed by NM, 5-Dec-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnaordex 
|- ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( B e. _om -> B e. On )
2 1 adantl 
 |-  ( ( A e. _om /\ B e. _om ) -> B e. On )
3 onelss 
 |-  ( B e. On -> ( A e. B -> A C_ B ) )
4 2 3 syl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B -> A C_ B ) )
5 nnawordex 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A C_ B <-> E. x e. _om ( A +o x ) = B ) )
6 4 5 sylibd 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B -> E. x e. _om ( A +o x ) = B ) )
7 simplr 
 |-  ( ( ( A e. _om /\ A e. B ) /\ x e. _om ) -> A e. B )
8 eleq2 
 |-  ( ( A +o x ) = B -> ( A e. ( A +o x ) <-> A e. B ) )
9 7 8 syl5ibrcom 
 |-  ( ( ( A e. _om /\ A e. B ) /\ x e. _om ) -> ( ( A +o x ) = B -> A e. ( A +o x ) ) )
10 peano1 
 |-  (/) e. _om
11 nnaord 
 |-  ( ( (/) e. _om /\ x e. _om /\ A e. _om ) -> ( (/) e. x <-> ( A +o (/) ) e. ( A +o x ) ) )
12 10 11 mp3an1 
 |-  ( ( x e. _om /\ A e. _om ) -> ( (/) e. x <-> ( A +o (/) ) e. ( A +o x ) ) )
13 12 ancoms 
 |-  ( ( A e. _om /\ x e. _om ) -> ( (/) e. x <-> ( A +o (/) ) e. ( A +o x ) ) )
14 nna0 
 |-  ( A e. _om -> ( A +o (/) ) = A )
15 14 adantr 
 |-  ( ( A e. _om /\ x e. _om ) -> ( A +o (/) ) = A )
16 15 eleq1d 
 |-  ( ( A e. _om /\ x e. _om ) -> ( ( A +o (/) ) e. ( A +o x ) <-> A e. ( A +o x ) ) )
17 13 16 bitrd 
 |-  ( ( A e. _om /\ x e. _om ) -> ( (/) e. x <-> A e. ( A +o x ) ) )
18 17 adantlr 
 |-  ( ( ( A e. _om /\ A e. B ) /\ x e. _om ) -> ( (/) e. x <-> A e. ( A +o x ) ) )
19 9 18 sylibrd 
 |-  ( ( ( A e. _om /\ A e. B ) /\ x e. _om ) -> ( ( A +o x ) = B -> (/) e. x ) )
20 19 ancrd 
 |-  ( ( ( A e. _om /\ A e. B ) /\ x e. _om ) -> ( ( A +o x ) = B -> ( (/) e. x /\ ( A +o x ) = B ) ) )
21 20 reximdva 
 |-  ( ( A e. _om /\ A e. B ) -> ( E. x e. _om ( A +o x ) = B -> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) )
22 21 ex 
 |-  ( A e. _om -> ( A e. B -> ( E. x e. _om ( A +o x ) = B -> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) ) )
23 22 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B -> ( E. x e. _om ( A +o x ) = B -> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) ) )
24 6 23 mpdd 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B -> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) )
25 17 biimpa 
 |-  ( ( ( A e. _om /\ x e. _om ) /\ (/) e. x ) -> A e. ( A +o x ) )
26 25 8 syl5ibcom 
 |-  ( ( ( A e. _om /\ x e. _om ) /\ (/) e. x ) -> ( ( A +o x ) = B -> A e. B ) )
27 26 expimpd 
 |-  ( ( A e. _om /\ x e. _om ) -> ( ( (/) e. x /\ ( A +o x ) = B ) -> A e. B ) )
28 27 rexlimdva 
 |-  ( A e. _om -> ( E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) -> A e. B ) )
29 28 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) -> A e. B ) )
30 24 29 impbid 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> E. x e. _om ( (/) e. x /\ ( A +o x ) = B ) ) )