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

Theorem nninfself 14765
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 14763 . . . . 5 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ 𝑛 ∈ Ο‰) β†’ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…) ∈ 2o)
3 eqid 2177 . . . . 5 (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)) = (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))
42, 3fmptd 5671 . . . 4 (π‘ž ∈ (2o β†‘π‘š β„•βˆž) β†’ (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)):Ο‰βŸΆ2o)
5 2onn 6522 . . . . . 6 2o ∈ Ο‰
65a1i 9 . . . . 5 (π‘ž ∈ (2o β†‘π‘š β„•βˆž) β†’ 2o ∈ Ο‰)
7 omex 4593 . . . . . 6 Ο‰ ∈ V
87a1i 9 . . . . 5 (π‘ž ∈ (2o β†‘π‘š β„•βˆž) β†’ Ο‰ ∈ V)
96, 8elmapd 6662 . . . 4 (π‘ž ∈ (2o β†‘π‘š β„•βˆž) β†’ ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)) ∈ (2o β†‘π‘š Ο‰) ↔ (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)):Ο‰βŸΆ2o))
104, 9mpbird 167 . . 3 (π‘ž ∈ (2o β†‘π‘š β„•βˆž) β†’ (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)) ∈ (2o β†‘π‘š Ο‰))
11 nninfsellemsuc 14764 . . . . 5 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ 𝑗 ∈ Ο‰) β†’ if(βˆ€π‘˜ ∈ suc suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…) βŠ† if(βˆ€π‘˜ ∈ suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))
12 peano2 4595 . . . . . 6 (𝑗 ∈ Ο‰ β†’ suc 𝑗 ∈ Ο‰)
13 nninfsellemcl 14763 . . . . . . 7 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ suc 𝑗 ∈ Ο‰) β†’ if(βˆ€π‘˜ ∈ suc suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…) ∈ 2o)
1412, 13sylan2 286 . . . . . 6 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ 𝑗 ∈ Ο‰) β†’ if(βˆ€π‘˜ ∈ suc suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…) ∈ 2o)
15 suceq 4403 . . . . . . . . 9 (𝑛 = suc 𝑗 β†’ suc 𝑛 = suc suc 𝑗)
1615raleqdv 2679 . . . . . . . 8 (𝑛 = suc 𝑗 β†’ (βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o ↔ βˆ€π‘˜ ∈ suc suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o))
1716ifbid 3556 . . . . . . 7 (𝑛 = suc 𝑗 β†’ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…) = if(βˆ€π‘˜ ∈ suc suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))
1817, 3fvmptg 5593 . . . . . 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 594 . . . . 5 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ 𝑗 ∈ Ο‰) β†’ ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜suc 𝑗) = if(βˆ€π‘˜ ∈ suc suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))
20 simpr 110 . . . . . 6 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ 𝑗 ∈ Ο‰) β†’ 𝑗 ∈ Ο‰)
21 nninfsellemcl 14763 . . . . . 6 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ 𝑗 ∈ Ο‰) β†’ if(βˆ€π‘˜ ∈ suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…) ∈ 2o)
22 suceq 4403 . . . . . . . . 9 (𝑛 = 𝑗 β†’ suc 𝑛 = suc 𝑗)
2322raleqdv 2679 . . . . . . . 8 (𝑛 = 𝑗 β†’ (βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o ↔ βˆ€π‘˜ ∈ suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o))
2423ifbid 3556 . . . . . . 7 (𝑛 = 𝑗 β†’ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…) = if(βˆ€π‘˜ ∈ suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))
2524, 3fvmptg 5593 . . . . . 6 ((𝑗 ∈ Ο‰ ∧ if(βˆ€π‘˜ ∈ suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…) ∈ 2o) β†’ ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜π‘—) = if(βˆ€π‘˜ ∈ suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))
2620, 21, 25syl2anc 411 . . . . 5 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ 𝑗 ∈ Ο‰) β†’ ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜π‘—) = if(βˆ€π‘˜ ∈ suc 𝑗(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))
2711, 19, 263sstr4d 3201 . . . 4 ((π‘ž ∈ (2o β†‘π‘š β„•βˆž) ∧ 𝑗 ∈ Ο‰) β†’ ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜suc 𝑗) βŠ† ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜π‘—))
2827ralrimiva 2550 . . 3 (π‘ž ∈ (2o β†‘π‘š β„•βˆž) β†’ βˆ€π‘— ∈ Ο‰ ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜suc 𝑗) βŠ† ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜π‘—))
29 fveq1 5515 . . . . . 6 (𝑓 = (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)) β†’ (π‘“β€˜suc 𝑗) = ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜suc 𝑗))
30 fveq1 5515 . . . . . 6 (𝑓 = (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)) β†’ (π‘“β€˜π‘—) = ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜π‘—))
3129, 30sseq12d 3187 . . . . 5 (𝑓 = (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)) β†’ ((π‘“β€˜suc 𝑗) βŠ† (π‘“β€˜π‘—) ↔ ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜suc 𝑗) βŠ† ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜π‘—)))
3231ralbidv 2477 . . . 4 (𝑓 = (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)) β†’ (βˆ€π‘— ∈ Ο‰ (π‘“β€˜suc 𝑗) βŠ† (π‘“β€˜π‘—) ↔ βˆ€π‘— ∈ Ο‰ ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜suc 𝑗) βŠ† ((𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…))β€˜π‘—)))
33 df-nninf 7119 . . . 4 β„•βˆž = {𝑓 ∈ (2o β†‘π‘š Ο‰) ∣ βˆ€π‘— ∈ Ο‰ (π‘“β€˜suc 𝑗) βŠ† (π‘“β€˜π‘—)}
3432, 33elrab2 2897 . . 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 417 . 2 (π‘ž ∈ (2o β†‘π‘š β„•βˆž) β†’ (𝑛 ∈ Ο‰ ↦ if(βˆ€π‘˜ ∈ suc 𝑛(π‘žβ€˜(𝑖 ∈ Ο‰ ↦ if(𝑖 ∈ π‘˜, 1o, βˆ…))) = 1o, 1o, βˆ…)) ∈ β„•βˆž)
361, 35fmpti 5669 1 𝐸:(2o β†‘π‘š β„•βˆž)βŸΆβ„•βˆž
Colors of variables: wff set class
Syntax hints:   ∧ wa 104   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455  Vcvv 2738   βŠ† wss 3130  βˆ…c0 3423  ifcif 3535   ↦ cmpt 4065  suc csuc 4366  Ο‰com 4590  βŸΆwf 5213  β€˜cfv 5217  (class class class)co 5875  1oc1o 6410  2oc2o 6411   β†‘π‘š cmap 6648  β„•βˆžxnninf 7118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-nul 4130  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537  ax-iinf 4588
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2740  df-sbc 2964  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-if 3536  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-br 4005  df-opab 4066  df-mpt 4067  df-tr 4103  df-id 4294  df-iord 4367  df-on 4369  df-suc 4372  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1o 6417  df-2o 6418  df-map 6650  df-nninf 7119
This theorem is referenced by:  nninfsellemeq  14766  nninfsellemeqinf  14768  nninfomnilem  14770
  Copyright terms: Public domain W3C validator