Theorem eulerpartlemt 34336

Description: Lemma for eulerpart 34347. (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 8907	. . . . . . . . . 10 ⊢ (𝑜 ∈ (ℕ0 ↑m 𝐽) → 𝑜:𝐽⟶ℕ0)
2	1	adantr 480	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜:𝐽⟶ℕ0)
3		c0ex 11284	. . . . . . . . . . 11 ⊢ 0 ∈ V
4	3	fconst 6807	. . . . . . . . . 10 ⊢ ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}
5	4	a1i 11	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0})
6		disjdif 4495	. . . . . . . . . 10 ⊢ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅)
8		fun 6783	. . . . . . . . 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 4103	. . . . . . . . . . 11 ⊢ {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
12	10, 11	eqsstri 4043	. . . . . . . . . 10 ⊢ 𝐽 ⊆ ℕ
13		undif 4505	. . . . . . . . . 10 ⊢ (𝐽 ⊆ ℕ ↔ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ)
14	12, 13	mpbi 230	. . . . . . . . 9 ⊢ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ
15		0nn0 12568	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
16		snssi 4833	. . . . . . . . . . 11 ⊢ (0 ∈ ℕ0 → {0} ⊆ ℕ0)
17	15, 16	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ ℕ0
18		ssequn2 4212	. . . . . . . . . 10 ⊢ ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
19	17, 18	mpbi 230	. . . . . . . . 9 ⊢ (ℕ0 ∪ {0}) = ℕ0
20	14, 19	feq23i 6741	. . . . . . . 8 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
21	9, 20	sylib 218	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
22		nn0ex 12559	. . . . . . . 8 ⊢ ℕ0 ∈ V
23		nnex 12299	. . . . . . . 8 ⊢ ℕ ∈ V
24	22, 23	elmap 8929	. . . . . . 7 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
25	21, 24	sylibr 234	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ))
26		cnvun 6174	. . . . . . . . 9 ⊢ ◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) = (◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0}))
27	26	imaeq1i 6086	. . . . . . . 8 ⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ)
28		imaundir 6182	. . . . . . . 8 ⊢ ((◡𝑜 ∪ ◡((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ))
29	27, 28	eqtri 2768	. . . . . . 7 ⊢ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ))
30		vex 3492	. . . . . . . . . . 11 ⊢ 𝑜 ∈ V
31		cnveq 5898	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑜 → ◡𝑓 = ◡𝑜)
32	31	imaeq1d 6088	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑜 → (◡𝑓 “ ℕ) = (◡𝑜 “ ℕ))
33	32	eleq1d 2829	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑜 → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡𝑜 “ ℕ) ∈ Fin))
34		eulerpart.r	. . . . . . . . . . 11 ⊢ 𝑅 = {𝑓 ∣ (◡𝑓 “ ℕ) ∈ Fin}
35	30, 33, 34	elab2 3698	. . . . . . . . . 10 ⊢ (𝑜 ∈ 𝑅 ↔ (◡𝑜 “ ℕ) ∈ Fin)
36	35	biimpi 216	. . . . . . . . 9 ⊢ (𝑜 ∈ 𝑅 → (◡𝑜 “ ℕ) ∈ Fin)
37	36	adantl 481	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ∈ Fin)
38		cnvxp 6188	. . . . . . . . . . . . . 14 ⊢ ◡((ℕ ∖ 𝐽) × {0}) = ({0} × (ℕ ∖ 𝐽))
39	38	dmeqi 5929	. . . . . . . . . . . . 13 ⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = dom ({0} × (ℕ ∖ 𝐽))
40		2nn 12366	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ
41		2z 12675	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℤ
42		iddvds 16318	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℤ → 2 ∥ 2)
43	41, 42	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ 2 ∥ 2
44		breq2 5170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 2 → (2 ∥ 𝑧 ↔ 2 ∥ 2))
45	44	notbid 318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 = 2 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 2))
46	45, 10	elrab2 3711	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ 𝐽 ↔ (2 ∈ ℕ ∧ ¬ 2 ∥ 2))
47	46	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ 𝐽 → ¬ 2 ∥ 2)
48	43, 47	mt2 200	. . . . . . . . . . . . . . 15 ⊢ ¬ 2 ∈ 𝐽
49		eldif 3986	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ (ℕ ∖ 𝐽) ↔ (2 ∈ ℕ ∧ ¬ 2 ∈ 𝐽))
50	40, 48, 49	mpbir2an 710	. . . . . . . . . . . . . 14 ⊢ 2 ∈ (ℕ ∖ 𝐽)
51		ne0i 4364	. . . . . . . . . . . . . 14 ⊢ (2 ∈ (ℕ ∖ 𝐽) → (ℕ ∖ 𝐽) ≠ ∅)
52		dmxp 5953	. . . . . . . . . . . . . 14 ⊢ ((ℕ ∖ 𝐽) ≠ ∅ → dom ({0} × (ℕ ∖ 𝐽)) = {0})
53	50, 51, 52	mp2b 10	. . . . . . . . . . . . 13 ⊢ dom ({0} × (ℕ ∖ 𝐽)) = {0}
54	39, 53	eqtri 2768	. . . . . . . . . . . 12 ⊢ dom ◡((ℕ ∖ 𝐽) × {0}) = {0}
55	54	ineq1i 4237	. . . . . . . . . . 11 ⊢ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ({0} ∩ ℕ)
56		incom 4230	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0}) = ({0} ∩ ℕ)
57		0nnn 12329	. . . . . . . . . . . 12 ⊢ ¬ 0 ∈ ℕ
58		disjsn 4736	. . . . . . . . . . . 12 ⊢ ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
59	57, 58	mpbir 231	. . . . . . . . . . 11 ⊢ (ℕ ∩ {0}) = ∅
60	55, 56, 59	3eqtr2i 2774	. . . . . . . . . 10 ⊢ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅
61		imadisj 6109	. . . . . . . . . 10 ⊢ ((◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅ ↔ (dom ◡((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅)
62	60, 61	mpbir 231	. . . . . . . . 9 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅
63		0fi 9108	. . . . . . . . 9 ⊢ ∅ ∈ Fin
64	62, 63	eqeltri 2840	. . . . . . . 8 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin
65		unfi 9238	. . . . . . . 8 ⊢ (((◡𝑜 “ ℕ) ∈ Fin ∧ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
66	37, 64, 65	sylancl 585	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
67	29, 66	eqeltrid 2848	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin)
68		cnvimass 6111	. . . . . . . . 9 ⊢ (◡𝑜 “ ℕ) ⊆ dom 𝑜
69	68, 2	fssdm 6766	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡𝑜 “ ℕ) ⊆ 𝐽)
70		0ss 4423	. . . . . . . . . 10 ⊢ ∅ ⊆ 𝐽
71	62, 70	eqsstri 4043	. . . . . . . . 9 ⊢ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽
72	71	a1i 11	. . . . . . . 8 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (◡((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽)
73	69, 72	unssd 4215	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((◡𝑜 “ ℕ) ∪ (◡((ℕ ∖ 𝐽) × {0}) “ ℕ)) ⊆ 𝐽)
74	29, 73	eqsstrid 4057	. . . . . 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 34334	. . . . . 6 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ↔ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0 ↑m ℕ) ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin ∧ (◡(𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆ 𝐽))
83	25, 67, 74, 82	syl3anbrc 1343	. . . . 5 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅))
84		resundir 6024	. . . . . 6 ⊢ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽) = ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽))
85		ffn 6747	. . . . . . . 8 ⊢ (𝑜:𝐽⟶ℕ0 → 𝑜 Fn 𝐽)
86		fnresdm 6699	. . . . . . . . 9 ⊢ (𝑜 Fn 𝐽 → (𝑜 ↾ 𝐽) = 𝑜)
87		disjdifr 4496	. . . . . . . . . . 11 ⊢ ((ℕ ∖ 𝐽) ∩ 𝐽) = ∅
88		fnconstg 6809	. . . . . . . . . . . 12 ⊢ (0 ∈ ℕ0 → ((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽))
89		fnresdisj 6700	. . . . . . . . . . . 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 4192	. . . . . . . 8 ⊢ (𝑜 Fn 𝐽 → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
94	2, 85, 93	3syl 18	. . . . . . 7 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
95		un0 4417	. . . . . . 7 ⊢ (𝑜 ∪ ∅) = 𝑜
96	94, 95	eqtrdi 2796	. . . . . 6 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ((𝑜 ↾ 𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = 𝑜)
97	84, 96	eqtr2id 2793	. . . . 5 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
98		reseq1 6003	. . . . . 6 ⊢ (𝑚 = (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) → (𝑚 ↾ 𝐽) = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
99	98	rspceeqv 3658	. . . . 5 ⊢ (((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
100	83, 97, 99	syl2anc 583	. . . 4 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) → ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
101		simpr 484	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 = (𝑚 ↾ 𝐽))
102		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (𝑇 ∩ 𝑅))
103	75, 76, 77, 10, 78, 79, 80, 34, 81	eulerpartlemt0 34334	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↔ (𝑚 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽))
104	102, 103	sylib 218	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ∈ (ℕ0 ↑m ℕ) ∧ (◡𝑚 “ ℕ) ∈ Fin ∧ (◡𝑚 “ ℕ) ⊆ 𝐽))
105	104	simp1d 1142	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚 ∈ (ℕ0 ↑m ℕ))
106	22, 23	elmap 8929	. . . . . . . . . 10 ⊢ (𝑚 ∈ (ℕ0 ↑m ℕ) ↔ 𝑚:ℕ⟶ℕ0)
107	105, 106	sylib 218	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑚:ℕ⟶ℕ0)
108		fssres 6787	. . . . . . . . 9 ⊢ ((𝑚:ℕ⟶ℕ0 ∧ 𝐽 ⊆ ℕ) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
109	107, 12, 108	sylancl 585	. . . . . . . 8 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
110	10, 23	rabex2 5359	. . . . . . . . 9 ⊢ 𝐽 ∈ V
111	22, 110	elmap 8929	. . . . . . . 8 ⊢ ((𝑚 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽) ↔ (𝑚 ↾ 𝐽):𝐽⟶ℕ0)
112	109, 111	sylibr 234	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ (ℕ0 ↑m 𝐽))
113	101, 112	eqeltrd 2844	. . . . . 6 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ (ℕ0 ↑m 𝐽))
114		ffun 6750	. . . . . . . . . 10 ⊢ (𝑚:ℕ⟶ℕ0 → Fun 𝑚)
115		respreima 7099	. . . . . . . . . 10 ⊢ (Fun 𝑚 → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽))
116	107, 114, 115	3syl 18	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) = ((◡𝑚 “ ℕ) ∩ 𝐽))
117	104	simp2d 1143	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡𝑚 “ ℕ) ∈ Fin)
118		infi 9330	. . . . . . . . . 10 ⊢ ((◡𝑚 “ ℕ) ∈ Fin → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
119	117, 118	syl 17	. . . . . . . . 9 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → ((◡𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
120	116, 119	eqeltrd 2844	. . . . . . . 8 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin)
121		vex 3492	. . . . . . . . . 10 ⊢ 𝑚 ∈ V
122	121	resex 6058	. . . . . . . . 9 ⊢ (𝑚 ↾ 𝐽) ∈ V
123		cnveq 5898	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → ◡𝑓 = ◡(𝑚 ↾ 𝐽))
124	123	imaeq1d 6088	. . . . . . . . . 10 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → (◡𝑓 “ ℕ) = (◡(𝑚 ↾ 𝐽) “ ℕ))
125	124	eleq1d 2829	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ↾ 𝐽) → ((◡𝑓 “ ℕ) ∈ Fin ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin))
126	122, 125, 34	elab2 3698	. . . . . . . 8 ⊢ ((𝑚 ↾ 𝐽) ∈ 𝑅 ↔ (◡(𝑚 ↾ 𝐽) “ ℕ) ∈ Fin)
127	120, 126	sylibr 234	. . . . . . 7 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑚 ↾ 𝐽) ∈ 𝑅)
128	101, 127	eqeltrd 2844	. . . . . 6 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → 𝑜 ∈ 𝑅)
129	113, 128	jca 511	. . . . 5 ⊢ ((𝑚 ∈ (𝑇 ∩ 𝑅) ∧ 𝑜 = (𝑚 ↾ 𝐽)) → (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅))
130	129	rexlimiva 3153	. . . 4 ⊢ (∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽) → (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅))
131	100, 130	impbii 209	. . 3 ⊢ ((𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅) ↔ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽))
132	131	abbii 2812	. 2 ⊢ {𝑜 ∣ (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅)} = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)}
133		df-in 3983	. 2 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = {𝑜 ∣ (𝑜 ∈ (ℕ0 ↑m 𝐽) ∧ 𝑜 ∈ 𝑅)}
134		eqid 2740	. . 3 ⊢ (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))
135	134	rnmpt 5980	. 2 ⊢ ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽)) = {𝑜 ∣ ∃𝑚 ∈ (𝑇 ∩ 𝑅)𝑜 = (𝑚 ↾ 𝐽)}
136	132, 133, 135	3eqtr4i 2778	1 ⊢ ((ℕ0 ↑m 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇 ∩ 𝑅) ↦ (𝑚 ↾ 𝐽))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  {cab 2717   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  {crab 3443   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  𝒫 cpw 4622  {csn 4648   class class class wbr 5166  {copab 5228   ↦ cmpt 5249   × cxp 5698  ^◡ccnv 5699  dom cdm 5700  ran crn 5701   ↾ cres 5702   “ cima 5703  Fun wfun 6567   Fn wfn 6568  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450   supp csupp 8201   ↑_m cmap 8884  Fincfn 9003  0cc0 11184  1c1 11185   · cmul 11189   ≤ cle 11325  ℕcn 12293  2c2 12348  ℕ₀cn0 12553  ℤcz 12639  ↑cexp 14112  Σcsu 15734   ∥ cdvds 16302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-neg 11523  df-nn 12294  df-2 12356  df-n0 12554  df-z 12640  df-dvds 16303

This theorem is referenced by:  eulerpartgbij  34337