Theorem eulerpartlem1

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

	Ref	Expression
Hypotheses	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	eulerpartlem1	⊢ 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2		eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3		eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
4		eulerpart.j	⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
5		eulerpart.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
6		eulerpart.h	⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
7		eulerpart.m	⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
8		nnex	⊢ ℕ ∈ V
9	4 8	rabex2	⊢ 𝐽 ∈ V
10		nn0ex	⊢ ℕ0 ∈ V
11		eqid	⊢ ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) = ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
12	9 10 11 6	fpwrelmapffs	⊢ ( ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )
13		ssrab2	⊢ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ⊆ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 )
14	10	pwex	⊢ 𝒫 ℕ0 ∈ V
15		inss1	⊢ ( 𝒫 ℕ0 ∩ Fin ) ⊆ 𝒫 ℕ0
16		mapss	⊢ ( ( 𝒫 ℕ0 ∈ V ∧ ( 𝒫 ℕ0 ∩ Fin ) ⊆ 𝒫 ℕ0 ) → ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ⊆ ( 𝒫 ℕ0 ↑m 𝐽 ) )
17	14 15 16	mp2an	⊢ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ⊆ ( 𝒫 ℕ0 ↑m 𝐽 )
18	13 17	sstri	⊢ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ⊆ ( 𝒫 ℕ0 ↑m 𝐽 )
19	6 18	eqsstri	⊢ 𝐻 ⊆ ( 𝒫 ℕ0 ↑m 𝐽 )
20		resmpt	⊢ ( 𝐻 ⊆ ( 𝒫 ℕ0 ↑m 𝐽 ) → ( ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ↾ 𝐻 ) = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) )
21	19 20	ax-mp	⊢ ( ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ↾ 𝐻 ) = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
22	7 21	eqtr4i	⊢ 𝑀 = ( ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ↾ 𝐻 )
23		f1oeq1	⊢ ( 𝑀 = ( ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ↾ 𝐻 ) → ( 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↔ ( ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ) )
24	22 23	ax-mp	⊢ ( 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) ↔ ( ( 𝑟 ∈ ( 𝒫 ℕ0 ↑m 𝐽 ) ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin ) )
25	12 24	mpbir	⊢ 𝑀 : 𝐻 –1-1-onto→ ( 𝒫 ( 𝐽 × ℕ0 ) ∩ Fin )