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

Theorem supinfneg 8800
 Description: If a set of real numbers has a least upper bound, the set of the negation of those numbers has a greatest lower bound. For a theorem which is similar but only for the boundedness part, see ublbneg 8815. (Contributed by Jim Kingdon, 15-Jan-2022.)
Hypotheses
Ref Expression
supinfneg.ex
supinfneg.ss
Assertion
Ref Expression
supinfneg
Distinct variable groups:   ,,,,   ,
Allowed substitution hints:   (,,)

Proof of Theorem supinfneg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 supinfneg.ex . . . 4
2 breq1 3809 . . . . . . . 8
32notbid 625 . . . . . . 7
43ralbidv 2373 . . . . . 6
5 breq2 3810 . . . . . . . 8
65imbi1d 229 . . . . . . 7
76ralbidv 2373 . . . . . 6
84, 7anbi12d 457 . . . . 5
98cbvrexv 2583 . . . 4
101, 9sylibr 132 . . 3
11 breq2 3810 . . . . . . 7
1211notbid 625 . . . . . 6
1312cbvralv 2582 . . . . 5
14 breq2 3810 . . . . . . . . 9
1514cbvrexv 2583 . . . . . . . 8
1615imbi2i 224 . . . . . . 7
1716ralbii 2377 . . . . . 6
18 breq1 3809 . . . . . . . 8
19 breq1 3809 . . . . . . . . 9
2019rexbidv 2374 . . . . . . . 8
2118, 20imbi12d 232 . . . . . . 7
2221cbvralv 2582 . . . . . 6
2317, 22bitri 182 . . . . 5
2413, 23anbi12i 448 . . . 4
2524rexbii 2378 . . 3
2610, 25sylibr 132 . 2
27 renegcl 7472 . . . . . 6
2827ad2antlr 473 . . . . 5
29 simplr 497 . . . . . 6
30 simprl 498 . . . . . 6
31 elrabi 2755 . . . . . . . . . . . 12
32 negeq 7404 . . . . . . . . . . . . . . 15
3332eleq1d 2151 . . . . . . . . . . . . . 14
3433elrab3 2759 . . . . . . . . . . . . 13
3534biimpd 142 . . . . . . . . . . . 12
3631, 35mpcom 36 . . . . . . . . . . 11
37 breq2 3810 . . . . . . . . . . . . 13
3837notbid 625 . . . . . . . . . . . 12
3938rspcv 2706 . . . . . . . . . . 11
4036, 39syl 14 . . . . . . . . . 10
4140adantr 270 . . . . . . . . 9
42 ltnegcon2 7671 . . . . . . . . . . 11
4342notbid 625 . . . . . . . . . 10
4431, 43sylan 277 . . . . . . . . 9
4541, 44sylibrd 167 . . . . . . . 8
4645ancoms 264 . . . . . . 7
4746ralrimdva 2446 . . . . . 6
4829, 30, 47sylc 61 . . . . 5
49 nfv 1462 . . . . . . . . . . . 12
50 nfcv 2223 . . . . . . . . . . . . 13
51 nfv 1462 . . . . . . . . . . . . . 14
52 nfre1 2412 . . . . . . . . . . . . . 14
5351, 52nfim 1505 . . . . . . . . . . . . 13
5450, 53nfralya 2409 . . . . . . . . . . . 12
5549, 54nfan 1498 . . . . . . . . . . 11
56 nfv 1462 . . . . . . . . . . 11
5755, 56nfan 1498 . . . . . . . . . 10
58 nfv 1462 . . . . . . . . . 10
5957, 58nfan 1498 . . . . . . . . 9
60 simplr 497 . . . . . . . . . . . . 13
61 supinfneg.ss . . . . . . . . . . . . . . 15
6261sseld 3008 . . . . . . . . . . . . . 14
6362ad6antr 482 . . . . . . . . . . . . 13
6460, 63mpd 13 . . . . . . . . . . . 12
6564renegcld 7587 . . . . . . . . . . 11
6664recnd 7245 . . . . . . . . . . . . 13
6766negnegd 7513 . . . . . . . . . . . 12
6867, 60eqeltrd 2159 . . . . . . . . . . 11
69 negeq 7404 . . . . . . . . . . . . 13
7069eleq1d 2151 . . . . . . . . . . . 12
7170elrab 2758 . . . . . . . . . . 11
7265, 68, 71sylanbrc 408 . . . . . . . . . 10
73 simp-4r 509 . . . . . . . . . . 11
74 simpr 108 . . . . . . . . . . 11
7573, 64, 74ltnegcon1d 7728 . . . . . . . . . 10
76 breq1 3809 . . . . . . . . . . 11
7776rspcev 2710 . . . . . . . . . 10
7872, 75, 77syl2anc 403 . . . . . . . . 9
79 simpllr 501 . . . . . . . . . . 11
80 simpr 108 . . . . . . . . . . 11
81 simplr 497 . . . . . . . . . . 11
8279, 80, 81jca31 302 . . . . . . . . . 10
83 ltnegcon1 7670 . . . . . . . . . . . . 13
8483adantr 270 . . . . . . . . . . . 12
85 renegcl 7472 . . . . . . . . . . . . . . 15
86 breq1 3809 . . . . . . . . . . . . . . . . 17
87 breq1 3809 . . . . . . . . . . . . . . . . . 18
8887rexbidv 2374 . . . . . . . . . . . . . . . . 17
8986, 88imbi12d 232 . . . . . . . . . . . . . . . 16
9089rspcv 2706 . . . . . . . . . . . . . . 15
9185, 90syl 14 . . . . . . . . . . . . . 14
9291adantl 271 . . . . . . . . . . . . 13
9392imp 122 . . . . . . . . . . . 12
9484, 93sylbid 148 . . . . . . . . . . 11
9594imp 122 . . . . . . . . . 10
9682, 95sylan 277 . . . . . . . . 9
9759, 78, 96r19.29af 2502 . . . . . . . 8
9897ex 113 . . . . . . 7
9998ralrimiva 2439 . . . . . 6
10099adantrl 462 . . . . 5
101 breq2 3810 . . . . . . . . 9
102101notbid 625 . . . . . . . 8
103102ralbidv 2373 . . . . . . 7
104 breq1 3809 . . . . . . . . 9
105104imbi1d 229 . . . . . . . 8
106105ralbidv 2373 . . . . . . 7
107103, 106anbi12d 457 . . . . . 6
108107rspcev 2710 . . . . 5
10928, 48, 100, 108syl12anc 1168 . . . 4
110109ex 113 . . 3
111110rexlimdva 2482 . 2
11226, 111mpd 13 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 102   wb 103   wceq 1285   wcel 1434  wral 2353  wrex 2354  crab 2357   wss 2983   class class class wbr 3806  cr 7078   clt 7251  cneg 7383 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-sep 3917  ax-pow 3969  ax-pr 3993  ax-un 4217  ax-setind 4309  ax-cnex 7165  ax-resscn 7166  ax-1cn 7167  ax-1re 7168  ax-icn 7169  ax-addcl 7170  ax-addrcl 7171  ax-mulcl 7172  ax-addcom 7174  ax-addass 7176  ax-distr 7178  ax-i2m1 7179  ax-0id 7182  ax-rnegex 7183  ax-cnre 7185  ax-pre-ltadd 7190 This theorem depends on definitions:  df-bi 115  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-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2612  df-sbc 2826  df-dif 2985  df-un 2987  df-in 2989  df-ss 2996  df-pw 3403  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-br 3807  df-opab 3861  df-id 4077  df-xp 4398  df-rel 4399  df-cnv 4400  df-co 4401  df-dm 4402  df-iota 4918  df-fun 4955  df-fv 4961  df-riota 5520  df-ov 5567  df-oprab 5568  df-mpt2 5569  df-pnf 7253  df-mnf 7254  df-ltxr 7256  df-sub 7384  df-neg 7385 This theorem is referenced by:  supminfex  8802  infssuzex  10536
 Copyright terms: Public domain W3C validator