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

Theorem axpre-ltwlin 7188
 Description: Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 7228. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
Assertion
Ref Expression
axpre-ltwlin

Proof of Theorem axpre-ltwlin
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elreal 7136 . 2
2 elreal 7136 . 2
3 elreal 7136 . 2
4 breq1 3809 . . 3
5 breq1 3809 . . . 4
65orbi1d 738 . . 3
74, 6imbi12d 232 . 2
8 breq2 3810 . . 3
9 breq2 3810 . . . 4
109orbi2d 737 . . 3
118, 10imbi12d 232 . 2
12 breq2 3810 . . . 4
13 breq1 3809 . . . 4
1412, 13orbi12d 740 . . 3
1514imbi2d 228 . 2
16 ltsosr 7080 . . . 4
17 sowlin 4104 . . . 4
1816, 17mpan 415 . . 3
19 ltresr 7146 . . 3
20 ltresr 7146 . . . 4
21 ltresr 7146 . . . 4
2220, 21orbi12i 714 . . 3
2318, 19, 223imtr4g 203 . 2
241, 2, 3, 7, 11, 15, 233gencl 2643 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 662   w3a 920   wceq 1285   wcel 1434  cop 3420   class class class wbr 3806   wor 4079  cnr 6626  c0r 6627   cltr 6632  cr 7119   cltrr 7124 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 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3914  ax-sep 3917  ax-nul 3925  ax-pow 3969  ax-pr 3993  ax-un 4217  ax-setind 4309  ax-iinf 4358 This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2613  df-sbc 2826  df-csb 2919  df-dif 2985  df-un 2987  df-in 2989  df-ss 2996  df-nul 3269  df-pw 3403  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-int 3658  df-iun 3701  df-br 3807  df-opab 3861  df-mpt 3862  df-tr 3897  df-eprel 4073  df-id 4077  df-po 4080  df-iso 4081  df-iord 4150  df-on 4152  df-suc 4155  df-iom 4361  df-xp 4398  df-rel 4399  df-cnv 4400  df-co 4401  df-dm 4402  df-rn 4403  df-res 4404  df-ima 4405  df-iota 4918  df-fun 4955  df-fn 4956  df-f 4957  df-f1 4958  df-fo 4959  df-f1o 4960  df-fv 4961  df-ov 5568  df-oprab 5569  df-mpt2 5570  df-1st 5820  df-2nd 5821  df-recs 5976  df-irdg 6041  df-1o 6087  df-2o 6088  df-oadd 6091  df-omul 6092  df-er 6195  df-ec 6197  df-qs 6201  df-ni 6633  df-pli 6634  df-mi 6635  df-lti 6636  df-plpq 6673  df-mpq 6674  df-enq 6676  df-nqqs 6677  df-plqqs 6678  df-mqqs 6679  df-1nqqs 6680  df-rq 6681  df-ltnqqs 6682  df-enq0 6753  df-nq0 6754  df-0nq0 6755  df-plq0 6756  df-mq0 6757  df-inp 6795  df-i1p 6796  df-iplp 6797  df-iltp 6799  df-enr 7042  df-nr 7043  df-ltr 7046  df-0r 7047  df-r 7130  df-lt 7133 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator