Metamath Proof Explorer

Theorem nnawordex

Description: Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002) (Revised by Mario Carneiro, 15-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( y = B -> ( A +o y ) = ( A +o B ) )
2 1 sseq2d 
 |-  ( y = B -> ( B C_ ( A +o y ) <-> B C_ ( A +o B ) ) )
3 simplr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> B e. _om )
4 nnon 
 |-  ( B e. _om -> B e. On )
5 3 4 syl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> B e. On )
6 simpll 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> A e. _om )
7 nnaword2 
 |-  ( ( B e. _om /\ A e. _om ) -> B C_ ( A +o B ) )
8 3 6 7 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> B C_ ( A +o B ) )
9 2 5 8 elrabd 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> B e. { y e. On | B C_ ( A +o y ) } )
10 intss1 
 |-  ( B e. { y e. On | B C_ ( A +o y ) } -> |^| { y e. On | B C_ ( A +o y ) } C_ B )
11 9 10 syl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> |^| { y e. On | B C_ ( A +o y ) } C_ B )
12 ssrab2 
 |-  { y e. On | B C_ ( A +o y ) } C_ On
13 9 ne0d 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> { y e. On | B C_ ( A +o y ) } =/= (/) )
14 oninton 
 |-  ( ( { y e. On | B C_ ( A +o y ) } C_ On /\ { y e. On | B C_ ( A +o y ) } =/= (/) ) -> |^| { y e. On | B C_ ( A +o y ) } e. On )
15 12 13 14 sylancr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> |^| { y e. On | B C_ ( A +o y ) } e. On )
16 eloni 
 |-  ( |^| { y e. On | B C_ ( A +o y ) } e. On -> Ord |^| { y e. On | B C_ ( A +o y ) } )
17 15 16 syl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> Ord |^| { y e. On | B C_ ( A +o y ) } )
18 ordom 
 |-  Ord _om
19 ordtr2 
 |-  ( ( Ord |^| { y e. On | B C_ ( A +o y ) } /\ Ord _om ) -> ( ( |^| { y e. On | B C_ ( A +o y ) } C_ B /\ B e. _om ) -> |^| { y e. On | B C_ ( A +o y ) } e. _om ) )
20 17 18 19 sylancl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> ( ( |^| { y e. On | B C_ ( A +o y ) } C_ B /\ B e. _om ) -> |^| { y e. On | B C_ ( A +o y ) } e. _om ) )
21 11 3 20 mp2and 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> |^| { y e. On | B C_ ( A +o y ) } e. _om )
22 nna0 
 |-  ( A e. _om -> ( A +o (/) ) = A )
23 22 ad2antrr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> ( A +o (/) ) = A )
24 simpr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> A C_ B )
25 23 24 eqsstrd 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> ( A +o (/) ) C_ B )
26 oveq2 
 |-  ( |^| { y e. On | B C_ ( A +o y ) } = (/) -> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) = ( A +o (/) ) )
27 26 sseq1d 
 |-  ( |^| { y e. On | B C_ ( A +o y ) } = (/) -> ( ( A +o |^| { y e. On | B C_ ( A +o y ) } ) C_ B <-> ( A +o (/) ) C_ B ) )
28 25 27 syl5ibrcom 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> ( |^| { y e. On | B C_ ( A +o y ) } = (/) -> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) C_ B ) )
29 simprr 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> |^| { y e. On | B C_ ( A +o y ) } = suc x )
30 29 oveq2d 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) = ( A +o suc x ) )
31 6 adantr 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> A e. _om )
32 simprl 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> x e. _om )
33 nnasuc 
 |-  ( ( A e. _om /\ x e. _om ) -> ( A +o suc x ) = suc ( A +o x ) )
34 31 32 33 syl2anc 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> ( A +o suc x ) = suc ( A +o x ) )
35 30 34 eqtrd 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) = suc ( A +o x ) )
36 nnord 
 |-  ( B e. _om -> Ord B )
37 3 36 syl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> Ord B )
38 37 adantr 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> Ord B )
39 nnon 
 |-  ( x e. _om -> x e. On )
40 39 adantr 
 |-  ( ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) -> x e. On )
41 vex 
 |-  x e. _V
42 41 sucid 
 |-  x e. suc x
43 simpr 
 |-  ( ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) -> |^| { y e. On | B C_ ( A +o y ) } = suc x )
44 42 43 eleqtrrid 
 |-  ( ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) -> x e. |^| { y e. On | B C_ ( A +o y ) } )
45 oveq2 
 |-  ( y = x -> ( A +o y ) = ( A +o x ) )
46 45 sseq2d 
 |-  ( y = x -> ( B C_ ( A +o y ) <-> B C_ ( A +o x ) ) )
47 46 onnminsb 
 |-  ( x e. On -> ( x e. |^| { y e. On | B C_ ( A +o y ) } -> -. B C_ ( A +o x ) ) )
48 40 44 47 sylc 
 |-  ( ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) -> -. B C_ ( A +o x ) )
49 48 adantl 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> -. B C_ ( A +o x ) )
50 nnacl 
 |-  ( ( A e. _om /\ x e. _om ) -> ( A +o x ) e. _om )
51 31 32 50 syl2anc 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> ( A +o x ) e. _om )
52 nnord 
 |-  ( ( A +o x ) e. _om -> Ord ( A +o x ) )
53 51 52 syl 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> Ord ( A +o x ) )
54 ordtri1 
 |-  ( ( Ord B /\ Ord ( A +o x ) ) -> ( B C_ ( A +o x ) <-> -. ( A +o x ) e. B ) )
55 38 53 54 syl2anc 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> ( B C_ ( A +o x ) <-> -. ( A +o x ) e. B ) )
56 55 con2bid 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> ( ( A +o x ) e. B <-> -. B C_ ( A +o x ) ) )
57 49 56 mpbird 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> ( A +o x ) e. B )
58 ordsucss 
 |-  ( Ord B -> ( ( A +o x ) e. B -> suc ( A +o x ) C_ B ) )
59 38 57 58 sylc 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> suc ( A +o x ) C_ B )
60 35 59 eqsstrd 
 |-  ( ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) /\ ( x e. _om /\ |^| { y e. On | B C_ ( A +o y ) } = suc x ) ) -> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) C_ B )
61 60 rexlimdvaa 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> ( E. x e. _om |^| { y e. On | B C_ ( A +o y ) } = suc x -> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) C_ B ) )
62 nn0suc 
 |-  ( |^| { y e. On | B C_ ( A +o y ) } e. _om -> ( |^| { y e. On | B C_ ( A +o y ) } = (/) \/ E. x e. _om |^| { y e. On | B C_ ( A +o y ) } = suc x ) )
63 21 62 syl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> ( |^| { y e. On | B C_ ( A +o y ) } = (/) \/ E. x e. _om |^| { y e. On | B C_ ( A +o y ) } = suc x ) )
64 28 61 63 mpjaod 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) C_ B )
65 onint 
 |-  ( ( { y e. On | B C_ ( A +o y ) } C_ On /\ { y e. On | B C_ ( A +o y ) } =/= (/) ) -> |^| { y e. On | B C_ ( A +o y ) } e. { y e. On | B C_ ( A +o y ) } )
66 12 13 65 sylancr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> |^| { y e. On | B C_ ( A +o y ) } e. { y e. On | B C_ ( A +o y ) } )
67 nfrab1 
 |-  F/_ y { y e. On | B C_ ( A +o y ) }
68 67 nfint 
 |-  F/_ y |^| { y e. On | B C_ ( A +o y ) }
69 nfcv 
 |-  F/_ y On
70 nfcv 
 |-  F/_ y B
71 nfcv 
 |-  F/_ y A
72 nfcv 
 |-  F/_ y +o
73 71 72 68 nfov 
 |-  F/_ y ( A +o |^| { y e. On | B C_ ( A +o y ) } )
74 70 73 nfss 
 |-  F/ y B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } )
75 oveq2 
 |-  ( y = |^| { y e. On | B C_ ( A +o y ) } -> ( A +o y ) = ( A +o |^| { y e. On | B C_ ( A +o y ) } ) )
76 75 sseq2d 
 |-  ( y = |^| { y e. On | B C_ ( A +o y ) } -> ( B C_ ( A +o y ) <-> B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } ) ) )
77 68 69 74 76 elrabf 
 |-  ( |^| { y e. On | B C_ ( A +o y ) } e. { y e. On | B C_ ( A +o y ) } <-> ( |^| { y e. On | B C_ ( A +o y ) } e. On /\ B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } ) ) )
78 77 simprbi 
 |-  ( |^| { y e. On | B C_ ( A +o y ) } e. { y e. On | B C_ ( A +o y ) } -> B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } ) )
79 66 78 syl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> B C_ ( A +o |^| { y e. On | B C_ ( A +o y ) } ) )
80 64 79 eqssd 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) = B )
81 oveq2 
 |-  ( x = |^| { y e. On | B C_ ( A +o y ) } -> ( A +o x ) = ( A +o |^| { y e. On | B C_ ( A +o y ) } ) )
82 81 eqeq1d 
 |-  ( x = |^| { y e. On | B C_ ( A +o y ) } -> ( ( A +o x ) = B <-> ( A +o |^| { y e. On | B C_ ( A +o y ) } ) = B ) )
83 82 rspcev 
 |-  ( ( |^| { y e. On | B C_ ( A +o y ) } e. _om /\ ( A +o |^| { y e. On | B C_ ( A +o y ) } ) = B ) -> E. x e. _om ( A +o x ) = B )
84 21 80 83 syl2anc 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ A C_ B ) -> E. x e. _om ( A +o x ) = B )
85 84 ex 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A C_ B -> E. x e. _om ( A +o x ) = B ) )
86 nnaword1 
 |-  ( ( A e. _om /\ x e. _om ) -> A C_ ( A +o x ) )
87 86 adantlr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ x e. _om ) -> A C_ ( A +o x ) )
88 sseq2 
 |-  ( ( A +o x ) = B -> ( A C_ ( A +o x ) <-> A C_ B ) )
89 87 88 syl5ibcom 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ x e. _om ) -> ( ( A +o x ) = B -> A C_ B ) )
90 89 rexlimdva 
 |-  ( ( A e. _om /\ B e. _om ) -> ( E. x e. _om ( A +o x ) = B -> A C_ B ) )
91 85 90 impbid 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A C_ B <-> E. x e. _om ( A +o x ) = B ) )