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

Theorem infsupneg 8801
 Description: If a set of real numbers has a greatest lower bound, the set of the negation of those numbers has a least upper bound. To go in the other direction see supinfneg 8800. (Contributed by Jim Kingdon, 15-Jan-2022.)
Hypotheses
Ref Expression
infsupneg.ex
infsupneg.ss
Assertion
Ref Expression
infsupneg
Distinct variable groups:   ,,,,   ,
Allowed substitution hints:   (,,)

Proof of Theorem infsupneg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 infsupneg.ex . . . 4
2 breq2 3810 . . . . . . . 8
32notbid 625 . . . . . . 7
43ralbidv 2373 . . . . . 6
5 breq1 3809 . . . . . . . 8
65imbi1d 229 . . . . . . 7
76ralbidv 2373 . . . . . 6
84, 7anbi12d 457 . . . . 5
98cbvrexv 2583 . . . 4
101, 9sylibr 132 . . 3
11 breq1 3809 . . . . . . 7
1211notbid 625 . . . . . 6
1312cbvralv 2582 . . . . 5
14 breq1 3809 . . . . . . . . 9
1514cbvrexv 2583 . . . . . . . 8
1615imbi2i 224 . . . . . . 7
1716ralbii 2377 . . . . . 6
18 breq2 3810 . . . . . . . 8
19 breq2 3810 . . . . . . . . 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 breq1 3809 . . . . . . . . . . . . 13
3837notbid 625 . . . . . . . . . . . 12
3938rspcv 2706 . . . . . . . . . . 11
4036, 39syl 14 . . . . . . . . . 10
4140adantr 270 . . . . . . . . 9
42 ltnegcon1 7670 . . . . . . . . . . . 12
4342ancoms 264 . . . . . . . . . . 11
4443notbid 625 . . . . . . . . . 10
4531, 44sylan 277 . . . . . . . . 9
4641, 45sylibrd 167 . . . . . . . 8
4746ancoms 264 . . . . . . 7
4847ralrimdva 2446 . . . . . 6
4929, 30, 48sylc 61 . . . . 5
50 nfv 1462 . . . . . . . . . . . 12
51 nfcv 2223 . . . . . . . . . . . . 13
52 nfv 1462 . . . . . . . . . . . . . 14
53 nfre1 2412 . . . . . . . . . . . . . 14
5452, 53nfim 1505 . . . . . . . . . . . . 13
5551, 54nfralya 2409 . . . . . . . . . . . 12
5650, 55nfan 1498 . . . . . . . . . . 11
57 nfv 1462 . . . . . . . . . . 11
5856, 57nfan 1498 . . . . . . . . . 10
59 nfv 1462 . . . . . . . . . 10
6058, 59nfan 1498 . . . . . . . . 9
61 simplr 497 . . . . . . . . . . . . 13
62 infsupneg.ss . . . . . . . . . . . . . . 15
6362sseld 3008 . . . . . . . . . . . . . 14
6463ad6antr 482 . . . . . . . . . . . . 13
6561, 64mpd 13 . . . . . . . . . . . 12
6665renegcld 7587 . . . . . . . . . . 11
6765recnd 7245 . . . . . . . . . . . . 13
6867negnegd 7513 . . . . . . . . . . . 12
6968, 61eqeltrd 2159 . . . . . . . . . . 11
70 negeq 7404 . . . . . . . . . . . . 13
7170eleq1d 2151 . . . . . . . . . . . 12
7271elrab 2758 . . . . . . . . . . 11
7366, 69, 72sylanbrc 408 . . . . . . . . . 10
74 simp-4r 509 . . . . . . . . . . 11
75 simpr 108 . . . . . . . . . . 11
7665, 74, 75ltnegcon2d 7729 . . . . . . . . . 10
77 breq2 3810 . . . . . . . . . . 11
7877rspcev 2710 . . . . . . . . . 10
7973, 76, 78syl2anc 403 . . . . . . . . 9
80 simpllr 501 . . . . . . . . . . 11
81 simpr 108 . . . . . . . . . . 11
82 simplr 497 . . . . . . . . . . 11
8380, 81, 82jca31 302 . . . . . . . . . 10
84 ltnegcon2 7671 . . . . . . . . . . . . . 14
8584ancoms 264 . . . . . . . . . . . . 13
8685adantr 270 . . . . . . . . . . . 12
87 renegcl 7472 . . . . . . . . . . . . . . 15
88 breq2 3810 . . . . . . . . . . . . . . . . 17
89 breq2 3810 . . . . . . . . . . . . . . . . . 18
9089rexbidv 2374 . . . . . . . . . . . . . . . . 17
9188, 90imbi12d 232 . . . . . . . . . . . . . . . 16
9291rspcv 2706 . . . . . . . . . . . . . . 15
9387, 92syl 14 . . . . . . . . . . . . . 14
9493adantl 271 . . . . . . . . . . . . 13
9594imp 122 . . . . . . . . . . . 12
9686, 95sylbid 148 . . . . . . . . . . 11
9796imp 122 . . . . . . . . . 10
9883, 97sylan 277 . . . . . . . . 9
9960, 79, 98r19.29af 2502 . . . . . . . 8
10099ex 113 . . . . . . 7
101100ralrimiva 2439 . . . . . 6
102101adantrl 462 . . . . 5
103 breq1 3809 . . . . . . . . 9
104103notbid 625 . . . . . . . 8
105104ralbidv 2373 . . . . . . 7
106 breq2 3810 . . . . . . . . 9
107106imbi1d 229 . . . . . . . 8
108107ralbidv 2373 . . . . . . 7
109105, 108anbi12d 457 . . . . . 6
110109rspcev 2710 . . . . 5
11128, 49, 102, 110syl12anc 1168 . . . 4
112111ex 113 . . 3
113112rexlimdva 2482 . 2
11426, 113mpd 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:  infssuzcldc  10538
 Copyright terms: Public domain W3C validator