Theorem eulerpartlem1 31625

Description: Lemma for eulerpart 31640. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)

Hypotheses

Ref	Expression
eulerpart.p	⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
eulerpart.o	⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d	⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
eulerpart.j	⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f	⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
eulerpart.h	⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m	⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})

Assertion

Ref	Expression
eulerpartlem1	⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)

Distinct variable groups:   𝑥,𝑟,𝑦,𝐽   𝐻,𝑟

Allowed substitution hints:   𝐷(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛)   𝐽(𝑧,𝑓,𝑔,𝑘,𝑛)   𝑀(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑁(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑂(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)

Proof of Theorem eulerpartlem1

Step	Hyp	Ref	Expression
1		eulerpart.j	. . . 4 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
2		nnex 11644	. . . 4 ⊢ ℕ ∈ V
3	1, 2	rabex2 5237	. . 3 ⊢ 𝐽 ∈ V
4		nn0ex 11904	. . 3 ⊢ ℕ0 ∈ V
5		eqid 2821	. . 3 ⊢ (𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) = (𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
6		eulerpart.h	. . 3 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
7	3, 4, 5, 6	fpwrelmapffs 30470	. 2 ⊢ ((𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ↾ 𝐻):𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)
8		eulerpart.m	. . . 4 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
9		ssrab2 4056	. . . . . . 7 ⊢ {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ⊆ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽)
10	4	pwex 5281	. . . . . . . 8 ⊢ 𝒫 ℕ0 ∈ V
11		inss1 4205	. . . . . . . 8 ⊢ (𝒫 ℕ0 ∩ Fin) ⊆ 𝒫 ℕ0
12		mapss 8453	. . . . . . . 8 ⊢ ((𝒫 ℕ0 ∈ V ∧ (𝒫 ℕ0 ∩ Fin) ⊆ 𝒫 ℕ0) → ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ⊆ (𝒫 ℕ0 ↑m 𝐽))
13	10, 11, 12	mp2an 690	. . . . . . 7 ⊢ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ⊆ (𝒫 ℕ0 ↑m 𝐽)
14	9, 13	sstri 3976	. . . . . 6 ⊢ {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin} ⊆ (𝒫 ℕ0 ↑m 𝐽)
15	6, 14	eqsstri 4001	. . . . 5 ⊢ 𝐻 ⊆ (𝒫 ℕ0 ↑m 𝐽)
16		resmpt 5905	. . . . 5 ⊢ (𝐻 ⊆ (𝒫 ℕ0 ↑m 𝐽) → ((𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ↾ 𝐻) = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}))
17	15, 16	ax-mp 5	. . . 4 ⊢ ((𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ↾ 𝐻) = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
18	8, 17	eqtr4i 2847	. . 3 ⊢ 𝑀 = ((𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ↾ 𝐻)
19		f1oeq1 6604	. . 3 ⊢ (𝑀 = ((𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ↾ 𝐻) → (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ ((𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ↾ 𝐻):𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)))
20	18, 19	ax-mp 5	. 2 ⊢ (𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin) ↔ ((𝑟 ∈ (𝒫 ℕ0 ↑m 𝐽) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))}) ↾ 𝐻):𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin))
21	7, 20	mpbir 233	1 ⊢ 𝑀:𝐻–1-1-onto→(𝒫 (𝐽 × ℕ0) ∩ Fin)

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  {crab 3142  Vcvv 3494   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539   class class class wbr 5066  {copab 5128   ↦ cmpt 5146   × cxp 5553  ^◡ccnv 5554   ↾ cres 5557   “ cima 5558  –1-1-onto→wf1o 6354  ‘cfv 6355  (class class class)co 7156   ∈ cmpo 7158   supp csupp 7830   ↑_m cmap 8406  Fincfn 8509  1c1 10538   · cmul 10542   ≤ cle 10676  ℕcn 11638  2c2 11693  ℕ₀cn0 11898  ↑cexp 13430  Σcsu 15042   ∥ cdvds 15607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-ac2 9885  ax-cnex 10593  ax-1cn 10595  ax-addcl 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-se 5515  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-isom 6364  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-supp 7831  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-oadd 8106  df-er 8289  df-map 8408  df-en 8510  df-dom 8511  df-fin 8513  df-card 9368  df-acn 9371  df-ac 9542  df-nn 11639  df-n0 11899

This theorem is referenced by:  eulerpartgbij  31630  eulerpartlemgvv  31634  eulerpartlemgf  31637