Metamath Proof Explorer

Theorem nnaordex2

Description: Equivalence for ordering. (Contributed by Scott Fenton, 18-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 nnaordex 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> E. y e. _om ( (/) e. y /\ ( A +o y ) = B ) ) )
2 nn0suc 
 |-  ( y e. _om -> ( y = (/) \/ E. x e. _om y = suc x ) )
3 2 ad2antrl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( y e. _om /\ ( (/) e. y /\ ( A +o y ) = B ) ) ) -> ( y = (/) \/ E. x e. _om y = suc x ) )
4 simprrl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( y e. _om /\ ( (/) e. y /\ ( A +o y ) = B ) ) ) -> (/) e. y )
5 n0i 
 |-  ( (/) e. y -> -. y = (/) )
6 4 5 syl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( y e. _om /\ ( (/) e. y /\ ( A +o y ) = B ) ) ) -> -. y = (/) )
7 3 6 orcnd 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( y e. _om /\ ( (/) e. y /\ ( A +o y ) = B ) ) ) -> E. x e. _om y = suc x )
8 simprrr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( y e. _om /\ ( (/) e. y /\ ( A +o y ) = B ) ) ) -> ( A +o y ) = B )
9 oveq2 
 |-  ( y = suc x -> ( A +o y ) = ( A +o suc x ) )
10 9 eqeq1d 
 |-  ( y = suc x -> ( ( A +o y ) = B <-> ( A +o suc x ) = B ) )
11 8 10 syl5ibcom 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( y e. _om /\ ( (/) e. y /\ ( A +o y ) = B ) ) ) -> ( y = suc x -> ( A +o suc x ) = B ) )
12 11 reximdv 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( y e. _om /\ ( (/) e. y /\ ( A +o y ) = B ) ) ) -> ( E. x e. _om y = suc x -> E. x e. _om ( A +o suc x ) = B ) )
13 7 12 mpd 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( y e. _om /\ ( (/) e. y /\ ( A +o y ) = B ) ) ) -> E. x e. _om ( A +o suc x ) = B )
14 13 rexlimdvaa 
 |-  ( ( A e. _om /\ B e. _om ) -> ( E. y e. _om ( (/) e. y /\ ( A +o y ) = B ) -> E. x e. _om ( A +o suc x ) = B ) )
15 peano2 
 |-  ( x e. _om -> suc x e. _om )
16 15 ad2antrl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( x e. _om /\ ( A +o suc x ) = B ) ) -> suc x e. _om )
17 nnord 
 |-  ( x e. _om -> Ord x )
18 17 ad2antrl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( x e. _om /\ ( A +o suc x ) = B ) ) -> Ord x )
19 0elsuc 
 |-  ( Ord x -> (/) e. suc x )
20 18 19 syl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( x e. _om /\ ( A +o suc x ) = B ) ) -> (/) e. suc x )
21 simprr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( x e. _om /\ ( A +o suc x ) = B ) ) -> ( A +o suc x ) = B )
22 eleq2 
 |-  ( y = suc x -> ( (/) e. y <-> (/) e. suc x ) )
23 22 10 anbi12d 
 |-  ( y = suc x -> ( ( (/) e. y /\ ( A +o y ) = B ) <-> ( (/) e. suc x /\ ( A +o suc x ) = B ) ) )
24 23 rspcev 
 |-  ( ( suc x e. _om /\ ( (/) e. suc x /\ ( A +o suc x ) = B ) ) -> E. y e. _om ( (/) e. y /\ ( A +o y ) = B ) )
25 16 20 21 24 syl12anc 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( x e. _om /\ ( A +o suc x ) = B ) ) -> E. y e. _om ( (/) e. y /\ ( A +o y ) = B ) )
26 25 rexlimdvaa 
 |-  ( ( A e. _om /\ B e. _om ) -> ( E. x e. _om ( A +o suc x ) = B -> E. y e. _om ( (/) e. y /\ ( A +o y ) = B ) ) )
27 14 26 impbid 
 |-  ( ( A e. _om /\ B e. _om ) -> ( E. y e. _om ( (/) e. y /\ ( A +o y ) = B ) <-> E. x e. _om ( A +o suc x ) = B ) )
28 1 27 bitrd 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> E. x e. _om ( A +o suc x ) = B ) )