Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  nninfself GIF version

Theorem nninfself 13548
 Description: Domain and range of the selection function for ℕ∞. (Contributed by Jim Kingdon, 6-Aug-2022.)
Hypothesis
Ref Expression
nninfsel.e 𝐸 = (𝑞 ∈ (2o𝑚) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)))
Assertion
Ref Expression
nninfself 𝐸:(2o𝑚)⟶ℕ
Distinct variable groups:   𝑖,𝑘,𝑛   𝑘,𝑞,𝑛
Allowed substitution hints:   𝐸(𝑖,𝑘,𝑛,𝑞)

Proof of Theorem nninfself
Dummy variables 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nninfsel.e . 2 𝐸 = (𝑞 ∈ (2o𝑚) ↦ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)))
2 nninfsellemcl 13546 . . . . 5 ((𝑞 ∈ (2o𝑚) ∧ 𝑛 ∈ ω) → if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ∈ 2o)
3 eqid 2157 . . . . 5 (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))
42, 3fmptd 5618 . . . 4 (𝑞 ∈ (2o𝑚) → (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)):ω⟶2o)
5 2onn 6461 . . . . . 6 2o ∈ ω
65a1i 9 . . . . 5 (𝑞 ∈ (2o𝑚) → 2o ∈ ω)
7 omex 4550 . . . . . 6 ω ∈ V
87a1i 9 . . . . 5 (𝑞 ∈ (2o𝑚) → ω ∈ V)
96, 8elmapd 6600 . . . 4 (𝑞 ∈ (2o𝑚) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) ∈ (2o𝑚 ω) ↔ (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)):ω⟶2o))
104, 9mpbird 166 . . 3 (𝑞 ∈ (2o𝑚) → (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) ∈ (2o𝑚 ω))
11 nninfsellemsuc 13547 . . . . 5 ((𝑞 ∈ (2o𝑚) ∧ 𝑗 ∈ ω) → if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ⊆ if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))
12 peano2 4552 . . . . . 6 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
13 nninfsellemcl 13546 . . . . . . 7 ((𝑞 ∈ (2o𝑚) ∧ suc 𝑗 ∈ ω) → if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ∈ 2o)
1412, 13sylan2 284 . . . . . 6 ((𝑞 ∈ (2o𝑚) ∧ 𝑗 ∈ ω) → if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ∈ 2o)
15 suceq 4361 . . . . . . . . 9 (𝑛 = suc 𝑗 → suc 𝑛 = suc suc 𝑗)
1615raleqdv 2658 . . . . . . . 8 (𝑛 = suc 𝑗 → (∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o ↔ ∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o))
1716ifbid 3526 . . . . . . 7 (𝑛 = suc 𝑗 → if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) = if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))
1817, 3fvmptg 5541 . . . . . 6 ((suc 𝑗 ∈ ω ∧ if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ∈ 2o) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘suc 𝑗) = if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))
1912, 14, 18syl2an2 584 . . . . 5 ((𝑞 ∈ (2o𝑚) ∧ 𝑗 ∈ ω) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘suc 𝑗) = if(∀𝑘 ∈ suc suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))
20 simpr 109 . . . . . 6 ((𝑞 ∈ (2o𝑚) ∧ 𝑗 ∈ ω) → 𝑗 ∈ ω)
21 nninfsellemcl 13546 . . . . . 6 ((𝑞 ∈ (2o𝑚) ∧ 𝑗 ∈ ω) → if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ∈ 2o)
22 suceq 4361 . . . . . . . . 9 (𝑛 = 𝑗 → suc 𝑛 = suc 𝑗)
2322raleqdv 2658 . . . . . . . 8 (𝑛 = 𝑗 → (∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o ↔ ∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o))
2423ifbid 3526 . . . . . . 7 (𝑛 = 𝑗 → if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) = if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))
2524, 3fvmptg 5541 . . . . . 6 ((𝑗 ∈ ω ∧ if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅) ∈ 2o) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘𝑗) = if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))
2620, 21, 25syl2anc 409 . . . . 5 ((𝑞 ∈ (2o𝑚) ∧ 𝑗 ∈ ω) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘𝑗) = if(∀𝑘 ∈ suc 𝑗(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))
2711, 19, 263sstr4d 3173 . . . 4 ((𝑞 ∈ (2o𝑚) ∧ 𝑗 ∈ ω) → ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘𝑗))
2827ralrimiva 2530 . . 3 (𝑞 ∈ (2o𝑚) → ∀𝑗 ∈ ω ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘𝑗))
29 fveq1 5464 . . . . . 6 (𝑓 = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) → (𝑓‘suc 𝑗) = ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘suc 𝑗))
30 fveq1 5464 . . . . . 6 (𝑓 = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) → (𝑓𝑗) = ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘𝑗))
3129, 30sseq12d 3159 . . . . 5 (𝑓 = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘𝑗)))
3231ralbidv 2457 . . . 4 (𝑓 = (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘𝑗)))
33 df-nninf 7054 . . . 4 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
3432, 33elrab2 2871 . . 3 ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) ∈ ℕ ↔ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘suc 𝑗) ⊆ ((𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅))‘𝑗)))
3510, 28, 34sylanbrc 414 . 2 (𝑞 ∈ (2o𝑚) → (𝑛 ∈ ω ↦ if(∀𝑘 ∈ suc 𝑛(𝑞‘(𝑖 ∈ ω ↦ if(𝑖𝑘, 1o, ∅))) = 1o, 1o, ∅)) ∈ ℕ)
361, 35fmpti 5616 1 𝐸:(2o𝑚)⟶ℕ
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   = wceq 1335   ∈ wcel 2128  ∀wral 2435  Vcvv 2712   ⊆ wss 3102  ∅c0 3394  ifcif 3505   ↦ cmpt 4025  suc csuc 4324  ωcom 4547  ⟶wf 5163  ‘cfv 5167  (class class class)co 5818  1oc1o 6350  2oc2o 6351   ↑𝑚 cmap 6586  ℕ∞xnninf 7053 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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4252  df-iord 4325  df-on 4327  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1o 6357  df-2o 6358  df-map 6588  df-nninf 7054 This theorem is referenced by:  nninfsellemeq  13549  nninfsellemeqinf  13551  nninfomnilem  13553
 Copyright terms: Public domain W3C validator