Theorem eulerpartlemt 34352

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

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	⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
eulerpart.r	⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
eulerpart.t	⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}

Assertion

Ref	Expression
eulerpartlemt	⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = 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 8887	. . . . . . . . . 10 ⊢ (𝑜 ∈ (ℕ0 ↑m 𝐽) → 𝑜:𝐽⟶ℕ0)
2	1	adantr 480	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜:𝐽⟶ℕ0)
3		c0ex 11252	. . . . . . . . . . 11 ⊢ 0 ∈ V
4	3	fconst 6794	. . . . . . . . . 10 ⊢ ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}
5	4	a1i 11	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0})
6		disjdif 4477	. . . . . . . . . 10 ⊢ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅)
8		fun 6770	. . . . . . . . 9 ⊢ (((𝑜:𝐽⟶ℕ0 ∧ ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}) ∧ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}))
9	2, 5, 7, 8	syl21anc 838	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}))
10		eulerpart.j	. . . . . . . . . . 11 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
11		ssrab2 4089	. . . . . . . . . . 11 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
12	10, 11	eqsstri 4029	. . . . . . . . . 10 ⊢ 𝐽 ⊆ ℕ
13		undif 4487	. . . . . . . . . 10 ⊢ (𝐽 ⊆ ℕ ↔ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ)
14	12, 13	mpbi 230	. . . . . . . . 9 ⊢ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ
15		0nn0 12538	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
16		snssi 4812	. . . . . . . . . . 11 ⊢ (0 ∈ ℕ0 → {0} ⊆ ℕ0)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ ℕ0
18		ssequn2 4198	. . . . . . . . . 10 ⊢ ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
19	17, 18	mpbi 230	. . . . . . . . 9 ⊢ (ℕ0 ∪ {0}) = ℕ0
20	14, 19	feq23i 6730	. . . . . . . 8 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
21	9, 20	sylib 218	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
22		nn0ex 12529	. . . . . . . 8 ⊢ ℕ0 ∈ V
23		nnex 12269	. . . . . . . 8 ⊢ ℕ ∈ V
24	22, 23	elmap 8909	. . . . . . 7 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
25	21, 24	sylibr 234	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ))
26		cnvun 6164	. . . . . . . . 9 ⊢ ◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) = (◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0}))
27	26	imaeq1i 6076	. . . . . . . 8 ⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ)
28		imaundir 6172	. . . . . . . 8 ⊢ ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ))
29	27, 28	eqtri 2762	. . . . . . 7 ⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ))
30		vex 3481	. . . . . . . . . . 11 ⊢ 𝑜 ∈ V
31		cnveq 5886	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
32	31	imaeq1d 6078	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ ℕ))
33	32	eleq1d 2823	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑜 “ ℕ) ∈ Fin))
34		eulerpart.r	. . . . . . . . . . 11 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
35	30, 33, 34	elab2 3684	. . . . . . . . . 10 ⊢ (𝑜 ∈ 𝑅 ↔ (◡𝑜 “ ℕ) ∈ Fin)
36	35	biimpi 216	. . . . . . . . 9 ⊢ (𝑜 ∈ 𝑅 → (◡𝑜 “ ℕ) ∈ Fin)
37	36	adantl 481	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ∈ Fin)
38		cnvxp 6178	. . . . . . . . . . . . . 14 ⊢ ◡((ℕ ∖ 𝐽) × {0}) = ({0} × (ℕ ∖ 𝐽))
39	38	dmeqi 5917	. . . . . . . . . . . . 13 ⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = dom ({0} × (ℕ ∖ 𝐽))
40		2nn 12336	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
41		2z 12646	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
42		iddvds 16303	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℤ → 2 ∥ 2)
43	41, 42	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 2 ∥ 2
44		breq2 5151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 2 → (2 ∥ 𝑧 ↔ 2 ∥ 2))
45	44	notbid 318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 2 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 2))
46	45, 10	elrab2 3697	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ 𝐽 ↔ (2 ∈ ℕ ∧ ¬ 2 ∥ 2))
47	46	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ 𝐽 → ¬ 2 ∥ 2)
48	43, 47	mt2 200	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ∈ 𝐽
49		eldif 3972	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ (ℕ ∖ 𝐽) ↔ (2 ∈ ℕ ∧ ¬ 2 ∈ 𝐽))
50	40, 48, 49	mpbir2an 711	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℕ ∖ 𝐽)
51		ne0i 4346	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℕ ∖ 𝐽) → (ℕ ∖ 𝐽) ≠ ∅)
52		dmxp 5941	. . . . . . . . . . . . . 14 ⊢ ((ℕ ∖ 𝐽) ≠ ∅ → dom ({0} × (ℕ ∖ 𝐽)) = {0})
53	50, 51, 52	mp2b 10	. . . . . . . . . . . . 13 ⊢ dom ({0} × (ℕ ∖ 𝐽)) = {0}
54	39, 53	eqtri 2762	. . . . . . . . . . . 12 ⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = {0}
55	54	ineq1i 4223	. . . . . . . . . . 11 ⊢ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ({0} ∩ ℕ)
56		incom 4216	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0}) = ({0} ∩ ℕ)
57		0nnn 12299	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ ℕ
58		disjsn 4715	. . . . . . . . . . . 12 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
59	57, 58	mpbir 231	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0}) = ∅
60	55, 56, 59	3eqtr2i 2768	. . . . . . . . . 10 ⊢ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅
61		imadisj 6099	. . . . . . . . . 10 ⊢ ((◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅ ↔ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅)
62	60, 61	mpbir 231	. . . . . . . . 9 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅
63		0fi 9080	. . . . . . . . 9 ⊢ ∅ ∈ Fin
64	62, 63	eqeltri 2834	. . . . . . . 8 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin
65		unfi 9209	. . . . . . . 8 ⊢ (((◡𝑜 “ ℕ) ∈ Fin ∧ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
66	37, 64, 65	sylancl 586	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
67	29, 66	eqeltrid 2842	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin)
68		cnvimass 6101	. . . . . . . . 9 ⊢ (◡𝑜 “ ℕ) ⊆ dom 𝑜
69	68, 2	fssdm 6755	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ⊆ 𝐽)
70		0ss 4405	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐽
71	62, 70	eqsstri 4029	. . . . . . . . 9 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽
72	71	a1i 11	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽)
73	69, 72	unssd 4201	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ⊆ 𝐽)
74	29, 73	eqsstrid 4043	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆ 𝐽)
75		eulerpart.p	. . . . . . 7 ⊢ 𝑃 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ ((◡𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓‘𝑘) · 𝑘) = 𝑁)}
76		eulerpart.o	. . . . . . 7 ⊢ 𝑂 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ (◡𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
77		eulerpart.d	. . . . . . 7 ⊢ 𝐷 = {𝑔 ∈ 𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ≤ 1}
78		eulerpart.f	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
79		eulerpart.h	. . . . . . 7 ⊢ 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑m 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
80		eulerpart.m	. . . . . . 7 ⊢ 𝑀 = (𝑟 ∈ 𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ (𝑟‘𝑥))})
81		eulerpart.t	. . . . . . 7 ⊢ 𝑇 = {𝑓 ∈ (ℕ0 ↑m ℕ) ∣ (◡𝑓 “ ℕ) ⊆ 𝐽}
82	75, 76, 77, 10, 78, 79, 80, 34, 81	eulerpartlemt0 34350	. . . . . 6 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ↔ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ) ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆ 𝐽))
83	25, 67, 74, 82	syl3anbrc 1342	. . . . 5 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅))
84		resundir 6014	. . . . . 6 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽) = ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽))
85		ffn 6736	. . . . . . . 8 ⊢ (𝑜:𝐽⟶ℕ0 → 𝑜 Fn 𝐽)
86		fnresdm 6687	. . . . . . . . 9 ⊢ (𝑜 Fn 𝐽 → (𝑜 ↾ 𝐽) = 𝑜)
87		disjdifr 4478	. . . . . . . . . . 11 ⊢ ((ℕ ∖ 𝐽) ∩ 𝐽) = ∅
88		fnconstg 6796	. . . . . . . . . . . 12 ⊢ (0 ∈ ℕ0 → ((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽))
89		fnresdisj 6688	. . . . . . . . . . . 12 ⊢ (((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽) → (((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅))
90	15, 88, 89	mp2b 10	. . . . . . . . . . 11 ⊢ (((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)
91	87, 90	mpbi 230	. . . . . . . . . 10 ⊢ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅
92	91	a1i 11	. . . . . . . . 9 ⊢ (𝑜 Fn 𝐽 → (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)
93	86, 92	uneq12d 4178	. . . . . . . 8 ⊢ (𝑜 Fn 𝐽 → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
94	2, 85, 93	3syl 18	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
95		un0 4399	. . . . . . 7 ⊢ (𝑜 ∪ ∅) = 𝑜
96	94, 95	eqtrdi 2790	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = 𝑜)
97	84, 96	eqtr2id 2787	. . . . 5 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
98		reseq1 5993	. . . . . 6 ⊢ (𝑚 = (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) → (𝑚 ↾ 𝐽) = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
99	98	rspceeqv 3644	. . . . 5 ⊢ (((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
100	83, 97, 99	syl2anc 584	. . . 4 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
101		simpr 484	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 = (𝑚 ↾ 𝐽))
102		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (𝑇 ∩ 𝑅))
103	75, 76, 77, 10, 78, 79, 80, 34, 81	eulerpartlemt0 34350	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↔ (𝑚 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽))
104	102, 103	sylib 218	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽))
105	104	simp1d 1141	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (ℕ0 ↑m ℕ))
106	22, 23	elmap 8909	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℕ0 ↑m ℕ) ↔ 𝑚:ℕ⟶ℕ0)
107	105, 106	sylib 218	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚:ℕ⟶ℕ0)
108		fssres 6774	. . . . . . . . 9 ⊢ ((𝑚:ℕ⟶ℕ0 ∧ 𝐽 ⊆ ℕ) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
109	107, 12, 108	sylancl 586	. . . . . . . 8 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
110	10, 23	rabex2 5346	. . . . . . . . 9 ⊢ 𝐽 ∈ V
111	22, 110	elmap 8909	. . . . . . . 8 ⊢ ((𝑚 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽) ↔ (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
112	109, 111	sylibr 234	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽))
113	101, 112	eqeltrd 2838	. . . . . 6 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ (ℕ0 ↑m 𝐽))
114		ffun 6739	. . . . . . . . . 10 ⊢ (𝑚:ℕ⟶ℕ0 → Fun 𝑚)
115		respreima 7085	. . . . . . . . . 10 ⊢ (Fun 𝑚 → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽))
116	107, 114, 115	3syl 18	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽))
117	104	simp2d 1142	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡𝑚 “ ℕ) ∈ Fin)
118		infi 9299	. . . . . . . . . 10 ⊢ ((◡𝑚 “ ℕ) ∈ Fin → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
119	117, 118	syl 17	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
120	116, 119	eqeltrd 2838	. . . . . . . 8 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin)
121		vex 3481	. . . . . . . . . 10 ⊢ 𝑚 ∈ V
122	121	resex 6048	. . . . . . . . 9 ⊢ (𝑚 ↾ 𝐽) ∈ V
123		cnveq 5886	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → ◡𝑓 = ◡(𝑚 ↾ 𝐽))
124	123	imaeq1d 6078	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → (◡𝑓 “ ℕ) = (◡(𝑚 ↾ 𝐽) “ ℕ))
125	124	eleq1d 2823	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin))
126	122, 125, 34	elab2 3684	. . . . . . . 8 ⊢ ((𝑚 ↾ 𝐽) ∈ 𝑅 ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin)
127	120, 126	sylibr 234	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ 𝑅)
128	101, 127	eqeltrd 2838	. . . . . 6 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ 𝑅)
129	113, 128	jca 511	. . . . 5 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅))
130	129	rexlimiva 3144	. . . 4 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽) → (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅))
131	100, 130	impbii 209	. . 3 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
132	131	abbii 2806	. 2 ⊢ {𝑜 ∣ (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅)} = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)}
133		df-in 3969	. 2 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑜 ∣ (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅)}
134		eqid 2734	. . 3 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
135	134	rnmpt 5970	. 2 ⊢ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)}
136	132, 133, 135	3eqtr4i 2772	1 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  {cab 2711   ≠ wne 2937  ∀wral 3058  ∃wrex 3067  {crab 3432   ∖ cdif 3959   ∪ cun 3960   ∩ cin 3961   ⊆ wss 3962  ∅c0 4338  𝒫 cpw 4604  {csn 4630   class class class wbr 5147  {copab 5209   ↦ cmpt 5230   × cxp 5686  ^◡ccnv 5687  dom cdm 5688  ran crn 5689   ↾ cres 5690   “ cima 5691  Fun wfun 6556   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430   ∈ cmpo 7432   supp csupp 8183   ↑_m cmap 8864  Fincfn 8983  0cc0 11152  1c1 11153   · cmul 11157   ≤ cle 11293  ℕcn 12263  2c2 12318  ℕ₀cn0 12523  ℤcz 12610  ↑cexp 14098  Σcsu 15718   ∥ cdvds 16286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-neg 11492  df-nn 12264  df-2 12326  df-n0 12524  df-z 12611  df-dvds 16287

This theorem is referenced by:  eulerpartgbij  34353