ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnsucelsuc Unicode version

Theorem nnsucelsuc 6252
Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4325, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4346. (Contributed by Jim Kingdon, 25-Aug-2019.)
Assertion
Ref Expression
nnsucelsuc  |-  ( B  e.  om  ->  ( A  e.  B  <->  suc  A  e. 
suc  B ) )

Proof of Theorem nnsucelsuc
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2151 . . . 4  |-  ( x  =  (/)  ->  ( A  e.  x  <->  A  e.  (/) ) )
2 suceq 4229 . . . . 5  |-  ( x  =  (/)  ->  suc  x  =  suc  (/) )
32eleq2d 2157 . . . 4  |-  ( x  =  (/)  ->  ( suc 
A  e.  suc  x  <->  suc 
A  e.  suc  (/) ) )
41, 3imbi12d 232 . . 3  |-  ( x  =  (/)  ->  ( ( A  e.  x  ->  suc  A  e.  suc  x
)  <->  ( A  e.  (/)  ->  suc  A  e.  suc  (/) ) ) )
5 eleq2 2151 . . . 4  |-  ( x  =  y  ->  ( A  e.  x  <->  A  e.  y ) )
6 suceq 4229 . . . . 5  |-  ( x  =  y  ->  suc  x  =  suc  y )
76eleq2d 2157 . . . 4  |-  ( x  =  y  ->  ( suc  A  e.  suc  x  <->  suc 
A  e.  suc  y
) )
85, 7imbi12d 232 . . 3  |-  ( x  =  y  ->  (
( A  e.  x  ->  suc  A  e.  suc  x )  <->  ( A  e.  y  ->  suc  A  e.  suc  y ) ) )
9 eleq2 2151 . . . 4  |-  ( x  =  suc  y  -> 
( A  e.  x  <->  A  e.  suc  y ) )
10 suceq 4229 . . . . 5  |-  ( x  =  suc  y  ->  suc  x  =  suc  suc  y )
1110eleq2d 2157 . . . 4  |-  ( x  =  suc  y  -> 
( suc  A  e.  suc  x  <->  suc  A  e.  suc  suc  y ) )
129, 11imbi12d 232 . . 3  |-  ( x  =  suc  y  -> 
( ( A  e.  x  ->  suc  A  e. 
suc  x )  <->  ( A  e.  suc  y  ->  suc  A  e.  suc  suc  y
) ) )
13 eleq2 2151 . . . 4  |-  ( x  =  B  ->  ( A  e.  x  <->  A  e.  B ) )
14 suceq 4229 . . . . 5  |-  ( x  =  B  ->  suc  x  =  suc  B )
1514eleq2d 2157 . . . 4  |-  ( x  =  B  ->  ( suc  A  e.  suc  x  <->  suc 
A  e.  suc  B
) )
1613, 15imbi12d 232 . . 3  |-  ( x  =  B  ->  (
( A  e.  x  ->  suc  A  e.  suc  x )  <->  ( A  e.  B  ->  suc  A  e.  suc  B ) ) )
17 noel 3290 . . . 4  |-  -.  A  e.  (/)
1817pm2.21i 610 . . 3  |-  ( A  e.  (/)  ->  suc  A  e. 
suc  (/) )
19 elsuci 4230 . . . . . . . 8  |-  ( A  e.  suc  y  -> 
( A  e.  y  \/  A  =  y ) )
2019adantl 271 . . . . . . 7  |-  ( ( ( A  e.  y  ->  suc  A  e.  suc  y )  /\  A  e.  suc  y )  -> 
( A  e.  y  \/  A  =  y ) )
21 simpl 107 . . . . . . . 8  |-  ( ( ( A  e.  y  ->  suc  A  e.  suc  y )  /\  A  e.  suc  y )  -> 
( A  e.  y  ->  suc  A  e.  suc  y ) )
22 suceq 4229 . . . . . . . . 9  |-  ( A  =  y  ->  suc  A  =  suc  y )
2322a1i 9 . . . . . . . 8  |-  ( ( ( A  e.  y  ->  suc  A  e.  suc  y )  /\  A  e.  suc  y )  -> 
( A  =  y  ->  suc  A  =  suc  y ) )
2421, 23orim12d 735 . . . . . . 7  |-  ( ( ( A  e.  y  ->  suc  A  e.  suc  y )  /\  A  e.  suc  y )  -> 
( ( A  e.  y  \/  A  =  y )  ->  ( suc  A  e.  suc  y  \/  suc  A  =  suc  y ) ) )
2520, 24mpd 13 . . . . . 6  |-  ( ( ( A  e.  y  ->  suc  A  e.  suc  y )  /\  A  e.  suc  y )  -> 
( suc  A  e.  suc  y  \/  suc  A  =  suc  y ) )
26 vex 2622 . . . . . . . 8  |-  y  e. 
_V
2726sucex 4316 . . . . . . 7  |-  suc  y  e.  _V
2827elsuc2 4234 . . . . . 6  |-  ( suc 
A  e.  suc  suc  y 
<->  ( suc  A  e. 
suc  y  \/  suc  A  =  suc  y ) )
2925, 28sylibr 132 . . . . 5  |-  ( ( ( A  e.  y  ->  suc  A  e.  suc  y )  /\  A  e.  suc  y )  ->  suc  A  e.  suc  suc  y )
3029ex 113 . . . 4  |-  ( ( A  e.  y  ->  suc  A  e.  suc  y
)  ->  ( A  e.  suc  y  ->  suc  A  e.  suc  suc  y
) )
3130a1i 9 . . 3  |-  ( y  e.  om  ->  (
( A  e.  y  ->  suc  A  e.  suc  y )  ->  ( A  e.  suc  y  ->  suc  A  e.  suc  suc  y ) ) )
324, 8, 12, 16, 18, 31finds 4415 . 2  |-  ( B  e.  om  ->  ( A  e.  B  ->  suc 
A  e.  suc  B
) )
33 nnon 4424 . . 3  |-  ( B  e.  om  ->  B  e.  On )
34 onsucelsucr 4325 . . 3  |-  ( B  e.  On  ->  ( suc  A  e.  suc  B  ->  A  e.  B ) )
3533, 34syl 14 . 2  |-  ( B  e.  om  ->  ( suc  A  e.  suc  B  ->  A  e.  B ) )
3632, 35impbid 127 1  |-  ( B  e.  om  ->  ( A  e.  B  <->  suc  A  e. 
suc  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 664    = wceq 1289    e. wcel 1438   (/)c0 3286   Oncon0 4190   suc csuc 4192   omcom 4405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-nul 3965  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-iinf 4403
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-pw 3431  df-sn 3452  df-pr 3453  df-uni 3654  df-int 3689  df-tr 3937  df-iord 4193  df-on 4195  df-suc 4198  df-iom 4406
This theorem is referenced by:  nnsucsssuc  6253  nntri3or  6254  nnsucuniel  6256  nnaordi  6265
  Copyright terms: Public domain W3C validator