Theorem eulerpartlemt 31920

Description: Lemma for eulerpart 31931. (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 8471	. . . . . . . . . 10 ⊢ (𝑜 ∈ (ℕ0 ↑m 𝐽) → 𝑜:𝐽⟶ℕ0)
2	1	adantr 484	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜:𝐽⟶ℕ0)
3		c0ex 10725	. . . . . . . . . . 11 ⊢ 0 ∈ V
4	3	fconst 6574	. . . . . . . . . 10 ⊢ ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}
5	4	a1i 11	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0})
6		disjdif 4371	. . . . . . . . . 10 ⊢ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅)
8		fun 6550	. . . . . . . . 9 ⊢ (((𝑜:𝐽⟶ℕ0 ∧ ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}) ∧ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}))
9	2, 5, 7, 8	syl21anc 837	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}))
10		eulerpart.j	. . . . . . . . . . 11 ⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
11		ssrab2 3979	. . . . . . . . . . 11 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
12	10, 11	eqsstri 3921	. . . . . . . . . 10 ⊢ 𝐽 ⊆ ℕ
13		undif 4381	. . . . . . . . . 10 ⊢ (𝐽 ⊆ ℕ ↔ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ)
14	12, 13	mpbi 233	. . . . . . . . 9 ⊢ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ
15		0nn0 12003	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
16		snssi 4706	. . . . . . . . . . 11 ⊢ (0 ∈ ℕ0 → {0} ⊆ ℕ0)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ ℕ0
18		ssequn2 4083	. . . . . . . . . 10 ⊢ ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
19	17, 18	mpbi 233	. . . . . . . . 9 ⊢ (ℕ0 ∪ {0}) = ℕ0
20	14, 19	feq23i 6508	. . . . . . . 8 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
21	9, 20	sylib 221	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
22		nn0ex 11994	. . . . . . . 8 ⊢ ℕ0 ∈ V
23		nnex 11734	. . . . . . . 8 ⊢ ℕ ∈ V
24	22, 23	elmap 8493	. . . . . . 7 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
25	21, 24	sylibr 237	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ))
26		cnvun 5985	. . . . . . . . 9 ⊢ ◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) = (◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0}))
27	26	imaeq1i 5910	. . . . . . . 8 ⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ)
28		imaundir 5993	. . . . . . . 8 ⊢ ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ))
29	27, 28	eqtri 2762	. . . . . . 7 ⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ))
30		vex 3404	. . . . . . . . . . 11 ⊢ 𝑜 ∈ V
31		cnveq 5726	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
32	31	imaeq1d 5912	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ ℕ))
33	32	eleq1d 2818	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑜 “ ℕ) ∈ Fin))
34		eulerpart.r	. . . . . . . . . . 11 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
35	30, 33, 34	elab2 3582	. . . . . . . . . 10 ⊢ (𝑜 ∈ 𝑅 ↔ (◡𝑜 “ ℕ) ∈ Fin)
36	35	biimpi 219	. . . . . . . . 9 ⊢ (𝑜 ∈ 𝑅 → (◡𝑜 “ ℕ) ∈ Fin)
37	36	adantl 485	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ∈ Fin)
38		cnvxp 5999	. . . . . . . . . . . . . 14 ⊢ ◡((ℕ ∖ 𝐽) × {0}) = ({0} × (ℕ ∖ 𝐽))
39	38	dmeqi 5757	. . . . . . . . . . . . 13 ⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = dom ({0} × (ℕ ∖ 𝐽))
40		2nn 11801	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
41		2z 12107	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
42		iddvds 15727	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℤ → 2 ∥ 2)
43	41, 42	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 2 ∥ 2
44		breq2 5044	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 2 → (2 ∥ 𝑧 ↔ 2 ∥ 2))
45	44	notbid 321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 2 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 2))
46	45, 10	elrab2 3596	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ 𝐽 ↔ (2 ∈ ℕ ∧ ¬ 2 ∥ 2))
47	46	simprbi 500	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ 𝐽 → ¬ 2 ∥ 2)
48	43, 47	mt2 203	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ∈ 𝐽
49		eldif 3863	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ (ℕ ∖ 𝐽) ↔ (2 ∈ ℕ ∧ ¬ 2 ∈ 𝐽))
50	40, 48, 49	mpbir2an 711	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℕ ∖ 𝐽)
51		ne0i 4233	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℕ ∖ 𝐽) → (ℕ ∖ 𝐽) ≠ ∅)
52		dmxp 5782	. . . . . . . . . . . . . 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 4109	. . . . . . . . . . 11 ⊢ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ({0} ∩ ℕ)
56		incom 4101	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0}) = ({0} ∩ ℕ)
57		0nnn 11764	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ ℕ
58		disjsn 4612	. . . . . . . . . . . 12 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
59	57, 58	mpbir 234	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0}) = ∅
60	55, 56, 59	3eqtr2i 2768	. . . . . . . . . 10 ⊢ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅
61		imadisj 5932	. . . . . . . . . 10 ⊢ ((◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅ ↔ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅)
62	60, 61	mpbir 234	. . . . . . . . 9 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅
63		0fin 8782	. . . . . . . . 9 ⊢ ∅ ∈ Fin
64	62, 63	eqeltri 2830	. . . . . . . 8 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin
65		unfi 8783	. . . . . . . 8 ⊢ (((◡𝑜 “ ℕ) ∈ Fin ∧ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
66	37, 64, 65	sylancl 589	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
67	29, 66	eqeltrid 2838	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin)
68		cnvimass 5933	. . . . . . . . 9 ⊢ (◡𝑜 “ ℕ) ⊆ dom 𝑜
69	68, 2	fssdm 6534	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ⊆ 𝐽)
70		0ss 4295	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐽
71	62, 70	eqsstri 3921	. . . . . . . . 9 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽
72	71	a1i 11	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽)
73	69, 72	unssd 4086	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ⊆ 𝐽)
74	29, 73	eqsstrid 3935	. . . . . 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 31918	. . . . . 6 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ↔ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ) ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆ 𝐽))
83	25, 67, 74, 82	syl3anbrc 1344	. . . . 5 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅))
84		resundir 5850	. . . . . 6 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽) = ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽))
85		ffn 6514	. . . . . . . 8 ⊢ (𝑜:𝐽⟶ℕ0 → 𝑜 Fn 𝐽)
86		fnresdm 6465	. . . . . . . . 9 ⊢ (𝑜 Fn 𝐽 → (𝑜 ↾ 𝐽) = 𝑜)
87		disjdifr 4372	. . . . . . . . . . 11 ⊢ ((ℕ ∖ 𝐽) ∩ 𝐽) = ∅
88		fnconstg 6576	. . . . . . . . . . . 12 ⊢ (0 ∈ ℕ0 → ((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽))
89		fnresdisj 6466	. . . . . . . . . . . 12 ⊢ (((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽) → (((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅))
90	15, 88, 89	mp2b 10	. . . . . . . . . . 11 ⊢ (((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)
91	87, 90	mpbi 233	. . . . . . . . . 10 ⊢ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅
92	91	a1i 11	. . . . . . . . 9 ⊢ (𝑜 Fn 𝐽 → (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)
93	86, 92	uneq12d 4064	. . . . . . . 8 ⊢ (𝑜 Fn 𝐽 → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
94	2, 85, 93	3syl 18	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
95		un0 4289	. . . . . . 7 ⊢ (𝑜 ∪ ∅) = 𝑜
96	94, 95	eqtrdi 2790	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = 𝑜)
97	84, 96	eqtr2id 2787	. . . . 5 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
98		reseq1 5829	. . . . . 6 ⊢ (𝑚 = (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) → (𝑚 ↾ 𝐽) = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
99	98	rspceeqv 3544	. . . . 5 ⊢ (((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
100	83, 97, 99	syl2anc 587	. . . 4 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
101		simpr 488	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 = (𝑚 ↾ 𝐽))
102		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (𝑇 ∩ 𝑅))
103	75, 76, 77, 10, 78, 79, 80, 34, 81	eulerpartlemt0 31918	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↔ (𝑚 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽))
104	102, 103	sylib 221	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽))
105	104	simp1d 1143	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (ℕ0 ↑m ℕ))
106	22, 23	elmap 8493	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℕ0 ↑m ℕ) ↔ 𝑚:ℕ⟶ℕ0)
107	105, 106	sylib 221	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚:ℕ⟶ℕ0)
108		fssres 6554	. . . . . . . . 9 ⊢ ((𝑚:ℕ⟶ℕ0 ∧ 𝐽 ⊆ ℕ) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
109	107, 12, 108	sylancl 589	. . . . . . . 8 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
110	10, 23	rabex2 5212	. . . . . . . . 9 ⊢ 𝐽 ∈ V
111	22, 110	elmap 8493	. . . . . . . 8 ⊢ ((𝑚 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽) ↔ (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
112	109, 111	sylibr 237	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽))
113	101, 112	eqeltrd 2834	. . . . . 6 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ (ℕ0 ↑m 𝐽))
114		ffun 6517	. . . . . . . . . 10 ⊢ (𝑚:ℕ⟶ℕ0 → Fun 𝑚)
115		respreima 6855	. . . . . . . . . 10 ⊢ (Fun 𝑚 → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽))
116	107, 114, 115	3syl 18	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽))
117	104	simp2d 1144	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡𝑚 “ ℕ) ∈ Fin)
118		infi 8832	. . . . . . . . . 10 ⊢ ((◡𝑚 “ ℕ) ∈ Fin → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
119	117, 118	syl 17	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
120	116, 119	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin)
121		vex 3404	. . . . . . . . . 10 ⊢ 𝑚 ∈ V
122	121	resex 5883	. . . . . . . . 9 ⊢ (𝑚 ↾ 𝐽) ∈ V
123		cnveq 5726	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → ◡𝑓 = ◡(𝑚 ↾ 𝐽))
124	123	imaeq1d 5912	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → (◡𝑓 “ ℕ) = (◡(𝑚 ↾ 𝐽) “ ℕ))
125	124	eleq1d 2818	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin))
126	122, 125, 34	elab2 3582	. . . . . . . 8 ⊢ ((𝑚 ↾ 𝐽) ∈ 𝑅 ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin)
127	120, 126	sylibr 237	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ 𝑅)
128	101, 127	eqeltrd 2834	. . . . . 6 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ 𝑅)
129	113, 128	jca 515	. . . . 5 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅))
130	129	rexlimiva 3192	. . . 4 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽) → (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅))
131	100, 130	impbii 212	. . 3 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
132	131	abbii 2804	. 2 ⊢ {𝑜 ∣ (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅)} = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)}
133		df-in 3860	. 2 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑜 ∣ (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅)}
134		eqid 2739	. . 3 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
135	134	rnmpt 5808	. 2 ⊢ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)}
136	132, 133, 135	3eqtr4i 2772	1 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  {cab 2717   ≠ wne 2935  ∀wral 3054  ∃wrex 3055  {crab 3058   ∖ cdif 3850   ∪ cun 3851   ∩ cin 3852   ⊆ wss 3853  ∅c0 4221  𝒫 cpw 4498  {csn 4526   class class class wbr 5040  {copab 5102   ↦ cmpt 5120   × cxp 5533  ^◡ccnv 5534  dom cdm 5535  ran crn 5536   ↾ cres 5537   “ cima 5538  Fun wfun 6343   Fn wfn 6344  ⟶wf 6345  ‘cfv 6349  (class class class)co 7182   ∈ cmpo 7184   supp csupp 7868   ↑_m cmap 8449  Fincfn 8567  0cc0 10627  1c1 10628   · cmul 10632   ≤ cle 10766  ℕcn 11728  2c2 11783  ℕ₀cn0 11988  ℤcz 12074  ↑cexp 13533  Σcsu 15147   ∥ cdvds 15711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7491  ax-cnex 10683  ax-resscn 10684  ax-1cn 10685  ax-icn 10686  ax-addcl 10687  ax-addrcl 10688  ax-mulcl 10689  ax-mulrcl 10690  ax-mulcom 10691  ax-addass 10692  ax-mulass 10693  ax-distr 10694  ax-i2m1 10695  ax-1ne0 10696  ax-1rid 10697  ax-rnegex 10698  ax-rrecex 10699  ax-cnre 10700  ax-pre-lttri 10701  ax-pre-lttrn 10702  ax-pre-ltadd 10703

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-iun 4893  df-br 5041  df-opab 5103  df-mpt 5121  df-tr 5147  df-id 5439  df-eprel 5444  df-po 5452  df-so 5453  df-fr 5493  df-we 5495  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-pred 6139  df-ord 6185  df-on 6186  df-lim 6187  df-suc 6188  df-iota 6307  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7185  df-oprab 7186  df-mpo 7187  df-om 7612  df-1st 7726  df-2nd 7727  df-wrecs 7988  df-recs 8049  df-rdg 8087  df-1o 8143  df-er 8332  df-map 8451  df-en 8568  df-dom 8569  df-sdom 8570  df-fin 8571  df-pnf 10767  df-mnf 10768  df-xr 10769  df-ltxr 10770  df-le 10771  df-neg 10963  df-nn 11729  df-2 11791  df-n0 11989  df-z 12075  df-dvds 15712

This theorem is referenced by:  eulerpartgbij  31921