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

Theorem ennnfonelemrn 12004
 Description: Lemma for ennnfone 12010. 𝐿 is onto 𝐴. (Contributed by Jim Kingdon, 16-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
ennnfonelemh.f (𝜑𝐹:ω–onto𝐴)
ennnfonelemh.ne (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
ennnfonelemh.g 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))
ennnfonelemh.n 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
ennnfonelemh.j 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
ennnfonelemh.h 𝐻 = seq0(𝐺, 𝐽)
ennnfone.l 𝐿 = 𝑖 ∈ ℕ0 (𝐻𝑖)
Assertion
Ref Expression
ennnfonelemrn (𝜑 → ran 𝐿 = 𝐴)
Distinct variable groups:   𝐴,𝑗,𝑥,𝑦   𝑖,𝐹,𝑗,𝑥,𝑦,𝑘   𝑛,𝐹,𝑘   𝑗,𝐺   𝑖,𝐻,𝑗,𝑥,𝑦,𝑘   𝑗,𝐽   𝑖,𝑁,𝑗,𝑥,𝑦,𝑘   𝜑,𝑖,𝑗,𝑥,𝑦,𝑘   𝑗,𝑛
Allowed substitution hints:   𝜑(𝑛)   𝐴(𝑖,𝑘,𝑛)   𝐺(𝑥,𝑦,𝑖,𝑘,𝑛)   𝐻(𝑛)   𝐽(𝑥,𝑦,𝑖,𝑘,𝑛)   𝐿(𝑥,𝑦,𝑖,𝑗,𝑘,𝑛)   𝑁(𝑛)

Proof of Theorem ennnfonelemrn
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 ennnfonelemh.dceq . . . 4 (𝜑 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
2 ennnfonelemh.f . . . 4 (𝜑𝐹:ω–onto𝐴)
3 ennnfonelemh.ne . . . 4 (𝜑 → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
4 ennnfonelemh.g . . . 4 𝐺 = (𝑥 ∈ (𝐴pm ω), 𝑦 ∈ ω ↦ if((𝐹𝑦) ∈ (𝐹𝑦), 𝑥, (𝑥 ∪ {⟨dom 𝑥, (𝐹𝑦)⟩})))
5 ennnfonelemh.n . . . 4 𝑁 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)
6 ennnfonelemh.j . . . 4 𝐽 = (𝑥 ∈ ℕ0 ↦ if(𝑥 = 0, ∅, (𝑁‘(𝑥 − 1))))
7 ennnfonelemh.h . . . 4 𝐻 = seq0(𝐺, 𝐽)
8 ennnfone.l . . . 4 𝐿 = 𝑖 ∈ ℕ0 (𝐻𝑖)
91, 2, 3, 4, 5, 6, 7, 8ennnfonelemf1 12003 . . 3 (𝜑𝐿:dom 𝐿1-1𝐴)
10 f1f 5340 . . 3 (𝐿:dom 𝐿1-1𝐴𝐿:dom 𝐿𝐴)
11 frn 5293 . . 3 (𝐿:dom 𝐿𝐴 → ran 𝐿𝐴)
129, 10, 113syl 17 . 2 (𝜑 → ran 𝐿𝐴)
13 foelrn 5666 . . . . . 6 ((𝐹:ω–onto𝐴𝑤𝐴) → ∃𝑗 ∈ ω 𝑤 = (𝐹𝑗))
142, 13sylan 281 . . . . 5 ((𝜑𝑤𝐴) → ∃𝑗 ∈ ω 𝑤 = (𝐹𝑗))
15 0zd 9119 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → 0 ∈ ℤ)
16 simprl 521 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → 𝑗 ∈ ω)
17 peano2 4520 . . . . . . . . 9 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
1816, 17syl 14 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → suc 𝑗 ∈ ω)
1915, 5, 18frec2uzuzd 10235 . . . . . . 7 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → (𝑁‘suc 𝑗) ∈ (ℤ‘0))
20 nn0uz 9413 . . . . . . 7 0 = (ℤ‘0)
2119, 20eleqtrrdi 2235 . . . . . 6 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → (𝑁‘suc 𝑗) ∈ ℕ0)
22 fofn 5359 . . . . . . . . . 10 (𝐹:ω–onto𝐴𝐹 Fn ω)
232, 22syl 14 . . . . . . . . 9 (𝜑𝐹 Fn ω)
2423ad2antrr 480 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → 𝐹 Fn ω)
25 ordom 4532 . . . . . . . . 9 Ord ω
26 ordsucss 4431 . . . . . . . . 9 (Ord ω → (𝑗 ∈ ω → suc 𝑗 ⊆ ω))
2725, 16, 26mpsyl 65 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → suc 𝑗 ⊆ ω)
28 vex 2694 . . . . . . . . . 10 𝑗 ∈ V
2928sucid 4350 . . . . . . . . 9 𝑗 ∈ suc 𝑗
3029a1i 9 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → 𝑗 ∈ suc 𝑗)
31 fnfvima 5664 . . . . . . . 8 ((𝐹 Fn ω ∧ suc 𝑗 ⊆ ω ∧ 𝑗 ∈ suc 𝑗) → (𝐹𝑗) ∈ (𝐹 “ suc 𝑗))
3224, 27, 30, 31syl3anc 1217 . . . . . . 7 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → (𝐹𝑗) ∈ (𝐹 “ suc 𝑗))
33 simprr 522 . . . . . . 7 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → 𝑤 = (𝐹𝑗))
3415, 5frec2uzf1od 10239 . . . . . . . . 9 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → 𝑁:ω–1-1-onto→(ℤ‘0))
35 f1ocnvfv1 5690 . . . . . . . . 9 ((𝑁:ω–1-1-onto→(ℤ‘0) ∧ suc 𝑗 ∈ ω) → (𝑁‘(𝑁‘suc 𝑗)) = suc 𝑗)
3634, 18, 35syl2anc 409 . . . . . . . 8 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → (𝑁‘(𝑁‘suc 𝑗)) = suc 𝑗)
3736imaeq2d 4893 . . . . . . 7 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → (𝐹 “ (𝑁‘(𝑁‘suc 𝑗))) = (𝐹 “ suc 𝑗))
3832, 33, 373eltr4d 2225 . . . . . 6 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → 𝑤 ∈ (𝐹 “ (𝑁‘(𝑁‘suc 𝑗))))
39 fveq2 5433 . . . . . . . . 9 (𝑖 = (𝑁‘suc 𝑗) → (𝑁𝑖) = (𝑁‘(𝑁‘suc 𝑗)))
4039imaeq2d 4893 . . . . . . . 8 (𝑖 = (𝑁‘suc 𝑗) → (𝐹 “ (𝑁𝑖)) = (𝐹 “ (𝑁‘(𝑁‘suc 𝑗))))
4140eleq2d 2211 . . . . . . 7 (𝑖 = (𝑁‘suc 𝑗) → (𝑤 ∈ (𝐹 “ (𝑁𝑖)) ↔ 𝑤 ∈ (𝐹 “ (𝑁‘(𝑁‘suc 𝑗)))))
4241rspcev 2795 . . . . . 6 (((𝑁‘suc 𝑗) ∈ ℕ0𝑤 ∈ (𝐹 “ (𝑁‘(𝑁‘suc 𝑗)))) → ∃𝑖 ∈ ℕ0 𝑤 ∈ (𝐹 “ (𝑁𝑖)))
4321, 38, 42syl2anc 409 . . . . 5 (((𝜑𝑤𝐴) ∧ (𝑗 ∈ ω ∧ 𝑤 = (𝐹𝑗))) → ∃𝑖 ∈ ℕ0 𝑤 ∈ (𝐹 “ (𝑁𝑖)))
4414, 43rexlimddv 2559 . . . 4 ((𝜑𝑤𝐴) → ∃𝑖 ∈ ℕ0 𝑤 ∈ (𝐹 “ (𝑁𝑖)))
45 eliun 3827 . . . 4 (𝑤 𝑖 ∈ ℕ0 (𝐹 “ (𝑁𝑖)) ↔ ∃𝑖 ∈ ℕ0 𝑤 ∈ (𝐹 “ (𝑁𝑖)))
4644, 45sylibr 133 . . 3 ((𝜑𝑤𝐴) → 𝑤 𝑖 ∈ ℕ0 (𝐹 “ (𝑁𝑖)))
478rneqi 4779 . . . . . . 7 ran 𝐿 = ran 𝑖 ∈ ℕ0 (𝐻𝑖)
48 rniun 4961 . . . . . . 7 ran 𝑖 ∈ ℕ0 (𝐻𝑖) = 𝑖 ∈ ℕ0 ran (𝐻𝑖)
4947, 48eqtri 2162 . . . . . 6 ran 𝐿 = 𝑖 ∈ ℕ0 ran (𝐻𝑖)
501adantr 274 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ0) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
512adantr 274 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ0) → 𝐹:ω–onto𝐴)
523adantr 274 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ0) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ∀𝑗 ∈ suc 𝑛(𝐹𝑘) ≠ (𝐹𝑗))
53 simpr 109 . . . . . . . . 9 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
5450, 51, 52, 4, 5, 6, 7, 53ennnfonelemhf1o 11998 . . . . . . . 8 ((𝜑𝑖 ∈ ℕ0) → (𝐻𝑖):dom (𝐻𝑖)–1-1-onto→(𝐹 “ (𝑁𝑖)))
55 f1ofo 5386 . . . . . . . 8 ((𝐻𝑖):dom (𝐻𝑖)–1-1-onto→(𝐹 “ (𝑁𝑖)) → (𝐻𝑖):dom (𝐻𝑖)–onto→(𝐹 “ (𝑁𝑖)))
56 forn 5360 . . . . . . . 8 ((𝐻𝑖):dom (𝐻𝑖)–onto→(𝐹 “ (𝑁𝑖)) → ran (𝐻𝑖) = (𝐹 “ (𝑁𝑖)))
5754, 55, 563syl 17 . . . . . . 7 ((𝜑𝑖 ∈ ℕ0) → ran (𝐻𝑖) = (𝐹 “ (𝑁𝑖)))
5857iuneq2dv 3844 . . . . . 6 (𝜑 𝑖 ∈ ℕ0 ran (𝐻𝑖) = 𝑖 ∈ ℕ0 (𝐹 “ (𝑁𝑖)))
5949, 58syl5eq 2186 . . . . 5 (𝜑 → ran 𝐿 = 𝑖 ∈ ℕ0 (𝐹 “ (𝑁𝑖)))
6059eleq2d 2211 . . . 4 (𝜑 → (𝑤 ∈ ran 𝐿𝑤 𝑖 ∈ ℕ0 (𝐹 “ (𝑁𝑖))))
6160adantr 274 . . 3 ((𝜑𝑤𝐴) → (𝑤 ∈ ran 𝐿𝑤 𝑖 ∈ ℕ0 (𝐹 “ (𝑁𝑖))))
6246, 61mpbird 166 . 2 ((𝜑𝑤𝐴) → 𝑤 ∈ ran 𝐿)
6312, 62eqelssd 3123 1 (𝜑 → ran 𝐿 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 820   = wceq 1332   ∈ wcel 1481   ≠ wne 2310  ∀wral 2418  ∃wrex 2419   ∪ cun 3076   ⊆ wss 3078  ∅c0 3370  ifcif 3481  {csn 3534  ⟨cop 3537  ∪ ciun 3823   ↦ cmpt 3999  Ord word 4295  suc csuc 4298  ωcom 4515  ◡ccnv 4550  dom cdm 4551  ran crn 4552   “ cima 4554   Fn wfn 5130  ⟶wf 5131  –1-1→wf1 5132  –onto→wfo 5133  –1-1-onto→wf1o 5134  ‘cfv 5135  (class class class)co 5786   ∈ cmpo 5788  freccfrec 6299   ↑pm cpm 6555  0cc0 7673  1c1 7674   + caddc 7676   − cmin 7986  ℕ0cn0 9030  ℤcz 9107  ℤ≥cuz 9379  seqcseq 10278 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 2123  ax-coll 4053  ax-sep 4056  ax-nul 4064  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463  ax-iinf 4513  ax-cnex 7764  ax-resscn 7765  ax-1cn 7766  ax-1re 7767  ax-icn 7768  ax-addcl 7769  ax-addrcl 7770  ax-mulcl 7771  ax-addcom 7773  ax-addass 7775  ax-distr 7777  ax-i2m1 7778  ax-0lt1 7779  ax-0id 7781  ax-rnegex 7782  ax-cnre 7784  ax-pre-ltirr 7785  ax-pre-ltwlin 7786  ax-pre-lttrn 7787  ax-pre-ltadd 7789 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 1738  df-eu 2004  df-mo 2005  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-nel 2406  df-ral 2423  df-rex 2424  df-reu 2425  df-rab 2427  df-v 2693  df-sbc 2916  df-csb 3010  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-nul 3371  df-if 3482  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-int 3782  df-iun 3825  df-br 3940  df-opab 4000  df-mpt 4001  df-tr 4037  df-id 4226  df-iord 4299  df-on 4301  df-ilim 4302  df-suc 4304  df-iom 4516  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-f1 5140  df-fo 5141  df-f1o 5142  df-fv 5143  df-riota 5742  df-ov 5789  df-oprab 5790  df-mpo 5791  df-1st 6050  df-2nd 6051  df-recs 6214  df-frec 6300  df-pm 6557  df-pnf 7855  df-mnf 7856  df-xr 7857  df-ltxr 7858  df-le 7859  df-sub 7988  df-neg 7989  df-inn 8774  df-n0 9031  df-z 9108  df-uz 9380  df-seqfrec 10279 This theorem is referenced by:  ennnfonelemen  12006
 Copyright terms: Public domain W3C validator