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

Theorem ennnfonelemhf1o 11985
 Description: Lemma for ennnfone 11997. Each of the functions in is one to one and onto an image of . (Contributed by Jim Kingdon, 17-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq DECID
ennnfonelemh.f
ennnfonelemh.ne
ennnfonelemh.g
ennnfonelemh.n frec
ennnfonelemh.j
ennnfonelemh.h
ennnfonelemhf1o.p
Assertion
Ref Expression
ennnfonelemhf1o
Distinct variable groups:   ,,,   ,,,,   ,   ,,,,   ,   ,,,,   ,,,,
Allowed substitution hints:   ()   (,)   (,,,,)   ()   (,,,)   ()   (,,,)   ()

Proof of Theorem ennnfonelemhf1o
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ennnfonelemhf1o.p . 2
2 fveq2 5431 . . . . 5
32dmeqd 4751 . . . . 5
4 fveq2 5431 . . . . . 6
54imaeq2d 4891 . . . . 5
62, 3, 5f1oeq123d 5372 . . . 4
76imbi2d 229 . . 3
8 fveq2 5431 . . . . 5
98dmeqd 4751 . . . . 5
10 fveq2 5431 . . . . . 6
1110imaeq2d 4891 . . . . 5
128, 9, 11f1oeq123d 5372 . . . 4
1312imbi2d 229 . . 3
14 fveq2 5431 . . . . 5
1514dmeqd 4751 . . . . 5
16 fveq2 5431 . . . . . 6
1716imaeq2d 4891 . . . . 5
1814, 15, 17f1oeq123d 5372 . . . 4
1918imbi2d 229 . . 3
20 fveq2 5431 . . . . 5
2120dmeqd 4751 . . . . 5
22 fveq2 5431 . . . . . 6
2322imaeq2d 4891 . . . . 5
2420, 21, 23f1oeq123d 5372 . . . 4
2524imbi2d 229 . . 3
26 f1o0 5414 . . . 4
27 ennnfonelemh.dceq . . . . . 6 DECID
28 ennnfonelemh.f . . . . . 6
29 ennnfonelemh.ne . . . . . 6
30 ennnfonelemh.g . . . . . 6
31 ennnfonelemh.n . . . . . 6 frec
32 ennnfonelemh.j . . . . . 6
33 ennnfonelemh.h . . . . . 6
3427, 28, 29, 30, 31, 32, 33ennnfonelem0 11977 . . . . 5
3534dmeqd 4751 . . . . . 6
36 dm0 4763 . . . . . 6
3735, 36eqtrdi 2189 . . . . 5
38 0zd 9113 . . . . . . . . . . . 12
3938, 31frec2uz0d 10226 . . . . . . . . . . 11
4039mptru 1341 . . . . . . . . . 10
4140fveq2i 5434 . . . . . . . . 9
4238, 31frec2uzf1od 10233 . . . . . . . . . . 11
4342mptru 1341 . . . . . . . . . 10
44 peano1 4517 . . . . . . . . . 10
45 f1ocnvfv1 5688 . . . . . . . . . 10
4643, 44, 45mp2an 423 . . . . . . . . 9
4741, 46eqtr3i 2163 . . . . . . . 8
4847imaeq2i 4889 . . . . . . 7
49 ima0 4908 . . . . . . 7
5048, 49eqtri 2161 . . . . . 6
5150a1i 9 . . . . 5
5234, 37, 51f1oeq123d 5372 . . . 4
5326, 52mpbiri 167 . . 3
54 simplr 520 . . . . . . . 8
5527ad2antrr 480 . . . . . . . . . . . 12 DECID
5628ad2antrr 480 . . . . . . . . . . . 12
5729ad2antrr 480 . . . . . . . . . . . 12
58 simplr 520 . . . . . . . . . . . 12
5955, 56, 57, 30, 31, 32, 33, 58ennnfonelemp1 11978 . . . . . . . . . . 11
6059adantr 274 . . . . . . . . . 10
61 simpr 109 . . . . . . . . . . 11
6261iftrued 3487 . . . . . . . . . 10
6360, 62eqtrd 2173 . . . . . . . . 9
6463dmeqd 4751 . . . . . . . . 9
65 0zd 9113 . . . . . . . . . . . . . . . . . 18
6631frechashgf1o 10255 . . . . . . . . . . . . . . . . . . . . 21
6766a1i 9 . . . . . . . . . . . . . . . . . . . 20
68 f1ocnv 5390 . . . . . . . . . . . . . . . . . . . 20
69 f1of 5377 . . . . . . . . . . . . . . . . . . . 20
7067, 68, 693syl 17 . . . . . . . . . . . . . . . . . . 19
7170, 58ffvelrnd 5566 . . . . . . . . . . . . . . . . . 18
7265, 31, 71frec2uzsucd 10228 . . . . . . . . . . . . . . . . 17
73 f1ocnvfv2 5689 . . . . . . . . . . . . . . . . . . 19
7466, 58, 73sylancr 411 . . . . . . . . . . . . . . . . . 18
7574oveq1d 5799 . . . . . . . . . . . . . . . . 17
7672, 75eqtrd 2173 . . . . . . . . . . . . . . . 16
7776fveq2d 5435 . . . . . . . . . . . . . . 15
78 peano2 4518 . . . . . . . . . . . . . . . . 17
7971, 78syl 14 . . . . . . . . . . . . . . . 16
80 f1ocnvfv1 5688 . . . . . . . . . . . . . . . 16
8166, 79, 80sylancr 411 . . . . . . . . . . . . . . 15
8277, 81eqtr3d 2175 . . . . . . . . . . . . . 14
83 df-suc 4302 . . . . . . . . . . . . . 14
8482, 83eqtrdi 2189 . . . . . . . . . . . . 13
8584imaeq2d 4891 . . . . . . . . . . . 12
86 imaundi 4961 . . . . . . . . . . . 12
8785, 86eqtrdi 2189 . . . . . . . . . . 11
8887adantr 274 . . . . . . . . . 10
8961snssd 3674 . . . . . . . . . . . 12
90 ssequn2 3255 . . . . . . . . . . . 12
9189, 90sylib 121 . . . . . . . . . . 11
92 fofn 5357 . . . . . . . . . . . . . . . 16
9356, 92syl 14 . . . . . . . . . . . . . . 15
94 fnsnfv 5490 . . . . . . . . . . . . . . 15
9593, 71, 94syl2anc 409 . . . . . . . . . . . . . 14
9695uneq2d 3236 . . . . . . . . . . . . 13
9796eqeq1d 2149 . . . . . . . . . . . 12
9897adantr 274 . . . . . . . . . . 11
9991, 98mpbid 146 . . . . . . . . . 10
10088, 99eqtrd 2173 . . . . . . . . 9
10163, 64, 100f1oeq123d 5372 . . . . . . . 8
10254, 101mpbird 166 . . . . . . 7
103 simplr 520 . . . . . . . . 9
10455, 56, 57, 30, 31, 32, 33, 58ennnfonelemom 11980 . . . . . . . . . . . 12
105104adantr 274 . . . . . . . . . . 11
106 fof 5355 . . . . . . . . . . . . . 14
10756, 106syl 14 . . . . . . . . . . . . 13
108107, 71ffvelrnd 5566 . . . . . . . . . . . 12
109108adantr 274 . . . . . . . . . . 11
110 f1osng 5418 . . . . . . . . . . 11
111105, 109, 110syl2anc 409 . . . . . . . . . 10
11295adantr 274 . . . . . . . . . . 11
113 f1oeq3 5368 . . . . . . . . . . 11
114112, 113syl 14 . . . . . . . . . 10
115111, 114mpbid 146 . . . . . . . . 9
116 nnord 4535 . . . . . . . . . 10
117 orddisj 4470 . . . . . . . . . 10
118105, 116, 1173syl 17 . . . . . . . . 9
119112ineq2d 3283 . . . . . . . . . 10
120 simpr 109 . . . . . . . . . . 11
121 disjsn 3594 . . . . . . . . . . 11
122120, 121sylibr 133 . . . . . . . . . 10
123119, 122eqtr3d 2175 . . . . . . . . 9
124 f1oun 5397 . . . . . . . . 9
125103, 115, 118, 123, 124syl22anc 1218 . . . . . . . 8
12659adantr 274 . . . . . . . . . 10
127120iffalsed 3490 . . . . . . . . . 10
128126, 127eqtrd 2173 . . . . . . . . 9
12955adantr 274 . . . . . . . . . . 11 DECID
13056adantr 274 . . . . . . . . . . 11
13157adantr 274 . . . . . . . . . . 11
13258adantr 274 . . . . . . . . . . 11
133129, 130, 131, 30, 31, 32, 33, 132, 120ennnfonelemhdmp1 11981 . . . . . . . . . 10
134 df-suc 4302 . . . . . . . . . 10
135133, 134eqtrdi 2189 . . . . . . . . 9
13687adantr 274 . . . . . . . . 9
137128, 135, 136f1oeq123d 5372 . . . . . . . 8
138125, 137mpbird 166 . . . . . . 7
13955, 56, 71ennnfonelemdc 11971 . . . . . . . 8 DECID
140 exmiddc 822 . . . . . . . 8 DECID
141139, 140syl 14 . . . . . . 7
142102, 138, 141mpjaodan 788 . . . . . 6
143142ex 114 . . . . 5
144143expcom 115 . . . 4
145144a2d 26 . . 3
1467, 13, 19, 25, 53, 145nn0ind 9212 . 2
1471, 146mpcom 36 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104   wo 698  DECID wdc 820   wceq 1332   wtru 1333   wcel 1481   wne 2309  wral 2417  wrex 2418   cun 3075   cin 3076   wss 3077  c0 3369  cif 3480  csn 3533  cop 3536   cmpt 3998   word 4293   csuc 4296  com 4513  ccnv 4548   cdm 4549  cima 4552   wfn 5128  wf 5129  wfo 5131  wf1o 5132  cfv 5133  (class class class)co 5784   cmpo 5786  freccfrec 6297   cpm 6553  cc0 7667  c1 7668   caddc 7670   cmin 7980  cn0 9024  cz 9101  cuz 9373   cseq 10272 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 4140  ax-un 4364  ax-setind 4461  ax-iinf 4511  ax-cnex 7758  ax-resscn 7759  ax-1cn 7760  ax-1re 7761  ax-icn 7762  ax-addcl 7763  ax-addrcl 7764  ax-mulcl 7765  ax-addcom 7767  ax-addass 7769  ax-distr 7771  ax-i2m1 7772  ax-0lt1 7773  ax-0id 7775  ax-rnegex 7776  ax-cnre 7778  ax-pre-ltirr 7779  ax-pre-ltwlin 7780  ax-pre-lttrn 7781  ax-pre-ltadd 7783 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 4224  df-iord 4297  df-on 4299  df-ilim 4300  df-suc 4302  df-iom 4514  df-xp 4555  df-rel 4556  df-cnv 4557  df-co 4558  df-dm 4559  df-rn 4560  df-res 4561  df-ima 4562  df-iota 5098  df-fun 5135  df-fn 5136  df-f 5137  df-f1 5138  df-fo 5139  df-f1o 5140  df-fv 5141  df-riota 5740  df-ov 5787  df-oprab 5788  df-mpo 5789  df-1st 6048  df-2nd 6049  df-recs 6212  df-frec 6298  df-pm 6555  df-pnf 7849  df-mnf 7850  df-xr 7851  df-ltxr 7852  df-le 7853  df-sub 7982  df-neg 7983  df-inn 8768  df-n0 9025  df-z 9102  df-uz 9374  df-seqfrec 10273 This theorem is referenced by:  ennnfonelemex  11986  ennnfonelemf1  11990  ennnfonelemrn  11991
 Copyright terms: Public domain W3C validator