Theorem eulerpartlemt 31242

Description: Lemma for eulerpart 31253. (Contributed by Thierry Arnoux, 19-Sep-2017.)

Hypotheses

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

Assertion

Ref	Expression
eulerpartlemt	⊢ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))

Distinct variable groups:   𝑓,𝑚,𝐽   𝑅,𝑚   𝑇,𝑚

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

Proof of Theorem eulerpartlemt

Dummy variable 𝑜 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elmapi 8285	. . . . . . . . . 10 ⊢ (𝑜 ∈ (ℕ0 ↑𝑚 𝐽) → 𝑜:𝐽⟶ℕ0)
2	1	adantr 481	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜:𝐽⟶ℕ0)
3		c0ex 10488	. . . . . . . . . . 11 ⊢ 0 ∈ V
4	3	fconst 6440	. . . . . . . . . 10 ⊢ ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}
5	4	a1i 11	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0})
6		disjdif 4341	. . . . . . . . . 10 ⊢ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅)
8		fun 6415	. . . . . . . . 9 ⊢ (((𝑜:𝐽⟶ℕ0 ∧ ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}) ∧ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}))
9	2, 5, 7, 8	syl21anc 834	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}))
10		eulerpart.j	. . . . . . . . . . 11 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
11		ssrab2 3983	. . . . . . . . . . 11 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
12	10, 11	eqsstri 3928	. . . . . . . . . 10 ⊢ 𝐽 ⊆ ℕ
13		undif 4350	. . . . . . . . . 10 ⊢ (𝐽 ⊆ ℕ ↔ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ)
14	12, 13	mpbi 231	. . . . . . . . 9 ⊢ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ
15		0nn0 11766	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
16		snssi 4654	. . . . . . . . . . 11 ⊢ (0 ∈ ℕ0 → {0} ⊆ ℕ0)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ ℕ0
18		ssequn2 4086	. . . . . . . . . 10 ⊢ ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
19	17, 18	mpbi 231	. . . . . . . . 9 ⊢ (ℕ0 ∪ {0}) = ℕ0
20	14, 19	feq23i 6383	. . . . . . . 8 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
21	9, 20	sylib 219	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
22		nn0ex 11757	. . . . . . . 8 ⊢ ℕ0 ∈ V
23		nnex 11498	. . . . . . . 8 ⊢ ℕ ∈ V
24	22, 23	elmap 8292	. . . . . . 7 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑𝑚 ℕ) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
25	21, 24	sylibr 235	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑𝑚 ℕ))
26		cnvun 5884	. . . . . . . . 9 ⊢ ◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) = (◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0}))
27	26	imaeq1i 5810	. . . . . . . 8 ⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ)
28		imaundir 5892	. . . . . . . 8 ⊢ ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ))
29	27, 28	eqtri 2821	. . . . . . 7 ⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ))
30		vex 3443	. . . . . . . . . . 11 ⊢ 𝑜 ∈ V
31		cnveq 5637	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
32	31	imaeq1d 5812	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ ℕ))
33	32	eleq1d 2869	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑜 “ ℕ) ∈ Fin))
34		eulerpart.r	. . . . . . . . . . 11 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
35	30, 33, 34	elab2 3611	. . . . . . . . . 10 ⊢ (𝑜 ∈ 𝑅 ↔ (◡𝑜 “ ℕ) ∈ Fin)
36	35	biimpi 217	. . . . . . . . 9 ⊢ (𝑜 ∈ 𝑅 → (◡𝑜 “ ℕ) ∈ Fin)
37	36	adantl 482	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ∈ Fin)
38		cnvxp 5897	. . . . . . . . . . . . . 14 ⊢ ◡((ℕ ∖ 𝐽) × {0}) = ({0} × (ℕ ∖ 𝐽))
39	38	dmeqi 5666	. . . . . . . . . . . . 13 ⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = dom ({0} × (ℕ ∖ 𝐽))
40		2nn 11564	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
41		2z 11868	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
42		iddvds 15460	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℤ → 2 ∥ 2)
43	41, 42	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 2 ∥ 2
44		breq2 4972	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 2 → (2 ∥ 𝑧 ↔ 2 ∥ 2))
45	44	notbid 319	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 2 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 2))
46	45, 10	elrab2 3624	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ 𝐽 ↔ (2 ∈ ℕ ∧ ¬ 2 ∥ 2))
47	46	simprbi 497	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ 𝐽 → ¬ 2 ∥ 2)
48	43, 47	mt2 201	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ∈ 𝐽
49		eldif 3875	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ (ℕ ∖ 𝐽) ↔ (2 ∈ ℕ ∧ ¬ 2 ∈ 𝐽))
50	40, 48, 49	mpbir2an 707	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℕ ∖ 𝐽)
51		ne0i 4226	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℕ ∖ 𝐽) → (ℕ ∖ 𝐽) ≠ ∅)
52		dmxp 5688	. . . . . . . . . . . . . 14 ⊢ ((ℕ ∖ 𝐽) ≠ ∅ → dom ({0} × (ℕ ∖ 𝐽)) = {0})
53	50, 51, 52	mp2b 10	. . . . . . . . . . . . 13 ⊢ dom ({0} × (ℕ ∖ 𝐽)) = {0}
54	39, 53	eqtri 2821	. . . . . . . . . . . 12 ⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = {0}
55	54	ineq1i 4111	. . . . . . . . . . 11 ⊢ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ({0} ∩ ℕ)
56		incom 4105	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0}) = ({0} ∩ ℕ)
57		0nnn 11527	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ ℕ
58		disjsn 4560	. . . . . . . . . . . 12 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
59	57, 58	mpbir 232	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0}) = ∅
60	55, 56, 59	3eqtr2i 2827	. . . . . . . . . 10 ⊢ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅
61		imadisj 5831	. . . . . . . . . 10 ⊢ ((◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅ ↔ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅)
62	60, 61	mpbir 232	. . . . . . . . 9 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅
63		0fin 8599	. . . . . . . . 9 ⊢ ∅ ∈ Fin
64	62, 63	eqeltri 2881	. . . . . . . 8 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin
65		unfi 8638	. . . . . . . 8 ⊢ (((◡𝑜 “ ℕ) ∈ Fin ∧ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
66	37, 64, 65	sylancl 586	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
67	29, 66	syl5eqel 2889	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin)
68		cnvimass 5832	. . . . . . . . 9 ⊢ (◡𝑜 “ ℕ) ⊆ dom 𝑜
69	68, 2	fssdm 6405	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ⊆ 𝐽)
70		0ss 4276	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐽
71	62, 70	eqsstri 3928	. . . . . . . . 9 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽
72	71	a1i 11	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽)
73	69, 72	unssd 4089	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ⊆ 𝐽)
74	29, 73	eqsstrid 3942	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆ 𝐽)
75		eulerpart.p	. . . . . . 7 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
76		eulerpart.o	. . . . . . 7 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
77		eulerpart.d	. . . . . . 7 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
78		eulerpart.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
79		eulerpart.h	. . . . . . 7 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
80		eulerpart.m	. . . . . . 7 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
81		eulerpart.t	. . . . . . 7 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑𝑚 ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
82	75, 76, 77, 10, 78, 79, 80, 34, 81	eulerpartlemt0 31240	. . . . . 6 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ↔ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑𝑚 ℕ) ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆ 𝐽))
83	25, 67, 74, 82	syl3anbrc 1336	. . . . 5 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅))
84		resundir 5756	. . . . . 6 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽) = ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽))
85		ffn 6389	. . . . . . . 8 ⊢ (𝑜:𝐽⟶ℕ0 → 𝑜 Fn 𝐽)
86		fnresdm 6343	. . . . . . . . 9 ⊢ (𝑜 Fn 𝐽 → (𝑜 ↾ 𝐽) = 𝑜)
87		incom 4105	. . . . . . . . . . . 12 ⊢ ((ℕ ∖ 𝐽) ∩ 𝐽) = (𝐽 ∩ (ℕ ∖ 𝐽))
88	87, 6	eqtri 2821	. . . . . . . . . . 11 ⊢ ((ℕ ∖ 𝐽) ∩ 𝐽) = ∅
89		fnconstg 6442	. . . . . . . . . . . 12 ⊢ (0 ∈ ℕ0 → ((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽))
90		fnresdisj 6344	. . . . . . . . . . . 12 ⊢ (((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽) → (((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅))
91	15, 89, 90	mp2b 10	. . . . . . . . . . 11 ⊢ (((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)
92	88, 91	mpbi 231	. . . . . . . . . 10 ⊢ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅
93	92	a1i 11	. . . . . . . . 9 ⊢ (𝑜 Fn 𝐽 → (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)
94	86, 93	uneq12d 4067	. . . . . . . 8 ⊢ (𝑜 Fn 𝐽 → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
95	2, 85, 94	3syl 18	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
96		un0 4270	. . . . . . 7 ⊢ (𝑜 ∪ ∅) = 𝑜
97	95, 96	syl6eq 2849	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = 𝑜)
98	84, 97	syl5req 2846	. . . . 5 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
99		reseq1 5735	. . . . . 6 ⊢ (𝑚 = (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) → (𝑚 ↾ 𝐽) = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
100	99	rspceeqv 3579	. . . . 5 ⊢ (((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
101	83, 98, 100	syl2anc 584	. . . 4 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
102		simpr 485	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 = (𝑚 ↾ 𝐽))
103		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (𝑇 ∩ 𝑅))
104	75, 76, 77, 10, 78, 79, 80, 34, 81	eulerpartlemt0 31240	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↔ (𝑚 ∈ (ℕ0 ↑𝑚 ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽))
105	103, 104	sylib 219	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ∈ (ℕ0 ↑𝑚 ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽))
106	105	simp1d 1135	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (ℕ0 ↑𝑚 ℕ))
107	22, 23	elmap 8292	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℕ0 ↑𝑚 ℕ) ↔ 𝑚:ℕ⟶ℕ0)
108	106, 107	sylib 219	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚:ℕ⟶ℕ0)
109		fssres 6419	. . . . . . . . 9 ⊢ ((𝑚:ℕ⟶ℕ0 ∧ 𝐽 ⊆ ℕ) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
110	108, 12, 109	sylancl 586	. . . . . . . 8 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
111	10, 23	rabex2 5135	. . . . . . . . 9 ⊢ 𝐽 ∈ V
112	22, 111	elmap 8292	. . . . . . . 8 ⊢ ((𝑚 ↾ 𝐽) ∈ (ℕ0 ↑𝑚 𝐽) ↔ (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
113	110, 112	sylibr 235	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ (ℕ0 ↑𝑚 𝐽))
114	102, 113	eqeltrd 2885	. . . . . 6 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ (ℕ0 ↑𝑚 𝐽))
115		ffun 6392	. . . . . . . . . 10 ⊢ (𝑚:ℕ⟶ℕ0 → Fun 𝑚)
116		respreima 6708	. . . . . . . . . 10 ⊢ (Fun 𝑚 → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽))
117	108, 115, 116	3syl 18	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽))
118	105	simp2d 1136	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡𝑚 “ ℕ) ∈ Fin)
119		infi 8595	. . . . . . . . . 10 ⊢ ((◡𝑚 “ ℕ) ∈ Fin → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
120	118, 119	syl 17	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
121	117, 120	eqeltrd 2885	. . . . . . . 8 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin)
122		vex 3443	. . . . . . . . . 10 ⊢ 𝑚 ∈ V
123	122	resex 5787	. . . . . . . . 9 ⊢ (𝑚 ↾ 𝐽) ∈ V
124		cnveq 5637	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → ◡𝑓 = ◡(𝑚 ↾ 𝐽))
125	124	imaeq1d 5812	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → (◡𝑓 “ ℕ) = (◡(𝑚 ↾ 𝐽) “ ℕ))
126	125	eleq1d 2869	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin))
127	123, 126, 34	elab2 3611	. . . . . . . 8 ⊢ ((𝑚 ↾ 𝐽) ∈ 𝑅 ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin)
128	121, 127	sylibr 235	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ 𝑅)
129	102, 128	eqeltrd 2885	. . . . . 6 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ 𝑅)
130	114, 129	jca 512	. . . . 5 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅))
131	130	rexlimiva 3246	. . . 4 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽) → (𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅))
132	101, 131	impbii 210	. . 3 ⊢ ((𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
133	132	abbii 2863	. 2 ⊢ {𝑜 ∣ (𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅)} = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)}
134		df-in 3872	. 2 ⊢ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = {𝑜 ∣ (𝑜 ∈ (ℕ0 ↑𝑚 𝐽) ∧ 𝑜 ∈ 𝑅)}
135		eqid 2797	. . 3 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
136	135	rnmpt 5716	. 2 ⊢ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)}
137	133, 134, 136	3eqtr4i 2831	1 ⊢ ((ℕ0 ↑𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))

Syntax hints:  ¬ wn 3   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083  {cab 2777   ≠ wne 2986  ∀wral 3107  ∃wrex 3108  {crab 3111   ∖ cdif 3862   ∪ cun 3863   ∩ cin 3864   ⊆ wss 3865  ∅c0 4217  𝒫 cpw 4459  {csn 4478   class class class wbr 4968  {copab 5030   ↦ cmpt 5047   × cxp 5448  ^◡ccnv 5449  dom cdm 5450  ran crn 5451   ↾ cres 5452   “ cima 5453  Fun wfun 6226   Fn wfn 6227  ⟶wf 6228  ‘cfv 6232  (class class class)co 7023   ∈ cmpo 7025   supp csupp 7688   ↑_𝑚 cmap 8263  Fincfn 8364  0cc0 10390  1c1 10391   · cmul 10395   ≤ cle 10529  ℕcn 11492  2c2 11546  ℕ₀cn0 11751  ℤcz 11835  ↑cexp 13283  Σcsu 14880   ∥ cdvds 15444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-oadd 7964  df-er 8146  df-map 8265  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-neg 10726  df-nn 11493  df-2 11554  df-n0 11752  df-z 11836  df-dvds 15445

This theorem is referenced by:  eulerpartgbij  31243