NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ltfintri Unicode version

Theorem ltfintri 4466
Description: Trichotomy law for finite less than. (Contributed by SF, 29-Jan-2015.)
Assertion
Ref Expression
ltfintri Nn Nn <fin <fin

Proof of Theorem ltfintri
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opkeq2 4060 . . . . . . . 8
21eleq1d 2419 . . . . . . 7 <fin <fin
3 eqeq2 2362 . . . . . . 7
4 opkeq1 4059 . . . . . . . 8
54eleq1d 2419 . . . . . . 7 <fin <fin
62, 3, 53orbi123d 1251 . . . . . 6 <fin <fin <fin <fin
76imbi2d 307 . . . . 5 <fin <fin <fin <fin
87imbi2d 307 . . . 4 Nn <fin <fin Nn <fin <fin
9 ltfintrilem1 4465 . . . . . 6 Nn <fin <fin
10 neeq1 2524 . . . . . . . 8 0c 0c
11 opkeq1 4059 . . . . . . . . . 10 0c 0c
1211eleq1d 2419 . . . . . . . . 9 0c <fin 0c <fin
13 eqeq1 2359 . . . . . . . . 9 0c 0c
14 opkeq2 4060 . . . . . . . . . 10 0c 0c
1514eleq1d 2419 . . . . . . . . 9 0c <fin 0c <fin
1612, 13, 153orbi123d 1251 . . . . . . . 8 0c <fin <fin 0c <fin 0c 0c <fin
1710, 16imbi12d 311 . . . . . . 7 0c <fin <fin 0c 0c <fin 0c 0c <fin
1817imbi2d 307 . . . . . 6 0c Nn <fin <fin Nn 0c 0c <fin 0c 0c <fin
19 neeq1 2524 . . . . . . . 8
20 opkeq1 4059 . . . . . . . . . 10
2120eleq1d 2419 . . . . . . . . 9 <fin <fin
22 eqeq1 2359 . . . . . . . . 9
23 opkeq2 4060 . . . . . . . . . 10
2423eleq1d 2419 . . . . . . . . 9 <fin <fin
2521, 22, 243orbi123d 1251 . . . . . . . 8 <fin <fin <fin <fin
2619, 25imbi12d 311 . . . . . . 7 <fin <fin <fin <fin
2726imbi2d 307 . . . . . 6 Nn <fin <fin Nn <fin <fin
28 neeq1 2524 . . . . . . . 8 1c 1c
29 opkeq1 4059 . . . . . . . . . 10 1c 1c
3029eleq1d 2419 . . . . . . . . 9 1c <fin 1c <fin
31 eqeq1 2359 . . . . . . . . 9 1c 1c
32 opkeq2 4060 . . . . . . . . . 10 1c 1c
3332eleq1d 2419 . . . . . . . . 9 1c <fin 1c <fin
3430, 31, 333orbi123d 1251 . . . . . . . 8 1c <fin <fin 1c <fin 1c 1c <fin
3528, 34imbi12d 311 . . . . . . 7 1c <fin <fin 1c 1c <fin 1c 1c <fin
3635imbi2d 307 . . . . . 6 1c Nn <fin <fin Nn 1c 1c <fin 1c 1c <fin
37 neeq1 2524 . . . . . . . 8
38 opkeq1 4059 . . . . . . . . . 10
3938eleq1d 2419 . . . . . . . . 9 <fin <fin
40 eqeq1 2359 . . . . . . . . 9
41 opkeq2 4060 . . . . . . . . . 10
4241eleq1d 2419 . . . . . . . . 9 <fin <fin
4339, 40, 423orbi123d 1251 . . . . . . . 8 <fin <fin <fin <fin
4437, 43imbi12d 311 . . . . . . 7 <fin <fin <fin <fin
4544imbi2d 307 . . . . . 6 Nn <fin <fin Nn <fin <fin
46 0cminle 4461 . . . . . . . . . 10 Nn 0c <_fin
4746adantr 451 . . . . . . . . 9 Nn 0c 0c <_fin
48 0cex 4392 . . . . . . . . . . 11 0c
49 lefinlteq 4463 . . . . . . . . . . 11 0c Nn 0c 0c <_fin 0c <fin 0c
5048, 49mp3an1 1264 . . . . . . . . . 10 Nn 0c 0c <_fin 0c <fin 0c
51 orcom 376 . . . . . . . . . 10 0c <fin 0c 0c 0c <fin
5250, 51syl6bb 252 . . . . . . . . 9 Nn 0c 0c <_fin 0c 0c <fin
5347, 52mpbid 201 . . . . . . . 8 Nn 0c 0c 0c <fin
54 3mix2 1125 . . . . . . . . 9 0c 0c <fin 0c 0c <fin
55 3mix1 1124 . . . . . . . . 9 0c <fin 0c <fin 0c 0c <fin
5654, 55jaoi 368 . . . . . . . 8 0c 0c <fin 0c <fin 0c 0c <fin
5753, 56syl 15 . . . . . . 7 Nn 0c 0c <fin 0c 0c <fin
5857ex 423 . . . . . 6 Nn 0c 0c <fin 0c 0c <fin
59 addcnnul 4453 . . . . . . . . . . . . 13 1c 1c
6059simpld 445 . . . . . . . . . . . 12 1c
61603ad2ant3 978 . . . . . . . . . . 11 Nn Nn 1c
62 addc32 4416 . . . . . . . . . . . . . . . . . . . 20 1c 1c
6362eqeq2i 2363 . . . . . . . . . . . . . . . . . . 19 1c 1c
6463rexbii 2639 . . . . . . . . . . . . . . . . . 18 Nn 1c Nn 1c
6564biimpi 186 . . . . . . . . . . . . . . . . 17 Nn 1c Nn 1c
6665adantl 452 . . . . . . . . . . . . . . . 16 Nn 1c Nn 1c
6766a1i 10 . . . . . . . . . . . . . . 15 Nn Nn 1c Nn 1c Nn 1c
68 opkltfing 4449 . . . . . . . . . . . . . . . 16 Nn Nn <fin Nn 1c
69683adant3 975 . . . . . . . . . . . . . . 15 Nn Nn 1c <fin Nn 1c
70 simp1 955 . . . . . . . . . . . . . . . . 17 Nn Nn 1c Nn
71 peano2 4403 . . . . . . . . . . . . . . . . 17 Nn 1c Nn
7270, 71syl 15 . . . . . . . . . . . . . . . 16 Nn Nn 1c 1c Nn
73 simp2 956 . . . . . . . . . . . . . . . 16 Nn Nn 1c Nn
74 opklefing 4448 . . . . . . . . . . . . . . . 16 1c Nn Nn 1c <_fin Nn 1c
7572, 73, 74syl2anc 642 . . . . . . . . . . . . . . 15 Nn Nn 1c 1c <_fin Nn 1c
7667, 69, 753imtr4d 259 . . . . . . . . . . . . . 14 Nn Nn 1c <fin 1c <_fin
77 lefinlteq 4463 . . . . . . . . . . . . . . 15 1c Nn Nn 1c 1c <_fin 1c <fin 1c
7871, 77syl3an1 1215 . . . . . . . . . . . . . 14 Nn Nn 1c 1c <_fin 1c <fin 1c
7976, 78sylibd 205 . . . . . . . . . . . . 13 Nn Nn 1c <fin 1c <fin 1c
80 3mix1 1124 . . . . . . . . . . . . . 14 1c <fin 1c <fin 1c 1c <fin
81 3mix2 1125 . . . . . . . . . . . . . 14 1c 1c <fin 1c 1c <fin
8280, 81jaoi 368 . . . . . . . . . . . . 13 1c <fin 1c 1c <fin 1c 1c <fin
8379, 82syl6 29 . . . . . . . . . . . 12 Nn Nn 1c <fin 1c <fin 1c 1c <fin
84 ltfinp1 4462 . . . . . . . . . . . . . . . 16 Nn 1c <fin
8560, 84sylan2 460 . . . . . . . . . . . . . . 15 Nn 1c 1c <fin
86853adant2 974 . . . . . . . . . . . . . 14 Nn Nn 1c 1c <fin
87 opkeq1 4059 . . . . . . . . . . . . . . 15 1c 1c
8887eleq1d 2419 . . . . . . . . . . . . . 14 1c <fin 1c <fin
8986, 88syl5ibcom 211 . . . . . . . . . . . . 13 Nn Nn 1c 1c <fin
90 3mix3 1126 . . . . . . . . . . . . 13 1c <fin 1c <fin 1c 1c <fin
9189, 90syl6 29 . . . . . . . . . . . 12 Nn Nn 1c 1c <fin 1c 1c <fin
92 ltfintr 4459 . . . . . . . . . . . . . . 15 Nn Nn 1c Nn <fin 1c <fin 1c <fin
9373, 70, 72, 92syl3anc 1182 . . . . . . . . . . . . . 14 Nn Nn 1c <fin 1c <fin 1c <fin
9486, 93mpan2d 655 . . . . . . . . . . . . 13 Nn Nn 1c <fin 1c <fin
9594, 90syl6 29 . . . . . . . . . . . 12 Nn Nn 1c <fin 1c <fin 1c 1c <fin
9683, 91, 953jaod 1246 . . . . . . . . . . 11 Nn Nn 1c <fin <fin 1c <fin 1c 1c <fin
9761, 96embantd 50 . . . . . . . . . 10 Nn Nn 1c <fin <fin 1c <fin 1c 1c <fin
98973expia 1153 . . . . . . . . 9 Nn Nn 1c <fin <fin 1c <fin 1c 1c <fin
9998com23 72 . . . . . . . 8 Nn Nn <fin <fin 1c 1c <fin 1c 1c <fin
10099ex 423 . . . . . . 7 Nn Nn <fin <fin 1c 1c <fin 1c 1c <fin
101100a2d 23 . . . . . 6 Nn Nn <fin <fin Nn 1c 1c <fin 1c 1c <fin
1029, 18, 27, 36, 45, 58, 101finds 4411 . . . . 5 Nn Nn <fin <fin
103102com12 27 . . . 4 Nn Nn <fin <fin
1048, 103vtoclga 2920 . . 3 Nn Nn <fin <fin
105104com12 27 . 2 Nn Nn <fin <fin
1061053imp 1145 1 Nn Nn <fin <fin
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176   wo 357   wa 358   w3o 933   w3a 934   wceq 1642   wcel 1710   wne 2516  wrex 2615  cvv 2859  c0 3550  copk 4057  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   cplc 4375   <_fin clefin 4432   <fin cltfin 4433
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-0c 4377  df-addc 4378  df-nnc 4379  df-lefin 4440  df-ltfin 4441
This theorem is referenced by:  lenltfin  4469  tfinltfin  4501  sfin111  4536
  Copyright terms: Public domain W3C validator