Metamath Proof Explorer

Theorem oneo

Description: If an ordinal number is even, its successor is odd. (Contributed by NM, 26-Jan-2006)

Ref Expression
Assertion oneo 
|- ( ( A e. On /\ B e. On /\ C = ( 2o .o A ) ) -> -. suc C = ( 2o .o B ) )

Proof

Step Hyp Ref Expression
1 onnbtwn 
 |-  ( A e. On -> -. ( A e. B /\ B e. suc A ) )
2 1 3ad2ant1 
 |-  ( ( A e. On /\ B e. On /\ C = ( 2o .o A ) ) -> -. ( A e. B /\ B e. suc A ) )
3 suceq 
 |-  ( C = ( 2o .o A ) -> suc C = suc ( 2o .o A ) )
4 3 eqeq1d 
 |-  ( C = ( 2o .o A ) -> ( suc C = ( 2o .o B ) <-> suc ( 2o .o A ) = ( 2o .o B ) ) )
5 4 3ad2ant3 
 |-  ( ( A e. On /\ B e. On /\ C = ( 2o .o A ) ) -> ( suc C = ( 2o .o B ) <-> suc ( 2o .o A ) = ( 2o .o B ) ) )
6 ovex 
 |-  ( 2o .o A ) e. _V
7 6 sucid 
 |-  ( 2o .o A ) e. suc ( 2o .o A )
8 eleq2 
 |-  ( suc ( 2o .o A ) = ( 2o .o B ) -> ( ( 2o .o A ) e. suc ( 2o .o A ) <-> ( 2o .o A ) e. ( 2o .o B ) ) )
9 7 8 mpbii 
 |-  ( suc ( 2o .o A ) = ( 2o .o B ) -> ( 2o .o A ) e. ( 2o .o B ) )
10 2on 
 |-  2o e. On
11 omord 
 |-  ( ( A e. On /\ B e. On /\ 2o e. On ) -> ( ( A e. B /\ (/) e. 2o ) <-> ( 2o .o A ) e. ( 2o .o B ) ) )
12 10 11 mp3an3 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A e. B /\ (/) e. 2o ) <-> ( 2o .o A ) e. ( 2o .o B ) ) )
13 simpl 
 |-  ( ( A e. B /\ (/) e. 2o ) -> A e. B )
14 12 13 biimtrrdi 
 |-  ( ( A e. On /\ B e. On ) -> ( ( 2o .o A ) e. ( 2o .o B ) -> A e. B ) )
15 9 14 syl5 
 |-  ( ( A e. On /\ B e. On ) -> ( suc ( 2o .o A ) = ( 2o .o B ) -> A e. B ) )
16 simpr 
 |-  ( ( ( A e. On /\ B e. On ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> suc ( 2o .o A ) = ( 2o .o B ) )
17 omcl 
 |-  ( ( 2o e. On /\ A e. On ) -> ( 2o .o A ) e. On )
18 10 17 mpan 
 |-  ( A e. On -> ( 2o .o A ) e. On )
19 oa1suc 
 |-  ( ( 2o .o A ) e. On -> ( ( 2o .o A ) +o 1o ) = suc ( 2o .o A ) )
20 18 19 syl 
 |-  ( A e. On -> ( ( 2o .o A ) +o 1o ) = suc ( 2o .o A ) )
21 1oex 
 |-  1o e. _V
22 21 sucid 
 |-  1o e. suc 1o
23 df-2o 
 |-  2o = suc 1o
24 22 23 eleqtrri 
 |-  1o e. 2o
25 1on 
 |-  1o e. On
26 oaord 
 |-  ( ( 1o e. On /\ 2o e. On /\ ( 2o .o A ) e. On ) -> ( 1o e. 2o <-> ( ( 2o .o A ) +o 1o ) e. ( ( 2o .o A ) +o 2o ) ) )
27 25 10 18 26 mp3an12i 
 |-  ( A e. On -> ( 1o e. 2o <-> ( ( 2o .o A ) +o 1o ) e. ( ( 2o .o A ) +o 2o ) ) )
28 24 27 mpbii 
 |-  ( A e. On -> ( ( 2o .o A ) +o 1o ) e. ( ( 2o .o A ) +o 2o ) )
29 omsuc 
 |-  ( ( 2o e. On /\ A e. On ) -> ( 2o .o suc A ) = ( ( 2o .o A ) +o 2o ) )
30 10 29 mpan 
 |-  ( A e. On -> ( 2o .o suc A ) = ( ( 2o .o A ) +o 2o ) )
31 28 30 eleqtrrd 
 |-  ( A e. On -> ( ( 2o .o A ) +o 1o ) e. ( 2o .o suc A ) )
32 20 31 eqeltrrd 
 |-  ( A e. On -> suc ( 2o .o A ) e. ( 2o .o suc A ) )
33 32 ad2antrr 
 |-  ( ( ( A e. On /\ B e. On ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> suc ( 2o .o A ) e. ( 2o .o suc A ) )
34 16 33 eqeltrrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> ( 2o .o B ) e. ( 2o .o suc A ) )
35 onsuc 
 |-  ( A e. On -> suc A e. On )
36 omord 
 |-  ( ( B e. On /\ suc A e. On /\ 2o e. On ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
37 10 36 mp3an3 
 |-  ( ( B e. On /\ suc A e. On ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
38 35 37 sylan2 
 |-  ( ( B e. On /\ A e. On ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
39 38 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
40 39 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
41 34 40 mpbird 
 |-  ( ( ( A e. On /\ B e. On ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> ( B e. suc A /\ (/) e. 2o ) )
42 41 simpld 
 |-  ( ( ( A e. On /\ B e. On ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> B e. suc A )
43 42 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( suc ( 2o .o A ) = ( 2o .o B ) -> B e. suc A ) )
44 15 43 jcad 
 |-  ( ( A e. On /\ B e. On ) -> ( suc ( 2o .o A ) = ( 2o .o B ) -> ( A e. B /\ B e. suc A ) ) )
45 44 3adant3 
 |-  ( ( A e. On /\ B e. On /\ C = ( 2o .o A ) ) -> ( suc ( 2o .o A ) = ( 2o .o B ) -> ( A e. B /\ B e. suc A ) ) )
46 5 45 sylbid 
 |-  ( ( A e. On /\ B e. On /\ C = ( 2o .o A ) ) -> ( suc C = ( 2o .o B ) -> ( A e. B /\ B e. suc A ) ) )
47 2 46 mtod 
 |-  ( ( A e. On /\ B e. On /\ C = ( 2o .o A ) ) -> -. suc C = ( 2o .o B ) )