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

Theorem nntri3or 6472
Description: Trichotomy for natural numbers. (Contributed by Jim Kingdon, 25-Aug-2019.)
Assertion
Ref Expression
nntri3or  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A
) )

Proof of Theorem nntri3or
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2234 . . . . 5  |-  ( x  =  B  ->  ( A  e.  x  <->  A  e.  B ) )
2 eqeq2 2180 . . . . 5  |-  ( x  =  B  ->  ( A  =  x  <->  A  =  B ) )
3 eleq1 2233 . . . . 5  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
41, 2, 33orbi123d 1306 . . . 4  |-  ( x  =  B  ->  (
( A  e.  x  \/  A  =  x  \/  x  e.  A
)  <->  ( A  e.  B  \/  A  =  B  \/  B  e.  A ) ) )
54imbi2d 229 . . 3  |-  ( x  =  B  ->  (
( A  e.  om  ->  ( A  e.  x  \/  A  =  x  \/  x  e.  A
) )  <->  ( A  e.  om  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A ) ) ) )
6 eleq2 2234 . . . . 5  |-  ( x  =  (/)  ->  ( A  e.  x  <->  A  e.  (/) ) )
7 eqeq2 2180 . . . . 5  |-  ( x  =  (/)  ->  ( A  =  x  <->  A  =  (/) ) )
8 eleq1 2233 . . . . 5  |-  ( x  =  (/)  ->  ( x  e.  A  <->  (/)  e.  A
) )
96, 7, 83orbi123d 1306 . . . 4  |-  ( x  =  (/)  ->  ( ( A  e.  x  \/  A  =  x  \/  x  e.  A )  <-> 
( A  e.  (/)  \/  A  =  (/)  \/  (/)  e.  A
) ) )
10 eleq2 2234 . . . . 5  |-  ( x  =  y  ->  ( A  e.  x  <->  A  e.  y ) )
11 eqeq2 2180 . . . . 5  |-  ( x  =  y  ->  ( A  =  x  <->  A  =  y ) )
12 eleq1 2233 . . . . 5  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
1310, 11, 123orbi123d 1306 . . . 4  |-  ( x  =  y  ->  (
( A  e.  x  \/  A  =  x  \/  x  e.  A
)  <->  ( A  e.  y  \/  A  =  y  \/  y  e.  A ) ) )
14 eleq2 2234 . . . . 5  |-  ( x  =  suc  y  -> 
( A  e.  x  <->  A  e.  suc  y ) )
15 eqeq2 2180 . . . . 5  |-  ( x  =  suc  y  -> 
( A  =  x  <-> 
A  =  suc  y
) )
16 eleq1 2233 . . . . 5  |-  ( x  =  suc  y  -> 
( x  e.  A  <->  suc  y  e.  A ) )
1714, 15, 163orbi123d 1306 . . . 4  |-  ( x  =  suc  y  -> 
( ( A  e.  x  \/  A  =  x  \/  x  e.  A )  <->  ( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )
) )
18 0elnn 4603 . . . . 5  |-  ( A  e.  om  ->  ( A  =  (/)  \/  (/)  e.  A
) )
19 olc 706 . . . . . 6  |-  ( ( A  =  (/)  \/  (/)  e.  A
)  ->  ( A  e.  (/)  \/  ( A  =  (/)  \/  (/)  e.  A
) ) )
20 3orass 976 . . . . . 6  |-  ( ( A  e.  (/)  \/  A  =  (/)  \/  (/)  e.  A
)  <->  ( A  e.  (/)  \/  ( A  =  (/)  \/  (/)  e.  A ) ) )
2119, 20sylibr 133 . . . . 5  |-  ( ( A  =  (/)  \/  (/)  e.  A
)  ->  ( A  e.  (/)  \/  A  =  (/)  \/  (/)  e.  A ) )
2218, 21syl 14 . . . 4  |-  ( A  e.  om  ->  ( A  e.  (/)  \/  A  =  (/)  \/  (/)  e.  A
) )
23 df-3or 974 . . . . . 6  |-  ( ( A  e.  y  \/  A  =  y  \/  y  e.  A )  <-> 
( ( A  e.  y  \/  A  =  y )  \/  y  e.  A ) )
24 elex 2741 . . . . . . . 8  |-  ( y  e.  om  ->  y  e.  _V )
25 elsuc2g 4390 . . . . . . . . 9  |-  ( y  e.  _V  ->  ( A  e.  suc  y  <->  ( A  e.  y  \/  A  =  y ) ) )
26 3mix1 1161 . . . . . . . . 9  |-  ( A  e.  suc  y  -> 
( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )
)
2725, 26syl6bir 163 . . . . . . . 8  |-  ( y  e.  _V  ->  (
( A  e.  y  \/  A  =  y )  ->  ( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )
) )
2824, 27syl 14 . . . . . . 7  |-  ( y  e.  om  ->  (
( A  e.  y  \/  A  =  y )  ->  ( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )
) )
29 nnsucelsuc 6470 . . . . . . . . 9  |-  ( A  e.  om  ->  (
y  e.  A  <->  suc  y  e. 
suc  A ) )
30 elsuci 4388 . . . . . . . . 9  |-  ( suc  y  e.  suc  A  ->  ( suc  y  e.  A  \/  suc  y  =  A ) )
3129, 30syl6bi 162 . . . . . . . 8  |-  ( A  e.  om  ->  (
y  e.  A  -> 
( suc  y  e.  A  \/  suc  y  =  A ) ) )
32 eqcom 2172 . . . . . . . . . . . . 13  |-  ( suc  y  =  A  <->  A  =  suc  y )
3332orbi2i 757 . . . . . . . . . . . 12  |-  ( ( suc  y  e.  A  \/  suc  y  =  A )  <->  ( suc  y  e.  A  \/  A  =  suc  y ) )
3433biimpi 119 . . . . . . . . . . 11  |-  ( ( suc  y  e.  A  \/  suc  y  =  A )  ->  ( suc  y  e.  A  \/  A  =  suc  y ) )
3534orcomd 724 . . . . . . . . . 10  |-  ( ( suc  y  e.  A  \/  suc  y  =  A )  ->  ( A  =  suc  y  \/  suc  y  e.  A )
)
3635olcd 729 . . . . . . . . 9  |-  ( ( suc  y  e.  A  \/  suc  y  =  A )  ->  ( A  e.  suc  y  \/  ( A  =  suc  y  \/ 
suc  y  e.  A
) ) )
37 3orass 976 . . . . . . . . 9  |-  ( ( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )  <->  ( A  e.  suc  y  \/  ( A  =  suc  y  \/ 
suc  y  e.  A
) ) )
3836, 37sylibr 133 . . . . . . . 8  |-  ( ( suc  y  e.  A  \/  suc  y  =  A )  ->  ( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )
)
3931, 38syl6 33 . . . . . . 7  |-  ( A  e.  om  ->  (
y  e.  A  -> 
( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )
) )
4028, 39jaao 714 . . . . . 6  |-  ( ( y  e.  om  /\  A  e.  om )  ->  ( ( ( A  e.  y  \/  A  =  y )  \/  y  e.  A )  ->  ( A  e. 
suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )
) )
4123, 40syl5bi 151 . . . . 5  |-  ( ( y  e.  om  /\  A  e.  om )  ->  ( ( A  e.  y  \/  A  =  y  \/  y  e.  A )  ->  ( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A
) ) )
4241ex 114 . . . 4  |-  ( y  e.  om  ->  ( A  e.  om  ->  ( ( A  e.  y  \/  A  =  y  \/  y  e.  A
)  ->  ( A  e.  suc  y  \/  A  =  suc  y  \/  suc  y  e.  A )
) ) )
439, 13, 17, 22, 42finds2 4585 . . 3  |-  ( x  e.  om  ->  ( A  e.  om  ->  ( A  e.  x  \/  A  =  x  \/  x  e.  A ) ) )
445, 43vtoclga 2796 . 2  |-  ( B  e.  om  ->  ( A  e.  om  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A )
) )
4544impcom 124 1  |-  ( ( A  e.  om  /\  B  e.  om )  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 703    \/ w3o 972    = wceq 1348    e. wcel 2141   _Vcvv 2730   (/)c0 3414   suc csuc 4350   omcom 4574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-iinf 4572
This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-uni 3797  df-int 3832  df-tr 4088  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575
This theorem is referenced by:  nntri2  6473  nntri1  6475  nntri3  6476  nntri2or2  6477  nndceq  6478  nndcel  6479  nnsseleq  6480  nntr2  6482  nnawordex  6508  nnwetri  6893  nnnninfeq  7104  ltsopi  7282  pitri3or  7284  frec2uzlt2d  10360  ennnfonelemk  12355  ennnfonelemex  12369
  Copyright terms: Public domain W3C validator