Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cantnfle Structured version   Unicode version

Theorem cantnfle 8179
 Description: A lower bound on the CNF function. Since CNF is defined as the sum of over all in the support of , it is larger than any of these terms (and all other terms are zero, so we can extend the statement to all instead of just those in the support). (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 28-Jun-2019.)
Hypotheses
Ref Expression
cantnfs.s CNF
cantnfs.a
cantnfs.b
cantnfcl.g OrdIso supp
cantnfcl.f
cantnfval.h seq𝜔
cantnfle.c
Assertion
Ref Expression
cantnfle CNF
Distinct variable groups:   ,,   ,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)

Proof of Theorem cantnfle
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6311 . . 3
21sseq1d 3492 . 2 CNF CNF
3 cantnfs.b . . . . . . . . . 10
4 suppssdm 6936 . . . . . . . . . . 11 supp
5 cantnfcl.f . . . . . . . . . . . . . 14
6 cantnfs.s . . . . . . . . . . . . . . 15 CNF
7 cantnfs.a . . . . . . . . . . . . . . 15
86, 7, 3cantnfs 8174 . . . . . . . . . . . . . 14 finSupp
95, 8mpbid 214 . . . . . . . . . . . . 13 finSupp
109simpld 461 . . . . . . . . . . . 12
11 fdm 5748 . . . . . . . . . . . 12
1210, 11syl 17 . . . . . . . . . . 11
134, 12syl5sseq 3513 . . . . . . . . . 10 supp
143, 13ssexd 4569 . . . . . . . . 9 supp
15 cantnfcl.g . . . . . . . . . . 11 OrdIso supp
166, 7, 3, 15, 5cantnfcl 8175 . . . . . . . . . 10 supp
1716simpld 461 . . . . . . . . 9 supp
1815oiiso 8056 . . . . . . . . 9 supp supp supp
1914, 17, 18syl2anc 666 . . . . . . . 8 supp
20 isof1o 6229 . . . . . . . 8 supp supp
2119, 20syl 17 . . . . . . 7 supp
2221adantr 467 . . . . . 6 supp
23 f1ocnv 5841 . . . . . 6 supp supp
24 f1of 5829 . . . . . 6 supp supp
2522, 23, 243syl 18 . . . . 5 supp
26 cantnfle.c . . . . . . 7
2726anim1i 571 . . . . . 6
2810adantr 467 . . . . . . . 8
29 ffn 5744 . . . . . . . 8
3028, 29syl 17 . . . . . . 7
313adantr 467 . . . . . . 7
32 0ex 4554 . . . . . . . 8
3332a1i 11 . . . . . . 7
34 elsuppfn 6931 . . . . . . 7 supp
3530, 31, 33, 34syl3anc 1265 . . . . . 6 supp
3627, 35mpbird 236 . . . . 5 supp
3725, 36ffvelrnd 6036 . . . 4
3816simprd 465 . . . . . 6
3938adantr 467 . . . . 5
40 eqimss 3517 . . . . . . . . . 10
4140biantrurd 511 . . . . . . . . 9
42 eleq2 2496 . . . . . . . . 9
4341, 42bitr3d 259 . . . . . . . 8
44 fveq2 5879 . . . . . . . . 9
4544sseq2d 3493 . . . . . . . 8
4643, 45imbi12d 322 . . . . . . 7
4746imbi2d 318 . . . . . 6
48 sseq1 3486 . . . . . . . . 9
49 eleq2 2496 . . . . . . . . 9
5048, 49anbi12d 716 . . . . . . . 8
51 fveq2 5879 . . . . . . . . 9
5251sseq2d 3493 . . . . . . . 8
5350, 52imbi12d 322 . . . . . . 7
54 sseq1 3486 . . . . . . . . 9
55 eleq2 2496 . . . . . . . . 9
5654, 55anbi12d 716 . . . . . . . 8
57 fveq2 5879 . . . . . . . . 9
5857sseq2d 3493 . . . . . . . 8
5956, 58imbi12d 322 . . . . . . 7
60 sseq1 3486 . . . . . . . . 9
61 eleq2 2496 . . . . . . . . 9
6260, 61anbi12d 716 . . . . . . . 8
63 fveq2 5879 . . . . . . . . 9
6463sseq2d 3493 . . . . . . . 8
6562, 64imbi12d 322 . . . . . . 7
66 noel 3766 . . . . . . . . . 10
6766pm2.21i 135 . . . . . . . . 9
6867adantl 468 . . . . . . . 8
6968a1i 11 . . . . . . 7
70 fvex 5889 . . . . . . . . . . . 12
7170elsuc 5509 . . . . . . . . . . 11
72 sssucid 5517 . . . . . . . . . . . . . . . . 17
73 sstr 3473 . . . . . . . . . . . . . . . . 17
7472, 73mpan 675 . . . . . . . . . . . . . . . 16
7574ad2antrl 733 . . . . . . . . . . . . . . 15
76 simprr 765 . . . . . . . . . . . . . . 15
77 pm2.27 41 . . . . . . . . . . . . . . 15
7875, 76, 77syl2anc 666 . . . . . . . . . . . . . 14
79 cantnfval.h . . . . . . . . . . . . . . . . . . . . 21 seq𝜔
8079cantnfvalf 8173 . . . . . . . . . . . . . . . . . . . 20
8180ffvelrni 6034 . . . . . . . . . . . . . . . . . . 19
8281ad2antlr 732 . . . . . . . . . . . . . . . . . 18
837ad3antrrr 735 . . . . . . . . . . . . . . . . . . . 20
843ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . 21
8513ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . . 22 supp
86 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . 24
87 sucidg 5518 . . . . . . . . . . . . . . . . . . . . . . . . 25
8887ad2antlr 732 . . . . . . . . . . . . . . . . . . . . . . . 24
8986, 88sseldd 3466 . . . . . . . . . . . . . . . . . . . . . . 23
9015oif 8049 . . . . . . . . . . . . . . . . . . . . . . . 24 supp
9190ffvelrni 6034 . . . . . . . . . . . . . . . . . . . . . . 23 supp
9289, 91syl 17 . . . . . . . . . . . . . . . . . . . . . 22 supp
9385, 92sseldd 3466 . . . . . . . . . . . . . . . . . . . . 21
94 onelon 5465 . . . . . . . . . . . . . . . . . . . . 21
9584, 93, 94syl2anc 666 . . . . . . . . . . . . . . . . . . . 20
96 oecl 7245 . . . . . . . . . . . . . . . . . . . 20
9783, 95, 96syl2anc 666 . . . . . . . . . . . . . . . . . . 19
9810ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . 21
9998, 93ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . 20
100 onelon 5465 . . . . . . . . . . . . . . . . . . . 20
10183, 99, 100syl2anc 666 . . . . . . . . . . . . . . . . . . 19
102 omcl 7244 . . . . . . . . . . . . . . . . . . 19
10397, 101, 102syl2anc 666 . . . . . . . . . . . . . . . . . 18
104 oaword2 7260 . . . . . . . . . . . . . . . . . 18
10582, 103, 104syl2anc 666 . . . . . . . . . . . . . . . . 17
106 simplll 767 . . . . . . . . . . . . . . . . . 18
107 simplr 761 . . . . . . . . . . . . . . . . . 18
1086, 7, 3, 15, 5, 79cantnfsuc 8178 . . . . . . . . . . . . . . . . . 18
109106, 107, 108syl2anc 666 . . . . . . . . . . . . . . . . 17
110105, 109sseqtr4d 3502 . . . . . . . . . . . . . . . 16
111 sstr 3473 . . . . . . . . . . . . . . . . 17
112111expcom 437 . . . . . . . . . . . . . . . 16
113110, 112syl 17 . . . . . . . . . . . . . . 15
114113adantrr 722 . . . . . . . . . . . . . 14
11578, 114syld 46 . . . . . . . . . . . . 13
116115expr 619 . . . . . . . . . . . 12
117 simprr 765 . . . . . . . . . . . . . . . . . . . 20
118117fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
119 f1ocnvfv2 6189 . . . . . . . . . . . . . . . . . . . . 21 supp supp
12022, 36, 119syl2anc 666 . . . . . . . . . . . . . . . . . . . 20
121120ad2antrr 731 . . . . . . . . . . . . . . . . . . 19
122118, 121eqtr3d 2466 . . . . . . . . . . . . . . . . . 18
123122oveq2d 6319 . . . . . . . . . . . . . . . . 17
124122fveq2d 5883 . . . . . . . . . . . . . . . . 17
125123, 124oveq12d 6321 . . . . . . . . . . . . . . . 16
126 oaword1 7259 . . . . . . . . . . . . . . . . . 18
127103, 82, 126syl2anc 666 . . . . . . . . . . . . . . . . 17
128127adantrr 722 . . . . . . . . . . . . . . . 16
129125, 128eqsstr3d 3500 . . . . . . . . . . . . . . 15
130109adantrr 722 . . . . . . . . . . . . . . 15
131129, 130sseqtr4d 3502 . . . . . . . . . . . . . 14
132131expr 619 . . . . . . . . . . . . 13
133132a1dd 48 . . . . . . . . . . . 12
134116, 133jaod 382 . . . . . . . . . . 11
13571, 134syl5bi 221 . . . . . . . . . 10
136135expimpd 607 . . . . . . . . 9
137136com23 82 . . . . . . . 8
138137expcom 437 . . . . . . 7
13953, 59, 65, 69, 138finds2 6733 . . . . . 6
14047, 139vtoclga 3146 . . . . 5
14139, 140mpcom 38 . . . 4
14237, 141mpd 15 . . 3
1436, 7, 3, 15, 5, 79cantnfval 8176 . . . 4 CNF
144143adantr 467 . . 3 CNF
145142, 144sseqtr4d 3502 . 2 CNF
146 onelon 5465 . . . . . 6
1473, 26, 146syl2anc 666 . . . . 5
148 oecl 7245 . . . . 5
1497, 147, 148syl2anc 666 . . . 4
150 om0 7225 . . . 4
151149, 150syl 17 . . 3
152 0ss 3792 . . 3 CNF
153151, 152syl6eqss 3515 . 2 CNF
1542, 145, 153pm2.61ne 2740 1 CNF
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wo 370   wa 371   wceq 1438   wcel 1869   wne 2619  cvv 3082   wss 3437  c0 3762   class class class wbr 4421   cep 4760   wwe 4809  ccnv 4850   cdm 4851  con0 5440   csuc 5442   wfn 5594  wf 5595  wf1o 5598  cfv 5599   wiso 5600  (class class class)co 6303   cmpt2 6305  com 6704   supp csupp 6923  seq𝜔cseqom 7170   coa 7185   comu 7186   coe 7187   finSupp cfsupp 7887  OrdIsocoi 8028   CNF ccnf 8169 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-se 4811  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-isom 5608  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-supp 6924  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-seqom 7171  df-1o 7188  df-oadd 7192  df-omul 7193  df-oexp 7194  df-er 7369  df-map 7480  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-fsupp 7888  df-oi 8029  df-cnf 8170 This theorem is referenced by:  cantnflem3  8199
 Copyright terms: Public domain W3C validator