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

Theorem iseqf1olemmo 10294
 Description: Lemma for seq3f1o 10306. Showing that is one-to-one. (Contributed by Jim Kingdon, 27-Aug-2022.)
Hypotheses
Ref Expression
iseqf1olemqf.k
iseqf1olemqf.j
iseqf1olemqf.q
iseqf1olemmo.a
iseqf1olemmo.b
iseqf1olemmo.eq
Assertion
Ref Expression
iseqf1olemmo
Distinct variable groups:   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem iseqf1olemmo
StepHypRef Expression
1 iseqf1olemqf.k . . . . 5
21ad2antrr 480 . . . 4
3 iseqf1olemqf.j . . . . 5
43ad2antrr 480 . . . 4
5 iseqf1olemmo.a . . . . 5
65ad2antrr 480 . . . 4
7 iseqf1olemmo.b . . . . 5
87ad2antrr 480 . . . 4
9 iseqf1olemmo.eq . . . . 5
109ad2antrr 480 . . . 4
11 iseqf1olemqf.q . . . 4
12 simplr 520 . . . 4
13 simpr 109 . . . 4
142, 4, 6, 8, 10, 11, 12, 13iseqf1olemab 10291 . . 3
15 simplr 520 . . . . 5
16 simpr 109 . . . . 5
1715, 16jca 304 . . . 4
181, 3, 5, 7, 9, 11iseqf1olemnab 10290 . . . . 5
1918ad2antrr 480 . . . 4
2017, 19pm2.21dd 610 . . 3
21 elfzelz 9835 . . . . . . 7
227, 21syl 14 . . . . . 6
23 elfzelz 9835 . . . . . . 7
241, 23syl 14 . . . . . 6
25 f1ocnv 5386 . . . . . . . . 9
26 f1of 5373 . . . . . . . . 9
273, 25, 263syl 17 . . . . . . . 8
2827, 1ffvelrnd 5562 . . . . . . 7
29 elfzelz 9835 . . . . . . 7
3028, 29syl 14 . . . . . 6
31 fzdcel 9849 . . . . . 6 DECID
3222, 24, 30, 31syl3anc 1217 . . . . 5 DECID
33 exmiddc 822 . . . . 5 DECID
3432, 33syl 14 . . . 4
3534adantr 274 . . 3
3614, 20, 35mpjaodan 788 . 2
37 simpr 109 . . . . 5
38 simplr 520 . . . . 5
3937, 38jca 304 . . . 4
409eqcomd 2146 . . . . . 6
411, 3, 7, 5, 40, 11iseqf1olemnab 10290 . . . . 5
4241ad2antrr 480 . . . 4
4339, 42pm2.21dd 610 . . 3
441ad2antrr 480 . . . 4
453ad2antrr 480 . . . 4
465ad2antrr 480 . . . 4
477ad2antrr 480 . . . 4
489ad2antrr 480 . . . 4
49 simplr 520 . . . 4
50 simpr 109 . . . 4
5144, 45, 46, 47, 48, 11, 49, 50iseqf1olemnanb 10292 . . 3
5234adantr 274 . . 3
5343, 51, 52mpjaodan 788 . 2
54 elfzelz 9835 . . . . 5
555, 54syl 14 . . . 4
56 fzdcel 9849 . . . 4 DECID
5755, 24, 30, 56syl3anc 1217 . . 3 DECID
58 exmiddc 822 . . 3 DECID
5957, 58syl 14 . 2
6036, 53, 59mpjaodan 788 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wo 698  DECID wdc 820   wceq 1332   wcel 1481  cif 3477   cmpt 3995  ccnv 4544  wf 5125  wf1o 5128  cfv 5129  (class class class)co 5780  c1 7643   cmin 7955  cz 9076  cfz 9819 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-sep 4052  ax-pow 4104  ax-pr 4137  ax-un 4361  ax-setind 4458  ax-cnex 7733  ax-resscn 7734  ax-1cn 7735  ax-1re 7736  ax-icn 7737  ax-addcl 7738  ax-addrcl 7739  ax-mulcl 7740  ax-addcom 7742  ax-addass 7744  ax-distr 7746  ax-i2m1 7747  ax-0lt1 7748  ax-0id 7750  ax-rnegex 7751  ax-cnre 7753  ax-pre-ltirr 7754  ax-pre-ltwlin 7755  ax-pre-lttrn 7756  ax-pre-ltadd 7758 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 2691  df-sbc 2913  df-dif 3076  df-un 3078  df-in 3080  df-ss 3087  df-if 3478  df-pw 3515  df-sn 3536  df-pr 3537  df-op 3539  df-uni 3743  df-int 3778  df-br 3936  df-opab 3996  df-mpt 3997  df-id 4221  df-xp 4551  df-rel 4552  df-cnv 4553  df-co 4554  df-dm 4555  df-rn 4556  df-res 4557  df-ima 4558  df-iota 5094  df-fun 5131  df-fn 5132  df-f 5133  df-f1 5134  df-fo 5135  df-f1o 5136  df-fv 5137  df-riota 5736  df-ov 5783  df-oprab 5784  df-mpo 5785  df-pnf 7824  df-mnf 7825  df-xr 7826  df-ltxr 7827  df-le 7828  df-sub 7957  df-neg 7958  df-inn 8743  df-n0 9000  df-z 9077  df-uz 9349  df-fz 9820 This theorem is referenced by:  iseqf1olemqf1o  10295
 Copyright terms: Public domain W3C validator