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

Theorem cantnfleOLD 8141
Description: A lower bound on the function. Since 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.) Obsolete version of cantnfle 8111 as of 28-Jun-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
cantnfsOLD.1
cantnfsOLD.2
cantnfsOLD.3
cantnfvalOLD.3
cantnfvalOLD.4
cantnfvalOLD.5
cantnfleOLD.5
Assertion
Ref Expression
cantnfleOLD
Distinct variable groups:   , ,   ,   , ,   , ,   S, ,   , ,   , ,

Proof of Theorem cantnfleOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6304 . . 3
21sseq1d 3530 . 2
3 cantnfsOLD.3 . . . . . . . . . 10
4 cnvimass 5362 . . . . . . . . . . 11
5 cantnfvalOLD.4 . . . . . . . . . . . . . 14
6 cantnfsOLD.1 . . . . . . . . . . . . . . 15
7 cantnfsOLD.2 . . . . . . . . . . . . . . 15
86, 7, 3cantnfsOLD 8136 . . . . . . . . . . . . . 14
95, 8mpbid 210 . . . . . . . . . . . . 13
109simpld 459 . . . . . . . . . . . 12
11 fdm 5740 . . . . . . . . . . . 12
1210, 11syl 16 . . . . . . . . . . 11
134, 12syl5sseq 3551 . . . . . . . . . 10
143, 13ssexd 4599 . . . . . . . . 9
15 cantnfvalOLD.3 . . . . . . . . . . 11
166, 7, 3, 15, 5cantnfclOLD 8137 . . . . . . . . . 10
1716simpld 459 . . . . . . . . 9
1815oiiso 7983 . . . . . . . . 9
1914, 17, 18syl2anc 661 . . . . . . . 8
20 isof1o 6221 . . . . . . . 8
2119, 20syl 16 . . . . . . 7
2221adantr 465 . . . . . 6
23 f1ocnv 5833 . . . . . 6
24 f1of 5821 . . . . . 6
2522, 23, 243syl 20 . . . . 5
26 cantnfleOLD.5 . . . . . . 7
2726adantr 465 . . . . . 6
28 simpr 461 . . . . . . 7
29 fvex 5881 . . . . . . . 8
30 dif1o 7169 . . . . . . . 8
3129, 30mpbiran 918 . . . . . . 7
3228, 31sylibr 212 . . . . . 6
3310adantr 465 . . . . . . 7
34 ffn 5736 . . . . . . 7
35 elpreima 6007 . . . . . . 7
3633, 34, 353syl 20 . . . . . 6
3727, 32, 36mpbir2and 922 . . . . 5
3825, 37ffvelrnd 6032 . . . 4
3916simprd 463 . . . . . 6
4039adantr 465 . . . . 5
41 eqimss 3555 . . . . . . . . . 10
4241biantrurd 508 . . . . . . . . 9
43 eleq2 2530 . . . . . . . . 9
4442, 43bitr3d 255 . . . . . . . 8
45 fveq2 5871 . . . . . . . . 9
4645sseq2d 3531 . . . . . . . 8
4744, 46imbi12d 320 . . . . . . 7
4847imbi2d 316 . . . . . 6
49 sseq1 3524 . . . . . . . . 9
50 eleq2 2530 . . . . . . . . 9
5149, 50anbi12d 710 . . . . . . . 8
52 fveq2 5871 . . . . . . . . 9
5352sseq2d 3531 . . . . . . . 8
5451, 53imbi12d 320 . . . . . . 7
55 sseq1 3524 . . . . . . . . 9
56 eleq2 2530 . . . . . . . . 9
5755, 56anbi12d 710 . . . . . . . 8
58 fveq2 5871 . . . . . . . . 9
5958sseq2d 3531 . . . . . . . 8
6057, 59imbi12d 320 . . . . . . 7
61 sseq1 3524 . . . . . . . . 9
62 eleq2 2530 . . . . . . . . 9
6361, 62anbi12d 710 . . . . . . . 8
64 fveq2 5871 . . . . . . . . 9
6564sseq2d 3531 . . . . . . . 8
6663, 65imbi12d 320 . . . . . . 7
67 noel 3788 . . . . . . . . . 10
6867pm2.21i 131 . . . . . . . . 9
6968adantl 466 . . . . . . . 8
7069a1i 11 . . . . . . 7
71 fvex 5881 . . . . . . . . . . . 12
7271elsuc 4952 . . . . . . . . . . 11
73 sssucid 4960 . . . . . . . . . . . . . . . . 17
74 sstr 3511 . . . . . . . . . . . . . . . . 17
7573, 74mpan 670 . . . . . . . . . . . . . . . 16
7675ad2antrl 727 . . . . . . . . . . . . . . 15
77 simprr 757 . . . . . . . . . . . . . . 15
78 pm2.27 39 . . . . . . . . . . . . . . 15
7976, 77, 78syl2anc 661 . . . . . . . . . . . . . 14
80 cantnfvalOLD.5 . . . . . . . . . . . . . . . . . . . . 21
8180cantnfvalf 8105 . . . . . . . . . . . . . . . . . . . 20
8281ffvelrni 6030 . . . . . . . . . . . . . . . . . . 19
8382ad2antlr 726 . . . . . . . . . . . . . . . . . 18
847ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20
853ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21
8613ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22
87 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . 24
88 sucidg 4961 . . . . . . . . . . . . . . . . . . . . . . . . 25
8988ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . 24
9087, 89sseldd 3504 . . . . . . . . . . . . . . . . . . . . . . 23
9115oif 7976 . . . . . . . . . . . . . . . . . . . . . . . 24
9291ffvelrni 6030 . . . . . . . . . . . . . . . . . . . . . . 23
9390, 92syl 16 . . . . . . . . . . . . . . . . . . . . . 22
9486, 93sseldd 3504 . . . . . . . . . . . . . . . . . . . . 21
95 onelon 4908 . . . . . . . . . . . . . . . . . . . . 21
9685, 94, 95syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
97 oecl 7206 . . . . . . . . . . . . . . . . . . . 20
9884, 96, 97syl2anc 661 . . . . . . . . . . . . . . . . . . 19
9910ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21
10099, 94ffvelrnd 6032 . . . . . . . . . . . . . . . . . . . 20
101 onelon 4908 . . . . . . . . . . . . . . . . . . . 20
10284, 100, 101syl2anc 661 . . . . . . . . . . . . . . . . . . 19
103 omcl 7205 . . . . . . . . . . . . . . . . . . 19
10498, 102, 103syl2anc 661 . . . . . . . . . . . . . . . . . 18
105 oaword2 7221 . . . . . . . . . . . . . . . . . 18
10683, 104, 105syl2anc 661 . . . . . . . . . . . . . . . . 17
107 simplll 759 . . . . . . . . . . . . . . . . . 18
108 simplr 755 . . . . . . . . . . . . . . . . . 18
1096, 7, 3, 15, 5, 80cantnfsucOLD 8140 . . . . . . . . . . . . . . . . . 18
110107, 108, 109syl2anc 661 . . . . . . . . . . . . . . . . 17
111106, 110sseqtr4d 3540 . . . . . . . . . . . . . . . 16
112 sstr 3511 . . . . . . . . . . . . . . . . 17
113112expcom 435 . . . . . . . . . . . . . . . 16
114111, 113syl 16 . . . . . . . . . . . . . . 15
115114adantrr 716 . . . . . . . . . . . . . 14
11679, 115syld 44 . . . . . . . . . . . . 13
117116expr 615 . . . . . . . . . . . 12
118 simprr 757 . . . . . . . . . . . . . . . . . . . 20
119118fveq2d 5875 . . . . . . . . . . . . . . . . . . 19
120 f1ocnvfv2 6183 . . . . . . . . . . . . . . . . . . . . 21
12122, 37, 120syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
122121ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
123119, 122eqtr3d 2500 . . . . . . . . . . . . . . . . . 18
124123oveq2d 6312 . . . . . . . . . . . . . . . . 17
125123fveq2d 5875 . . . . . . . . . . . . . . . . 17
126124, 125oveq12d 6314 . . . . . . . . . . . . . . . 16
127 oaword1 7220 . . . . . . . . . . . . . . . . . 18
128104, 83, 127syl2anc 661 . . . . . . . . . . . . . . . . 17
129128adantrr 716 . . . . . . . . . . . . . . . 16
130126, 129eqsstr3d 3538 . . . . . . . . . . . . . . 15
131110adantrr 716 . . . . . . . . . . . . . . 15
132130, 131sseqtr4d 3540 . . . . . . . . . . . . . 14
133132expr 615 . . . . . . . . . . . . 13
134133a1dd 46 . . . . . . . . . . . 12
135117, 134jaod 380 . . . . . . . . . . 11
13672, 135syl5bi 217 . . . . . . . . . 10
137136expimpd 603 . . . . . . . . 9
138137com23 78 . . . . . . . 8
139138expcom 435 . . . . . . 7
14054, 60, 66, 70, 139finds2 6728 . . . . . 6
14148, 140vtoclga 3173 . . . . 5
14240, 141mpcom 36 . . . 4
14338, 142mpd 15 . . 3
1446, 7, 3, 15, 5, 80cantnfvalOLD 8138 . . . 4
145144adantr 465 . . 3
146143, 145sseqtr4d 3540 . 2
147 onelon 4908 . . . . . 6
1483, 26, 147syl2anc 661 . . . . 5
149 oecl 7206 . . . . 5
1507, 148, 149syl2anc 661 . . . 4
151 om0 7186 . . . 4
152150, 151syl 16 . . 3
153 0ss 3814 . . 3
154152, 153syl6eqss 3553 . 2
1552, 146, 154pm2.61ne 2772 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652   cvv 3109  \cdif 3472  C_wss 3475   c0 3784   cep 4794  Wewwe 4842   con0 4883  succsuc 4885  `'ccnv 5003  domcdm 5004  "cima 5007  Fnwfn 5588  -->wf 5589  -1-1-onto->wf1o 5592  `cfv 5593  Isomwiso 5594  (class class class)co 6296  e.cmpt2 6298   com 6700  seqomcseqom 7131   c1o 7142   coa 7146   comu 7147   coe 7148   cfn 7536  OrdIsocoi 7955   ccnf 8099
This theorem is referenced by:  cantnflem3OLD  8153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-se 4844  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-supp 6919  df-recs 7061  df-rdg 7095  df-seqom 7132  df-1o 7149  df-oadd 7153  df-omul 7154  df-oexp 7155  df-er 7330  df-map 7441  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-fsupp 7850  df-oi 7956  df-cnf 8100
  Copyright terms: Public domain W3C validator