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

Theorem hashennn 10647
 Description: The size of a set equinumerous to an element of ω. (Contributed by Jim Kingdon, 21-Feb-2022.)
Assertion
Ref Expression
hashennn ((𝑁 ∈ ω ∧ 𝑁𝐴) → (♯‘𝐴) = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)‘𝑁))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑁

Proof of Theorem hashennn
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ihash 10643 . . . . 5 ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
21fveq1i 5468 . . . 4 (♯‘𝐴) = (((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))‘𝐴)
3 funmpt 5207 . . . . 5 Fun (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})
4 hashennnuni 10646 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑁𝐴) → {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴} = 𝑁)
54eqcomd 2163 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑁𝐴) → 𝑁 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴})
6 nnfi 6814 . . . . . . . . . . 11 (𝑁 ∈ ω → 𝑁 ∈ Fin)
76adantr 274 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑁𝐴) → 𝑁 ∈ Fin)
8 simpr 109 . . . . . . . . . . 11 ((𝑁 ∈ ω ∧ 𝑁𝐴) → 𝑁𝐴)
98ensymd 6725 . . . . . . . . . 10 ((𝑁 ∈ ω ∧ 𝑁𝐴) → 𝐴𝑁)
10 enfii 6816 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝐴𝑁) → 𝐴 ∈ Fin)
117, 9, 10syl2anc 409 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑁𝐴) → 𝐴 ∈ Fin)
12 simpl 108 . . . . . . . . 9 ((𝑁 ∈ ω ∧ 𝑁𝐴) → 𝑁 ∈ ω)
13 simpr 109 . . . . . . . . . . 11 ((𝑥 = 𝐴𝑧 = 𝑁) → 𝑧 = 𝑁)
14 breq2 3969 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (𝑦𝑥𝑦𝐴))
1514adantr 274 . . . . . . . . . . . . 13 ((𝑥 = 𝐴𝑧 = 𝑁) → (𝑦𝑥𝑦𝐴))
1615rabbidv 2701 . . . . . . . . . . . 12 ((𝑥 = 𝐴𝑧 = 𝑁) → {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥} = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴})
1716unieqd 3783 . . . . . . . . . . 11 ((𝑥 = 𝐴𝑧 = 𝑁) → {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥} = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴})
1813, 17eqeq12d 2172 . . . . . . . . . 10 ((𝑥 = 𝐴𝑧 = 𝑁) → (𝑧 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥} ↔ 𝑁 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴}))
1918opelopabga 4223 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝑁 ∈ ω) → (⟨𝐴, 𝑁⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ 𝑧 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}} ↔ 𝑁 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴}))
2011, 12, 19syl2anc 409 . . . . . . . 8 ((𝑁 ∈ ω ∧ 𝑁𝐴) → (⟨𝐴, 𝑁⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ 𝑧 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}} ↔ 𝑁 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴}))
215, 20mpbird 166 . . . . . . 7 ((𝑁 ∈ ω ∧ 𝑁𝐴) → ⟨𝐴, 𝑁⟩ ∈ {⟨𝑥, 𝑧⟩ ∣ 𝑧 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}})
22 mptv 4061 . . . . . . 7 (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}) = {⟨𝑥, 𝑧⟩ ∣ 𝑧 = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}}
2321, 22eleqtrrdi 2251 . . . . . 6 ((𝑁 ∈ ω ∧ 𝑁𝐴) → ⟨𝐴, 𝑁⟩ ∈ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
24 opeldmg 4790 . . . . . . 7 ((𝐴 ∈ Fin ∧ 𝑁 ∈ ω) → (⟨𝐴, 𝑁⟩ ∈ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}) → 𝐴 ∈ dom (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})))
2511, 12, 24syl2anc 409 . . . . . 6 ((𝑁 ∈ ω ∧ 𝑁𝐴) → (⟨𝐴, 𝑁⟩ ∈ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}) → 𝐴 ∈ dom (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})))
2623, 25mpd 13 . . . . 5 ((𝑁 ∈ ω ∧ 𝑁𝐴) → 𝐴 ∈ dom (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))
27 fvco 5537 . . . . 5 ((Fun (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}) ∧ 𝐴 ∈ dom (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})) → (((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))‘𝐴) = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘((𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})‘𝐴)))
283, 26, 27sylancr 411 . . . 4 ((𝑁 ∈ ω ∧ 𝑁𝐴) → (((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}))‘𝐴) = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘((𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})‘𝐴)))
292, 28syl5eq 2202 . . 3 ((𝑁 ∈ ω ∧ 𝑁𝐴) → (♯‘𝐴) = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘((𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})‘𝐴)))
3011elexd 2725 . . . . . 6 ((𝑁 ∈ ω ∧ 𝑁𝐴) → 𝐴 ∈ V)
314, 12eqeltrd 2234 . . . . . 6 ((𝑁 ∈ ω ∧ 𝑁𝐴) → {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴} ∈ ω)
3214rabbidv 2701 . . . . . . . 8 (𝑥 = 𝐴 → {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥} = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴})
3332unieqd 3783 . . . . . . 7 (𝑥 = 𝐴 {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥} = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴})
34 eqid 2157 . . . . . . 7 (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥}) = (𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})
3533, 34fvmptg 5543 . . . . . 6 ((𝐴 ∈ V ∧ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴} ∈ ω) → ((𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})‘𝐴) = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴})
3630, 31, 35syl2anc 409 . . . . 5 ((𝑁 ∈ ω ∧ 𝑁𝐴) → ((𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})‘𝐴) = {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝐴})
3736, 4eqtrd 2190 . . . 4 ((𝑁 ∈ ω ∧ 𝑁𝐴) → ((𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})‘𝐴) = 𝑁)
3837fveq2d 5471 . . 3 ((𝑁 ∈ ω ∧ 𝑁𝐴) → ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘((𝑥 ∈ V ↦ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦𝑥})‘𝐴)) = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘𝑁))
3929, 38eqtrd 2190 . 2 ((𝑁 ∈ ω ∧ 𝑁𝐴) → (♯‘𝐴) = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘𝑁))
40 ordom 4565 . . . . . . 7 Ord ω
41 ordirr 4500 . . . . . . 7 (Ord ω → ¬ ω ∈ ω)
4240, 41ax-mp 5 . . . . . 6 ¬ ω ∈ ω
43 eleq1 2220 . . . . . 6 (ω = 𝑁 → (ω ∈ ω ↔ 𝑁 ∈ ω))
4442, 43mtbii 664 . . . . 5 (ω = 𝑁 → ¬ 𝑁 ∈ ω)
4544necon2ai 2381 . . . 4 (𝑁 ∈ ω → ω ≠ 𝑁)
46 fvunsng 5660 . . . 4 ((𝑁 ∈ ω ∧ ω ≠ 𝑁) → ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘𝑁) = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)‘𝑁))
4745, 46mpdan 418 . . 3 (𝑁 ∈ ω → ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘𝑁) = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)‘𝑁))
4847adantr 274 . 2 ((𝑁 ∈ ω ∧ 𝑁𝐴) → ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩})‘𝑁) = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)‘𝑁))
4939, 48eqtrd 2190 1 ((𝑁 ∈ ω ∧ 𝑁𝐴) → (♯‘𝐴) = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)‘𝑁))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1335   ∈ wcel 2128   ≠ wne 2327  {crab 2439  Vcvv 2712   ∪ cun 3100  {csn 3560  ⟨cop 3563  ∪ cuni 3772   class class class wbr 3965  {copab 4024   ↦ cmpt 4025  Ord word 4322  ωcom 4548  dom cdm 4585   ∘ ccom 4589  Fun wfun 5163  ‘cfv 5169  (class class class)co 5821  freccfrec 6334   ≈ cen 6680   ≼ cdom 6681  Fincfn 6682  0cc0 7726  1c1 7727   + caddc 7729  +∞cpnf 7903  ℤcz 9161  ♯chash 10642 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 4135  ax-pr 4169  ax-un 4393  ax-setind 4495  ax-iinf 4546 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-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 4253  df-iord 4326  df-on 4328  df-suc 4331  df-iom 4549  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-fv 5177  df-er 6477  df-en 6683  df-dom 6684  df-fin 6685  df-ihash 10643 This theorem is referenced by:  hashcl  10648  hashfz1  10650  hashen  10651  fihashdom  10670  hashun  10672
 Copyright terms: Public domain W3C validator