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

Theorem ennnfonelemhom 11998
 Description: Lemma for ennnfone 12008. The sequences in increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq DECID
ennnfonelemh.f
ennnfonelemh.ne
ennnfonelemh.g
ennnfonelemh.n frec
ennnfonelemh.j
ennnfonelemh.h
ennnfonelemhom.m
Assertion
Ref Expression
ennnfonelemhom
Distinct variable groups:   ,,,,,   ,   ,,,,,   ,   ,,,,   ,   ,   ,,,,   ,,   ,,,   ,   ,,,   ,,,
Allowed substitution hints:   (,,)   ()   (,,,,)   (,,,,)   (,,,,)   ()

Proof of Theorem ennnfonelemhom
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ennnfonelemhom.m . 2
2 eleq1 2203 . . . . 5
32rexbidv 2440 . . . 4
43imbi2d 229 . . 3
5 eleq1 2203 . . . . 5
65rexbidv 2440 . . . 4
76imbi2d 229 . . 3
8 eleq1 2203 . . . . 5
98rexbidv 2440 . . . 4
109imbi2d 229 . . 3
11 eleq1 2203 . . . . 5
1211rexbidv 2440 . . . 4
1312imbi2d 229 . . 3
14 1nn0 9044 . . . 4
15 0ex 4064 . . . . . 6
1615snid 3564 . . . . 5
17 ennnfonelemh.dceq . . . . . . . 8 DECID
18 ennnfonelemh.f . . . . . . . 8
19 ennnfonelemh.ne . . . . . . . 8
20 ennnfonelemh.g . . . . . . . 8
21 ennnfonelemh.n . . . . . . . 8 frec
22 ennnfonelemh.j . . . . . . . 8
23 ennnfonelemh.h . . . . . . . 8
2417, 18, 19, 20, 21, 22, 23ennnfonelem1 11990 . . . . . . 7
2524dmeqd 4752 . . . . . 6
26 peano1 4518 . . . . . . . 8
27 fof 5356 . . . . . . . . . 10
2818, 27syl 14 . . . . . . . . 9
2926a1i 9 . . . . . . . . 9
3028, 29ffvelrnd 5567 . . . . . . . 8
31 fnsng 5181 . . . . . . . 8
3226, 30, 31sylancr 411 . . . . . . 7
33 fndm 5233 . . . . . . 7
3432, 33syl 14 . . . . . 6
3525, 34eqtrd 2173 . . . . 5
3616, 35eleqtrrid 2230 . . . 4
37 fveq2 5432 . . . . . . 7
3837dmeqd 4752 . . . . . 6
3938eleq2d 2210 . . . . 5
4039rspcev 2794 . . . 4
4114, 36, 40sylancr 411 . . 3
4217ad3antrrr 484 . . . . . . . . 9 DECID
4318ad3antrrr 484 . . . . . . . . 9
4419ad3antrrr 484 . . . . . . . . . 10
45 fveq2 5432 . . . . . . . . . . . . . 14
4645neeq1d 2327 . . . . . . . . . . . . 13
4746ralbidv 2439 . . . . . . . . . . . 12
4847cbvrexv 2659 . . . . . . . . . . 11
4948ralbii 2445 . . . . . . . . . 10
5044, 49sylib 121 . . . . . . . . 9
51 simplr 520 . . . . . . . . 9
5242, 43, 50, 20, 21, 22, 23, 51ennnfonelemex 11997 . . . . . . . 8
5342ad2antrr 480 . . . . . . . . . . . . . 14 DECID
5443ad2antrr 480 . . . . . . . . . . . . . 14
5544ad2antrr 480 . . . . . . . . . . . . . 14
56 simplr 520 . . . . . . . . . . . . . 14
5753, 54, 55, 20, 21, 22, 23, 56ennnfonelemom 11991 . . . . . . . . . . . . 13
58 nnord 4536 . . . . . . . . . . . . 13
5957, 58syl 14 . . . . . . . . . . . 12
60 simpr 109 . . . . . . . . . . . 12
61 ordsucss 4430 . . . . . . . . . . . 12
6259, 60, 61sylc 62 . . . . . . . . . . 11
63 simpr 109 . . . . . . . . . . . . 13
6442, 43, 44, 20, 21, 22, 23, 51ennnfonelemom 11991 . . . . . . . . . . . . . 14
65 nnsucelsuc 6398 . . . . . . . . . . . . . 14
6664, 65syl 14 . . . . . . . . . . . . 13
6763, 66mpbid 146 . . . . . . . . . . . 12
6867ad2antrr 480 . . . . . . . . . . 11
6962, 68sseldd 3104 . . . . . . . . . 10
7069ex 114 . . . . . . . . 9
7170reximdva 2538 . . . . . . . 8
7252, 71mpd 13 . . . . . . 7
7372rexlimdva2 2556 . . . . . 6
74 fveq2 5432 . . . . . . . . 9
7574dmeqd 4752 . . . . . . . 8
7675eleq2d 2210 . . . . . . 7
7776cbvrexv 2659 . . . . . 6
7873, 77syl6ibr 161 . . . . 5
7978expcom 115 . . . 4
8079a2d 26 . . 3
814, 7, 10, 13, 41, 80finds 4524 . 2
821, 81mpcom 36 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104  DECID wdc 820   wceq 1332   wcel 1481   wne 2309  wral 2417  wrex 2418   cun 3075   wss 3077  c0 3369  cif 3480  csn 3533  cop 3536   cmpt 3998   word 4294   csuc 4297  com 4514  ccnv 4549   cdm 4550  cima 4553   wfn 5129  wf 5130  wfo 5132  cfv 5134  (class class class)co 5785   cmpo 5787  freccfrec 6298   cpm 6554  cc0 7671  c1 7672   caddc 7674   cmin 7984  cn0 9028  cz 9105   cseq 10276 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4052  ax-sep 4055  ax-nul 4063  ax-pow 4107  ax-pr 4141  ax-un 4365  ax-setind 4462  ax-iinf 4512  ax-cnex 7762  ax-resscn 7763  ax-1cn 7764  ax-1re 7765  ax-icn 7766  ax-addcl 7767  ax-addrcl 7768  ax-mulcl 7769  ax-addcom 7771  ax-addass 7773  ax-distr 7775  ax-i2m1 7776  ax-0lt1 7777  ax-0id 7779  ax-rnegex 7780  ax-cnre 7782  ax-pre-ltirr 7783  ax-pre-ltwlin 7784  ax-pre-lttrn 7785  ax-pre-ltadd 7787 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2692  df-sbc 2915  df-csb 3009  df-dif 3079  df-un 3081  df-in 3083  df-ss 3090  df-nul 3370  df-if 3481  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-int 3781  df-iun 3824  df-br 3939  df-opab 3999  df-mpt 4000  df-tr 4036  df-id 4225  df-iord 4298  df-on 4300  df-ilim 4301  df-suc 4303  df-iom 4515  df-xp 4556  df-rel 4557  df-cnv 4558  df-co 4559  df-dm 4560  df-rn 4561  df-res 4562  df-ima 4563  df-iota 5099  df-fun 5136  df-fn 5137  df-f 5138  df-f1 5139  df-fo 5140  df-f1o 5141  df-fv 5142  df-riota 5741  df-ov 5788  df-oprab 5789  df-mpo 5790  df-1st 6049  df-2nd 6050  df-recs 6213  df-frec 6299  df-pm 6556  df-pnf 7853  df-mnf 7854  df-xr 7855  df-ltxr 7856  df-le 7857  df-sub 7986  df-neg 7987  df-inn 8772  df-n0 9029  df-z 9106  df-uz 9378  df-seqfrec 10277 This theorem is referenced by:  ennnfonelemdm  12003
 Copyright terms: Public domain W3C validator