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

Theorem cantnfle 7619
 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.)
Hypotheses
Ref Expression
cantnfs.1 CNF
cantnfs.2
cantnfs.3
cantnfval.3 OrdIso
cantnfval.4
cantnfval.5 seq𝜔
cantnfle.5
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 6082 . . 3
21sseq1d 3368 . 2 CNF CNF
3 cantnfs.3 . . . . . . . . . 10
4 cnvimass 5217 . . . . . . . . . . 11
5 cantnfval.4 . . . . . . . . . . . . . 14
6 cantnfs.1 . . . . . . . . . . . . . . 15 CNF
7 cantnfs.2 . . . . . . . . . . . . . . 15
86, 7, 3cantnfs 7614 . . . . . . . . . . . . . 14
95, 8mpbid 202 . . . . . . . . . . . . 13
109simpld 446 . . . . . . . . . . . 12
11 fdm 5588 . . . . . . . . . . . 12
1210, 11syl 16 . . . . . . . . . . 11
134, 12syl5sseq 3389 . . . . . . . . . 10
143, 13ssexd 4343 . . . . . . . . 9
15 cantnfval.3 . . . . . . . . . . 11 OrdIso
166, 7, 3, 15, 5cantnfcl 7615 . . . . . . . . . 10
1716simpld 446 . . . . . . . . 9
1815oiiso 7499 . . . . . . . . 9
1914, 17, 18syl2anc 643 . . . . . . . 8
20 isof1o 6038 . . . . . . . 8
2119, 20syl 16 . . . . . . 7
2221adantr 452 . . . . . 6
23 f1ocnv 5680 . . . . . 6
24 f1of 5667 . . . . . 6
2522, 23, 243syl 19 . . . . 5
26 cantnfle.5 . . . . . . 7
2726adantr 452 . . . . . 6
28 simpr 448 . . . . . . 7
29 fvex 5735 . . . . . . . 8
30 dif1o 6737 . . . . . . . 8
3129, 30mpbiran 885 . . . . . . 7
3228, 31sylibr 204 . . . . . 6
3310adantr 452 . . . . . . 7
34 ffn 5584 . . . . . . 7
35 elpreima 5843 . . . . . . 7
3633, 34, 353syl 19 . . . . . 6
3727, 32, 36mpbir2and 889 . . . . 5
3825, 37ffvelrnd 5864 . . . 4
3916simprd 450 . . . . . 6
4039adantr 452 . . . . 5
41 eqimss 3393 . . . . . . . . . 10
4241biantrurd 495 . . . . . . . . 9
43 eleq2 2497 . . . . . . . . 9
4442, 43bitr3d 247 . . . . . . . 8
45 fveq2 5721 . . . . . . . . 9
4645sseq2d 3369 . . . . . . . 8
4744, 46imbi12d 312 . . . . . . 7
4847imbi2d 308 . . . . . 6
49 sseq1 3362 . . . . . . . . 9
50 eleq2 2497 . . . . . . . . 9
5149, 50anbi12d 692 . . . . . . . 8
52 fveq2 5721 . . . . . . . . 9
5352sseq2d 3369 . . . . . . . 8
5451, 53imbi12d 312 . . . . . . 7
55 sseq1 3362 . . . . . . . . 9
56 eleq2 2497 . . . . . . . . 9
5755, 56anbi12d 692 . . . . . . . 8
58 fveq2 5721 . . . . . . . . 9
5958sseq2d 3369 . . . . . . . 8
6057, 59imbi12d 312 . . . . . . 7
61 sseq1 3362 . . . . . . . . 9
62 eleq2 2497 . . . . . . . . 9
6361, 62anbi12d 692 . . . . . . . 8
64 fveq2 5721 . . . . . . . . 9
6564sseq2d 3369 . . . . . . . 8
6663, 65imbi12d 312 . . . . . . 7
67 noel 3625 . . . . . . . . . 10
6867pm2.21i 125 . . . . . . . . 9
6968adantl 453 . . . . . . . 8
7069a1i 11 . . . . . . 7
71 fvex 5735 . . . . . . . . . . . 12
7271elsuc 4643 . . . . . . . . . . 11
73 sssucid 4651 . . . . . . . . . . . . . . . . 17
74 sstr 3349 . . . . . . . . . . . . . . . . 17
7573, 74mpan 652 . . . . . . . . . . . . . . . 16
7675ad2antrl 709 . . . . . . . . . . . . . . 15
77 simprr 734 . . . . . . . . . . . . . . 15
78 pm2.27 37 . . . . . . . . . . . . . . 15
7976, 77, 78syl2anc 643 . . . . . . . . . . . . . 14
80 cantnfval.5 . . . . . . . . . . . . . . . . . . . . 21 seq𝜔
8180cantnfvalf 7613 . . . . . . . . . . . . . . . . . . . 20
8281ffvelrni 5862 . . . . . . . . . . . . . . . . . . 19
8382ad2antlr 708 . . . . . . . . . . . . . . . . . 18
847ad3antrrr 711 . . . . . . . . . . . . . . . . . . . 20
853ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . 21
8613ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . 22
87 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24
88 sucidg 4652 . . . . . . . . . . . . . . . . . . . . . . . . 25
8988ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24
9087, 89sseldd 3342 . . . . . . . . . . . . . . . . . . . . . . 23
9115oif 7492 . . . . . . . . . . . . . . . . . . . . . . . 24
9291ffvelrni 5862 . . . . . . . . . . . . . . . . . . . . . . 23
9390, 92syl 16 . . . . . . . . . . . . . . . . . . . . . 22
9486, 93sseldd 3342 . . . . . . . . . . . . . . . . . . . . 21
95 onelon 4599 . . . . . . . . . . . . . . . . . . . . 21
9685, 94, 95syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
97 oecl 6774 . . . . . . . . . . . . . . . . . . . 20
9884, 96, 97syl2anc 643 . . . . . . . . . . . . . . . . . . 19
9910ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . 21
10099, 94ffvelrnd 5864 . . . . . . . . . . . . . . . . . . . 20
101 onelon 4599 . . . . . . . . . . . . . . . . . . . 20
10284, 100, 101syl2anc 643 . . . . . . . . . . . . . . . . . . 19
103 omcl 6773 . . . . . . . . . . . . . . . . . . 19
10498, 102, 103syl2anc 643 . . . . . . . . . . . . . . . . . 18
105 oaword2 6789 . . . . . . . . . . . . . . . . . 18
10683, 104, 105syl2anc 643 . . . . . . . . . . . . . . . . 17
107 simplll 735 . . . . . . . . . . . . . . . . . 18
108 simplr 732 . . . . . . . . . . . . . . . . . 18
1096, 7, 3, 15, 5, 80cantnfsuc 7618 . . . . . . . . . . . . . . . . . 18
110107, 108, 109syl2anc 643 . . . . . . . . . . . . . . . . 17
111106, 110sseqtr4d 3378 . . . . . . . . . . . . . . . 16
112 sstr 3349 . . . . . . . . . . . . . . . . 17
113112expcom 425 . . . . . . . . . . . . . . . 16
114111, 113syl 16 . . . . . . . . . . . . . . 15
115114adantrr 698 . . . . . . . . . . . . . 14
11679, 115syld 42 . . . . . . . . . . . . 13
117116expr 599 . . . . . . . . . . . 12
118 simprr 734 . . . . . . . . . . . . . . . . . . . 20
119118fveq2d 5725 . . . . . . . . . . . . . . . . . . 19
120 f1ocnvfv2 6008 . . . . . . . . . . . . . . . . . . . . 21
12122, 37, 120syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
122121ad2antrr 707 . . . . . . . . . . . . . . . . . . 19
123119, 122eqtr3d 2470 . . . . . . . . . . . . . . . . . 18
124123oveq2d 6090 . . . . . . . . . . . . . . . . 17
125123fveq2d 5725 . . . . . . . . . . . . . . . . 17
126124, 125oveq12d 6092 . . . . . . . . . . . . . . . 16
127 oaword1 6788 . . . . . . . . . . . . . . . . . 18
128104, 83, 127syl2anc 643 . . . . . . . . . . . . . . . . 17
129128adantrr 698 . . . . . . . . . . . . . . . 16
130126, 129eqsstr3d 3376 . . . . . . . . . . . . . . 15
131110adantrr 698 . . . . . . . . . . . . . . 15
132130, 131sseqtr4d 3378 . . . . . . . . . . . . . 14
133132expr 599 . . . . . . . . . . . . 13
134133a1dd 44 . . . . . . . . . . . 12
135117, 134jaod 370 . . . . . . . . . . 11
13672, 135syl5bi 209 . . . . . . . . . 10
137136expimpd 587 . . . . . . . . 9
138137com23 74 . . . . . . . 8
139138expcom 425 . . . . . . 7
14054, 60, 66, 70, 139finds2 4866 . . . . . 6
14148, 140vtoclga 3010 . . . . 5
14240, 141mpcom 34 . . . 4
14338, 142mpd 15 . . 3
1446, 7, 3, 15, 5, 80cantnfval 7616 . . . 4 CNF
145144adantr 452 . . 3 CNF
146143, 145sseqtr4d 3378 . 2 CNF
147 onelon 4599 . . . . . 6
1483, 26, 147syl2anc 643 . . . . 5
149 oecl 6774 . . . . 5
1507, 148, 149syl2anc 643 . . . 4
151 om0 6754 . . . 4
152150, 151syl 16 . . 3
153 0ss 3649 . . 3 CNF
154152, 153syl6eqss 3391 . 2 CNF
1552, 146, 154pm2.61ne 2674 1 CNF
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wo 358   wa 359   wceq 1652   wcel 1725   wne 2599  cvv 2949   cdif 3310   wss 3313  c0 3621   cep 4485   wwe 4533  con0 4574   csuc 4576  com 4838  ccnv 4870   cdm 4871  cima 4874   wfn 5442  wf 5443  wf1o 5446  cfv 5447   wiso 5448  (class class class)co 6074   cmpt2 6076  seq𝜔cseqom 6697  c1o 6710   coa 6714   comu 6715   coe 6716  cfn 7102  OrdIsocoi 7471   CNF ccnf 7609 This theorem is referenced by:  cantnflem3  7640 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4313  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396  ax-un 4694 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-reu 2705  df-rmo 2706  df-rab 2707  df-v 2951  df-sbc 3155  df-csb 3245  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-tp 3815  df-op 3816  df-uni 4009  df-iun 4088  df-br 4206  df-opab 4260  df-mpt 4261  df-tr 4296  df-eprel 4487  df-id 4491  df-po 4496  df-so 4497  df-fr 4534  df-se 4535  df-we 4536  df-ord 4577  df-on 4578  df-lim 4579  df-suc 4580  df-om 4839  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-f1 5452  df-fo 5453  df-f1o 5454  df-fv 5455  df-isom 5456  df-ov 6077  df-oprab 6078  df-mpt2 6079  df-1st 6342  df-2nd 6343  df-riota 6542  df-recs 6626  df-rdg 6661  df-seqom 6698  df-1o 6717  df-oadd 6721  df-omul 6722  df-oexp 6723  df-er 6898  df-map 7013  df-en 7103  df-dom 7104  df-sdom 7105  df-fin 7106  df-oi 7472  df-cnf 7610
 Copyright terms: Public domain W3C validator