Theorem eulerpart

Description: Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let P be the set of all partitions of N , represented as multisets of positive integers, which is to say functions from NN to NN0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals N . Then the set O of all partitions that only consist of odd numbers and the set D of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
	eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
	eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
Assertion	eulerpart	⊢ ( ♯ ‘ 𝑂 ) = ( ♯ ‘ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2		eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3		eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
4		eqid	⊢ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
5		oveq2	⊢ ( 𝑎 = 𝑥 → ( ( 2 ↑ 𝑏 ) · 𝑎 ) = ( ( 2 ↑ 𝑏 ) · 𝑥 ) )
6		oveq2	⊢ ( 𝑏 = 𝑦 → ( 2 ↑ 𝑏 ) = ( 2 ↑ 𝑦 ) )
7	6	oveq1d	⊢ ( 𝑏 = 𝑦 → ( ( 2 ↑ 𝑏 ) · 𝑥 ) = ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
8	5 7	cbvmpov	⊢ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) ) = ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
9		oveq1	⊢ ( 𝑟 = 𝑚 → ( 𝑟 supp ∅ ) = ( 𝑚 supp ∅ ) )
10	9	eleq1d	⊢ ( 𝑟 = 𝑚 → ( ( 𝑟 supp ∅ ) ∈ Fin ↔ ( 𝑚 supp ∅ ) ∈ Fin ) )
11	10	cbvrabv	⊢ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } = { 𝑚 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑚 supp ∅ ) ∈ Fin }
12	11	eqcomi	⊢ { 𝑚 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑚 supp ∅ ) ∈ Fin } = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
13		fveq1	⊢ ( 𝑡 = 𝑟 → ( 𝑡 ‘ 𝑎 ) = ( 𝑟 ‘ 𝑎 ) )
14	13	eleq2d	⊢ ( 𝑡 = 𝑟 → ( 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ↔ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) )
15	14	anbi2d	⊢ ( 𝑡 = 𝑟 → ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) ↔ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) ) )
16	15	opabbidv	⊢ ( 𝑡 = 𝑟 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) } )
17	16	cbvmptv	⊢ ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } ) = ( 𝑟 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) } )
18		oveq1	⊢ ( 𝑚 = 𝑠 → ( 𝑚 supp ∅ ) = ( 𝑠 supp ∅ ) )
19	18	eleq1d	⊢ ( 𝑚 = 𝑠 → ( ( 𝑚 supp ∅ ) ∈ Fin ↔ ( 𝑠 supp ∅ ) ∈ Fin ) )
20	19	cbvrabv	⊢ { 𝑚 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑚 supp ∅ ) ∈ Fin } = { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin }
21	20	eqcomi	⊢ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } = { 𝑚 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑚 supp ∅ ) ∈ Fin }
22		simpl	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → 𝑎 = 𝑥 )
23	22	eleq1d	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ↔ 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) )
24		simpr	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → 𝑏 = 𝑦 )
25	22	fveq2d	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( 𝑟 ‘ 𝑎 ) = ( 𝑟 ‘ 𝑥 ) )
26	24 25	eleq12d	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ↔ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) )
27	23 26	anbi12d	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) ↔ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) ) )
28	27	cbvopabv	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) }
29	21 28	mpteq12i	⊢ ( 𝑟 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) } ) = ( 𝑟 ∈ { 𝑚 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑚 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
30	17 29	eqtri	⊢ ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } ) = ( 𝑟 ∈ { 𝑚 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑚 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
31		cnveq	⊢ ( ℎ = 𝑓 → ◡ ℎ = ◡ 𝑓 )
32	31	imaeq1d	⊢ ( ℎ = 𝑓 → ( ◡ ℎ “ ℕ ) = ( ◡ 𝑓 “ ℕ ) )
33	32	eleq1d	⊢ ( ℎ = 𝑓 → ( ( ◡ ℎ “ ℕ ) ∈ Fin ↔ ( ◡ 𝑓 “ ℕ ) ∈ Fin ) )
34	33	cbvabv	⊢ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
35	32	sseq1d	⊢ ( ℎ = 𝑓 → ( ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ↔ ( ◡ 𝑓 “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) )
36	35	cbvrabv	⊢ { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } }
37		reseq1	⊢ ( 𝑜 = 𝑞 → ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) = ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) )
38	37	coeq2d	⊢ ( 𝑜 = 𝑞 → ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) = ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) )
39	38	fveq2d	⊢ ( 𝑜 = 𝑞 → ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) = ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) )
40	39	imaeq2d	⊢ ( 𝑜 = 𝑞 → ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) = ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) )
41	40	fveq2d	⊢ ( 𝑜 = 𝑞 → ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) = ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) )
42	41	cbvmptv	⊢ ( 𝑜 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) = ( 𝑞 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) )
43	8	eqcomi	⊢ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) = ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) )
44	43	imaeq1i	⊢ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) = ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) )
45		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) }
46	11 45	mpteq12i	⊢ ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) = ( 𝑟 ∈ { 𝑚 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑚 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
47		fveq1	⊢ ( 𝑟 = 𝑡 → ( 𝑟 ‘ 𝑎 ) = ( 𝑡 ‘ 𝑎 ) )
48	47	eleq2d	⊢ ( 𝑟 = 𝑡 → ( 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ↔ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) )
49	48	anbi2d	⊢ ( 𝑟 = 𝑡 → ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) ↔ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) ) )
50	49	opabbidv	⊢ ( 𝑟 = 𝑡 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } )
51	50	cbvmptv	⊢ ( 𝑟 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑟 ‘ 𝑎 ) ) } ) = ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } )
52	46 29 51	3eqtr2i	⊢ ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) = ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } )
53	52	fveq1i	⊢ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) = ( ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) )
54	53	imaeq2i	⊢ ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) = ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) ) “ ( ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) )
55	44 54	eqtri	⊢ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) = ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) ) “ ( ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) )
56	55	fveq2i	⊢ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) = ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) ) “ ( ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) )
57	56	mpteq2i	⊢ ( 𝑞 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) = ( 𝑞 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) ) “ ( ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) )
58	42 57	eqtri	⊢ ( 𝑜 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) = ( 𝑞 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑏 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑏 ) · 𝑎 ) ) “ ( ( 𝑡 ∈ { 𝑠 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑠 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑏 ∈ ( 𝑡 ‘ 𝑎 ) ) } ) ‘ ( bits ∘ ( 𝑞 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) )
59		eqid	⊢ ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) ) = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
60	1 2 3 4 8 12 30 34 36 58 59	eulerpartlemn	⊢ ( ( 𝑜 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) ↾ 𝑂 ) : 𝑂 –1-1-onto→ 𝐷
61		ovex	⊢ ( ℕ0 ↑m ℕ ) ∈ V
62	61	rabex	⊢ { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∈ V
63	62	inex1	⊢ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ∈ V
64	63	mptex	⊢ ( 𝑜 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) ∈ V
65	64	resex	⊢ ( ( 𝑜 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) ↾ 𝑂 ) ∈ V
66		f1oeq1	⊢ ( 𝑔 = ( ( 𝑜 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) ↾ 𝑂 ) → ( 𝑔 : 𝑂 –1-1-onto→ 𝐷 ↔ ( ( 𝑜 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) ↾ 𝑂 ) : 𝑂 –1-1-onto→ 𝐷 ) )
67	65 66	spcev	⊢ ( ( ( 𝑜 ∈ ( { ℎ ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ ℎ “ ℕ ) ⊆ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } } ∩ { ℎ ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) ) “ ( ( 𝑟 ∈ { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ∣ ( 𝑟 supp ∅ ) ∈ Fin } ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } ) ‘ ( bits ∘ ( 𝑜 ↾ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ) ) ) ) ) ) ↾ 𝑂 ) : 𝑂 –1-1-onto→ 𝐷 → ∃ 𝑔 𝑔 : 𝑂 –1-1-onto→ 𝐷 )
68		bren	⊢ ( 𝑂 ≈ 𝐷 ↔ ∃ 𝑔 𝑔 : 𝑂 –1-1-onto→ 𝐷 )
69		hasheni	⊢ ( 𝑂 ≈ 𝐷 → ( ♯ ‘ 𝑂 ) = ( ♯ ‘ 𝐷 ) )
70	68 69	sylbir	⊢ ( ∃ 𝑔 𝑔 : 𝑂 –1-1-onto→ 𝐷 → ( ♯ ‘ 𝑂 ) = ( ♯ ‘ 𝐷 ) )
71	60 67 70	mp2b	⊢ ( ♯ ‘ 𝑂 ) = ( ♯ ‘ 𝐷 )