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

Theorem nnsucsssuc 6493
Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucsssucr 4509, but the forward direction, for all ordinals, implies excluded middle as seen as onsucsssucexmid 4527. (Contributed by Jim Kingdon, 25-Aug-2019.)
Assertion
Ref Expression
nnsucsssuc  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  C_  B  <->  suc 
A  C_  suc  B ) )

Proof of Theorem nnsucsssuc
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3179 . . . . . 6  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
2 suceq 4403 . . . . . . 7  |-  ( x  =  A  ->  suc  x  =  suc  A )
32sseq1d 3185 . . . . . 6  |-  ( x  =  A  ->  ( suc  x  C_  suc  B  <->  suc  A  C_  suc  B ) )
41, 3imbi12d 234 . . . . 5  |-  ( x  =  A  ->  (
( x  C_  B  ->  suc  x  C_  suc  B )  <->  ( A  C_  B  ->  suc  A  C_  suc  B ) ) )
54imbi2d 230 . . . 4  |-  ( x  =  A  ->  (
( B  e.  om  ->  ( x  C_  B  ->  suc  x  C_  suc  B ) )  <->  ( B  e.  om  ->  ( A  C_  B  ->  suc  A  C_  suc  B ) ) ) )
6 sseq1 3179 . . . . . 6  |-  ( x  =  (/)  ->  ( x 
C_  B  <->  (/)  C_  B
) )
7 suceq 4403 . . . . . . 7  |-  ( x  =  (/)  ->  suc  x  =  suc  (/) )
87sseq1d 3185 . . . . . 6  |-  ( x  =  (/)  ->  ( suc  x  C_  suc  B  <->  suc  (/)  C_  suc  B ) )
96, 8imbi12d 234 . . . . 5  |-  ( x  =  (/)  ->  ( ( x  C_  B  ->  suc  x  C_  suc  B )  <-> 
( (/)  C_  B  ->  suc  (/)  C_  suc  B ) ) )
10 sseq1 3179 . . . . . 6  |-  ( x  =  y  ->  (
x  C_  B  <->  y  C_  B ) )
11 suceq 4403 . . . . . . 7  |-  ( x  =  y  ->  suc  x  =  suc  y )
1211sseq1d 3185 . . . . . 6  |-  ( x  =  y  ->  ( suc  x  C_  suc  B  <->  suc  y  C_  suc  B ) )
1310, 12imbi12d 234 . . . . 5  |-  ( x  =  y  ->  (
( x  C_  B  ->  suc  x  C_  suc  B )  <->  ( y  C_  B  ->  suc  y  C_  suc  B ) ) )
14 sseq1 3179 . . . . . 6  |-  ( x  =  suc  y  -> 
( x  C_  B  <->  suc  y  C_  B )
)
15 suceq 4403 . . . . . . 7  |-  ( x  =  suc  y  ->  suc  x  =  suc  suc  y )
1615sseq1d 3185 . . . . . 6  |-  ( x  =  suc  y  -> 
( suc  x  C_  suc  B  <->  suc  suc  y  C_  suc  B ) )
1714, 16imbi12d 234 . . . . 5  |-  ( x  =  suc  y  -> 
( ( x  C_  B  ->  suc  x  C_  suc  B )  <->  ( suc  y  C_  B  ->  suc  suc  y  C_ 
suc  B ) ) )
18 peano3 4596 . . . . . . . . 9  |-  ( B  e.  om  ->  suc  B  =/=  (/) )
1918neneqd 2368 . . . . . . . 8  |-  ( B  e.  om  ->  -.  suc  B  =  (/) )
20 peano2 4595 . . . . . . . . . 10  |-  ( B  e.  om  ->  suc  B  e.  om )
21 0elnn 4619 . . . . . . . . . 10  |-  ( suc 
B  e.  om  ->  ( suc  B  =  (/)  \/  (/)  e.  suc  B ) )
2220, 21syl 14 . . . . . . . . 9  |-  ( B  e.  om  ->  ( suc  B  =  (/)  \/  (/)  e.  suc  B ) )
2322ord 724 . . . . . . . 8  |-  ( B  e.  om  ->  ( -.  suc  B  =  (/)  -> 
(/)  e.  suc  B ) )
2419, 23mpd 13 . . . . . . 7  |-  ( B  e.  om  ->  (/)  e.  suc  B )
25 nnord 4612 . . . . . . . 8  |-  ( B  e.  om  ->  Ord  B )
26 ordsucim 4500 . . . . . . . 8  |-  ( Ord 
B  ->  Ord  suc  B
)
27 0ex 4131 . . . . . . . . 9  |-  (/)  e.  _V
28 ordelsuc 4505 . . . . . . . . 9  |-  ( (
(/)  e.  _V  /\  Ord  suc 
B )  ->  ( (/) 
e.  suc  B  <->  suc  (/)  C_  suc  B ) )
2927, 28mpan 424 . . . . . . . 8  |-  ( Ord 
suc  B  ->  ( (/)  e.  suc  B  <->  suc  (/)  C_  suc  B ) )
3025, 26, 293syl 17 . . . . . . 7  |-  ( B  e.  om  ->  ( (/) 
e.  suc  B  <->  suc  (/)  C_  suc  B ) )
3124, 30mpbid 147 . . . . . 6  |-  ( B  e.  om  ->  suc  (/)  C_  suc  B )
3231a1d 22 . . . . 5  |-  ( B  e.  om  ->  ( (/)  C_  B  ->  suc  (/)  C_  suc  B ) )
33 simp3 999 . . . . . . . . . 10  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  suc  y  C_  B )
34 simp1l 1021 . . . . . . . . . . 11  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  y  e.  om )
35 simp1r 1022 . . . . . . . . . . . 12  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  B  e.  om )
3635, 25syl 14 . . . . . . . . . . 11  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  Ord  B )
37 ordelsuc 4505 . . . . . . . . . . 11  |-  ( ( y  e.  om  /\  Ord  B )  ->  (
y  e.  B  <->  suc  y  C_  B ) )
3834, 36, 37syl2anc 411 . . . . . . . . . 10  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  (
y  e.  B  <->  suc  y  C_  B ) )
3933, 38mpbird 167 . . . . . . . . 9  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  y  e.  B )
40 nnsucelsuc 6492 . . . . . . . . . 10  |-  ( B  e.  om  ->  (
y  e.  B  <->  suc  y  e. 
suc  B ) )
4135, 40syl 14 . . . . . . . . 9  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  (
y  e.  B  <->  suc  y  e. 
suc  B ) )
4239, 41mpbid 147 . . . . . . . 8  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  suc  y  e.  suc  B )
43 peano2 4595 . . . . . . . . . 10  |-  ( y  e.  om  ->  suc  y  e.  om )
4434, 43syl 14 . . . . . . . . 9  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  suc  y  e.  om )
4536, 26syl 14 . . . . . . . . 9  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  Ord  suc 
B )
46 ordelsuc 4505 . . . . . . . . 9  |-  ( ( suc  y  e.  om  /\ 
Ord  suc  B )  -> 
( suc  y  e.  suc  B  <->  suc  suc  y  C_  suc  B ) )
4744, 45, 46syl2anc 411 . . . . . . . 8  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  ( suc  y  e.  suc  B  <->  suc  suc  y  C_  suc  B ) )
4842, 47mpbid 147 . . . . . . 7  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B )  /\  suc  y  C_  B )  ->  suc  suc  y  C_  suc  B )
49483expia 1205 . . . . . 6  |-  ( ( ( y  e.  om  /\  B  e.  om )  /\  ( y  C_  B  ->  suc  y  C_  suc  B ) )  ->  ( suc  y  C_  B  ->  suc  suc  y  C_  suc  B ) )
5049exp31 364 . . . . 5  |-  ( y  e.  om  ->  ( B  e.  om  ->  ( ( y  C_  B  ->  suc  y  C_  suc  B )  ->  ( suc  y  C_  B  ->  suc  suc  y  C_  suc  B ) ) ) )
519, 13, 17, 32, 50finds2 4601 . . . 4  |-  ( x  e.  om  ->  ( B  e.  om  ->  ( x  C_  B  ->  suc  x  C_  suc  B ) ) )
525, 51vtoclga 2804 . . 3  |-  ( A  e.  om  ->  ( B  e.  om  ->  ( A  C_  B  ->  suc 
A  C_  suc  B ) ) )
5352imp 124 . 2  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  C_  B  ->  suc  A  C_  suc  B ) )
54 nnon 4610 . . 3  |-  ( A  e.  om  ->  A  e.  On )
55 onsucsssucr 4509 . . 3  |-  ( ( A  e.  On  /\  Ord  B )  ->  ( suc  A  C_  suc  B  ->  A  C_  B ) )
5654, 25, 55syl2an 289 . 2  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( suc  A  C_  suc  B  ->  A  C_  B
) )
5753, 56impbid 129 1  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  C_  B  <->  suc 
A  C_  suc  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 708    /\ w3a 978    = wceq 1353    e. wcel 2148   _Vcvv 2738    C_ wss 3130   (/)c0 3423   Ord word 4363   Oncon0 4364   suc csuc 4366   omcom 4590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-iinf 4588
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-v 2740  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-uni 3811  df-int 3846  df-tr 4103  df-iord 4367  df-on 4369  df-suc 4372  df-iom 4591
This theorem is referenced by:  nnaword  6512  ennnfonelemk  12401  ennnfonelemkh  12413
  Copyright terms: Public domain W3C validator