Metamath Proof Explorer

Theorem eulerpartlemt

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

Ref Expression
Hypotheses 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 eulerpartlemt ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2 eulerpart.o ⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3 eulerpart.d ⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
4 eulerpart.j ⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
5 eulerpart.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
6 eulerpart.h ⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
7 eulerpart.m ⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
8 eulerpart.r ⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
9 eulerpart.t ⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
10 elmapi ⊢ ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) → 𝑜 : 𝐽 ⟶ ℕ0 )
11 10 adantr ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → 𝑜 : 𝐽 ⟶ ℕ0 )
12 c0ex ⊢ 0 ∈ V
13 12 fconst ⊢ ( ( ℕ ∖ 𝐽 ) × { 0 } ) : ( ℕ ∖ 𝐽 ) ⟶ { 0 }
14 13 a1i ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( ℕ ∖ 𝐽 ) × { 0 } ) : ( ℕ ∖ 𝐽 ) ⟶ { 0 } )
15 disjdif ⊢ ( 𝐽 ∩ ( ℕ ∖ 𝐽 ) ) = ∅
16 15 a1i ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( 𝐽 ∩ ( ℕ ∖ 𝐽 ) ) = ∅ )
17 fun ⊢ ( ( ( 𝑜 : 𝐽 ⟶ ℕ0 ∧ ( ( ℕ ∖ 𝐽 ) × { 0 } ) : ( ℕ ∖ 𝐽 ) ⟶ { 0 } ) ∧ ( 𝐽 ∩ ( ℕ ∖ 𝐽 ) ) = ∅ ) → ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) : ( 𝐽 ∪ ( ℕ ∖ 𝐽 ) ) ⟶ ( ℕ0 ∪ { 0 } ) )
18 11 14 16 17 syl21anc ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) : ( 𝐽 ∪ ( ℕ ∖ 𝐽 ) ) ⟶ ( ℕ0 ∪ { 0 } ) )
19 ssrab2 ⊢ { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 } ⊆ ℕ
20 4 19 eqsstri ⊢ 𝐽 ⊆ ℕ
21 undif ⊢ ( 𝐽 ⊆ ℕ ↔ ( 𝐽 ∪ ( ℕ ∖ 𝐽 ) ) = ℕ )
22 20 21 mpbi ⊢ ( 𝐽 ∪ ( ℕ ∖ 𝐽 ) ) = ℕ
23 0nn0 ⊢ 0 ∈ ℕ0
24 snssi ⊢ ( 0 ∈ ℕ0 → { 0 } ⊆ ℕ0 )
25 23 24 ax-mp ⊢ { 0 } ⊆ ℕ0
26 ssequn2 ⊢ ( { 0 } ⊆ ℕ0 ↔ ( ℕ0 ∪ { 0 } ) = ℕ0 )
27 25 26 mpbi ⊢ ( ℕ0 ∪ { 0 } ) = ℕ0
28 22 27 feq23i ⊢ ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) : ( 𝐽 ∪ ( ℕ ∖ 𝐽 ) ) ⟶ ( ℕ0 ∪ { 0 } ) ↔ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) : ℕ ⟶ ℕ0 )
29 18 28 sylib ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) : ℕ ⟶ ℕ0 )
30 nn0ex ⊢ ℕ0 ∈ V
31 nnex ⊢ ℕ ∈ V
32 30 31 elmap ⊢ ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( ℕ0 ↑m ℕ ) ↔ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) : ℕ ⟶ ℕ0 )
33 29 32 sylibr ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( ℕ0 ↑m ℕ ) )
34 cnvun ⊢ ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) = ( ◡ 𝑜 ∪ ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) )
35 34 imaeq1i ⊢ ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) = ( ( ◡ 𝑜 ∪ ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ )
36 imaundir ⊢ ( ( ◡ 𝑜 ∪ ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) = ( ( ◡ 𝑜 “ ℕ ) ∪ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) )
37 35 36 eqtri ⊢ ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) = ( ( ◡ 𝑜 “ ℕ ) ∪ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) )
38 vex ⊢ 𝑜 ∈ V
39 cnveq ⊢ ( 𝑓 = 𝑜 → ◡ 𝑓 = ◡ 𝑜 )
40 39 imaeq1d ⊢ ( 𝑓 = 𝑜 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝑜 “ ℕ ) )
41 40 eleq1d ⊢ ( 𝑓 = 𝑜 → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ 𝑜 “ ℕ ) ∈ Fin ) )
42 38 41 8 elab2 ⊢ ( 𝑜 ∈ 𝑅 ↔ ( ◡ 𝑜 “ ℕ ) ∈ Fin )
43 42 bilani ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ 𝑜 “ ℕ ) ∈ Fin )
44 cnvxp ⊢ ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) = ( { 0 } × ( ℕ ∖ 𝐽 ) )
45 44 dmeqi ⊢ dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) = dom ( { 0 } × ( ℕ ∖ 𝐽 ) )
46 2nn ⊢ 2 ∈ ℕ
47 2z ⊢ 2 ∈ ℤ
48 iddvds ⊢ ( 2 ∈ ℤ → 2 ∥ 2 )
49 47 48 ax-mp ⊢ 2 ∥ 2
50 breq2 ⊢ ( 𝑧 = 2 → ( 2 ∥ 𝑧 ↔ 2 ∥ 2 ) )
51 50 notbid ⊢ ( 𝑧 = 2 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 2 ) )
52 51 4 elrab2 ⊢ ( 2 ∈ 𝐽 ↔ ( 2 ∈ ℕ ∧ ¬ 2 ∥ 2 ) )
53 52 simprbi ⊢ ( 2 ∈ 𝐽 → ¬ 2 ∥ 2 )
54 49 53 mt2 ⊢ ¬ 2 ∈ 𝐽
55 eldif ⊢ ( 2 ∈ ( ℕ ∖ 𝐽 ) ↔ ( 2 ∈ ℕ ∧ ¬ 2 ∈ 𝐽 ) )
56 46 54 55 mpbir2an ⊢ 2 ∈ ( ℕ ∖ 𝐽 )
57 ne0i ⊢ ( 2 ∈ ( ℕ ∖ 𝐽 ) → ( ℕ ∖ 𝐽 ) ≠ ∅ )
58 dmxp ⊢ ( ( ℕ ∖ 𝐽 ) ≠ ∅ → dom ( { 0 } × ( ℕ ∖ 𝐽 ) ) = { 0 } )
59 56 57 58 mp2b ⊢ dom ( { 0 } × ( ℕ ∖ 𝐽 ) ) = { 0 }
60 45 59 eqtri ⊢ dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) = { 0 }
61 60 ineq1i ⊢ ( dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ∩ ℕ ) = ( { 0 } ∩ ℕ )
62 incom ⊢ ( ℕ ∩ { 0 } ) = ( { 0 } ∩ ℕ )
63 0nnn ⊢ ¬ 0 ∈ ℕ
64 disjsn ⊢ ( ( ℕ ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ℕ )
65 63 64 mpbir ⊢ ( ℕ ∩ { 0 } ) = ∅
66 61 62 65 3eqtr2i ⊢ ( dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ∩ ℕ ) = ∅
67 imadisj ⊢ ( ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) = ∅ ↔ ( dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ∩ ℕ ) = ∅ )
68 66 67 mpbir ⊢ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) = ∅
69 0fi ⊢ ∅ ∈ Fin
70 68 69 eqeltri ⊢ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ∈ Fin
71 unfi ⊢ ( ( ( ◡ 𝑜 “ ℕ ) ∈ Fin ∧ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ∈ Fin ) → ( ( ◡ 𝑜 “ ℕ ) ∪ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ) ∈ Fin )
72 43 70 71 sylancl ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( ◡ 𝑜 “ ℕ ) ∪ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ) ∈ Fin )
73 37 72 eqeltrid ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) ∈ Fin )
74 cnvimass ⊢ ( ◡ 𝑜 “ ℕ ) ⊆ dom 𝑜
75 74 11 fssdm ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ 𝑜 “ ℕ ) ⊆ 𝐽 )
76 0ss ⊢ ∅ ⊆ 𝐽
77 68 76 eqsstri ⊢ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ⊆ 𝐽
78 77 a1i ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ⊆ 𝐽 )
79 75 78 unssd ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( ◡ 𝑜 “ ℕ ) ∪ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ) ⊆ 𝐽 )
80 37 79 eqsstrid ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) ⊆ 𝐽 )
81 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ⊢ ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) ∈ Fin ∧ ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) ⊆ 𝐽 ) )
82 33 73 80 81 syl3anbrc ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( 𝑇 ∩ 𝑅 ) )
83 resundir ⊢ ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ↾ 𝐽 ) = ( ( 𝑜 ↾ 𝐽 ) ∪ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) )
84 ffn ⊢ ( 𝑜 : 𝐽 ⟶ ℕ0 → 𝑜 Fn 𝐽 )
85 fnresdm ⊢ ( 𝑜 Fn 𝐽 → ( 𝑜 ↾ 𝐽 ) = 𝑜 )
86 disjdifr ⊢ ( ( ℕ ∖ 𝐽 ) ∩ 𝐽 ) = ∅
87 fnconstg ⊢ ( 0 ∈ ℕ0 → ( ( ℕ ∖ 𝐽 ) × { 0 } ) Fn ( ℕ ∖ 𝐽 ) )
88 fnresdisj ⊢ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) Fn ( ℕ ∖ 𝐽 ) → ( ( ( ℕ ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ↔ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) = ∅ ) )
89 23 87 88 mp2b ⊢ ( ( ( ℕ ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ↔ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) = ∅ )
90 86 89 mpbi ⊢ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) = ∅
91 90 a1i ⊢ ( 𝑜 Fn 𝐽 → ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) = ∅ )
92 85 91 uneq12d ⊢ ( 𝑜 Fn 𝐽 → ( ( 𝑜 ↾ 𝐽 ) ∪ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) ) = ( 𝑜 ∪ ∅ ) )
93 11 84 92 3syl ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( 𝑜 ↾ 𝐽 ) ∪ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) ) = ( 𝑜 ∪ ∅ ) )
94 un0 ⊢ ( 𝑜 ∪ ∅ ) = 𝑜
95 93 94 eqtrdi ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( 𝑜 ↾ 𝐽 ) ∪ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) ) = 𝑜 )
96 83 95 eqtr2id ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → 𝑜 = ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ↾ 𝐽 ) )
97 reseq1 ⊢ ( 𝑚 = ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) → ( 𝑚 ↾ 𝐽 ) = ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ↾ 𝐽 ) )
98 97 rspceeqv ⊢ ( ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ↾ 𝐽 ) ) → ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) )
99 82 96 98 syl2anc ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) )
100 simpr ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑜 = ( 𝑚 ↾ 𝐽 ) )
101 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ⊢ ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝑚 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝑚 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑚 “ ℕ ) ⊆ 𝐽 ) )
102 101 birani ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑚 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝑚 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑚 “ ℕ ) ⊆ 𝐽 ) )
103 102 simp1d ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑚 ∈ ( ℕ0 ↑m ℕ ) )
104 30 31 elmap ⊢ ( 𝑚 ∈ ( ℕ0 ↑m ℕ ) ↔ 𝑚 : ℕ ⟶ ℕ0 )
105 103 104 sylib ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑚 : ℕ ⟶ ℕ0 )
106 fssres ⊢ ( ( 𝑚 : ℕ ⟶ ℕ0 ∧ 𝐽 ⊆ ℕ ) → ( 𝑚 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
107 105 20 106 sylancl ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑚 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
108 4 31 rabex2 ⊢ 𝐽 ∈ V
109 30 108 elmap ⊢ ( ( 𝑚 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) ↔ ( 𝑚 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
110 107 109 sylibr ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑚 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) )
111 100 110 eqeltrd ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) )
112 ffun ⊢ ( 𝑚 : ℕ ⟶ ℕ0 → Fun 𝑚 )
113 respreima ⊢ ( Fun 𝑚 → ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) = ( ( ◡ 𝑚 “ ℕ ) ∩ 𝐽 ) )
114 105 112 113 3syl ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) = ( ( ◡ 𝑚 “ ℕ ) ∩ 𝐽 ) )
115 102 simp2d ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( ◡ 𝑚 “ ℕ ) ∈ Fin )
116 infi ⊢ ( ( ◡ 𝑚 “ ℕ ) ∈ Fin → ( ( ◡ 𝑚 “ ℕ ) ∩ 𝐽 ) ∈ Fin )
117 115 116 syl ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( ( ◡ 𝑚 “ ℕ ) ∩ 𝐽 ) ∈ Fin )
118 114 117 eqeltrd ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) ∈ Fin )
119 vex ⊢ 𝑚 ∈ V
120 119 resex ⊢ ( 𝑚 ↾ 𝐽 ) ∈ V
121 cnveq ⊢ ( 𝑓 = ( 𝑚 ↾ 𝐽 ) → ◡ 𝑓 = ◡ ( 𝑚 ↾ 𝐽 ) )
122 121 imaeq1d ⊢ ( 𝑓 = ( 𝑚 ↾ 𝐽 ) → ( ◡ 𝑓 “ ℕ ) = ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) )
123 122 eleq1d ⊢ ( 𝑓 = ( 𝑚 ↾ 𝐽 ) → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) ∈ Fin ) )
124 120 123 8 elab2 ⊢ ( ( 𝑚 ↾ 𝐽 ) ∈ 𝑅 ↔ ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) ∈ Fin )
125 118 124 sylibr ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑚 ↾ 𝐽 ) ∈ 𝑅 )
126 100 125 eqeltrd ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑜 ∈ 𝑅 )
127 111 126 jca ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) )
128 127 rexlimiva ⊢ ( ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) → ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) )
129 99 128 impbii ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) ↔ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) )
130 129 abbii ⊢ { 𝑜 ∣ ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) } = { 𝑜 ∣ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) }
131 df-in ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = { 𝑜 ∣ ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) }
132 eqid ⊢ ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) ) = ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) )
133 132 rnmpt ⊢ ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) ) = { 𝑜 ∣ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) }
134 130 131 133 3eqtr4i ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) )