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 biimpi ⊢ ( 𝑜 ∈ 𝑅 → ( ◡ 𝑜 “ ℕ ) ∈ Fin )
44 43 adantl ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ 𝑜 “ ℕ ) ∈ Fin )
45 cnvxp ⊢ ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) = ( { 0 } × ( ℕ ∖ 𝐽 ) )
46 45 dmeqi ⊢ dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) = dom ( { 0 } × ( ℕ ∖ 𝐽 ) )
47 2nn ⊢ 2 ∈ ℕ
48 2z ⊢ 2 ∈ ℤ
49 iddvds ⊢ ( 2 ∈ ℤ → 2 ∥ 2 )
50 48 49 ax-mp ⊢ 2 ∥ 2
51 breq2 ⊢ ( 𝑧 = 2 → ( 2 ∥ 𝑧 ↔ 2 ∥ 2 ) )
52 51 notbid ⊢ ( 𝑧 = 2 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 2 ) )
53 52 4 elrab2 ⊢ ( 2 ∈ 𝐽 ↔ ( 2 ∈ ℕ ∧ ¬ 2 ∥ 2 ) )
54 53 simprbi ⊢ ( 2 ∈ 𝐽 → ¬ 2 ∥ 2 )
55 50 54 mt2 ⊢ ¬ 2 ∈ 𝐽
56 eldif ⊢ ( 2 ∈ ( ℕ ∖ 𝐽 ) ↔ ( 2 ∈ ℕ ∧ ¬ 2 ∈ 𝐽 ) )
57 47 55 56 mpbir2an ⊢ 2 ∈ ( ℕ ∖ 𝐽 )
58 ne0i ⊢ ( 2 ∈ ( ℕ ∖ 𝐽 ) → ( ℕ ∖ 𝐽 ) ≠ ∅ )
59 dmxp ⊢ ( ( ℕ ∖ 𝐽 ) ≠ ∅ → dom ( { 0 } × ( ℕ ∖ 𝐽 ) ) = { 0 } )
60 57 58 59 mp2b ⊢ dom ( { 0 } × ( ℕ ∖ 𝐽 ) ) = { 0 }
61 46 60 eqtri ⊢ dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) = { 0 }
62 61 ineq1i ⊢ ( dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ∩ ℕ ) = ( { 0 } ∩ ℕ )
63 incom ⊢ ( ℕ ∩ { 0 } ) = ( { 0 } ∩ ℕ )
64 0nnn ⊢ ¬ 0 ∈ ℕ
65 disjsn ⊢ ( ( ℕ ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ℕ )
66 64 65 mpbir ⊢ ( ℕ ∩ { 0 } ) = ∅
67 62 63 66 3eqtr2i ⊢ ( dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ∩ ℕ ) = ∅
68 imadisj ⊢ ( ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) = ∅ ↔ ( dom ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ∩ ℕ ) = ∅ )
69 67 68 mpbir ⊢ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) = ∅
70 0fin ⊢ ∅ ∈ Fin
71 69 70 eqeltri ⊢ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ∈ Fin
72 unfi ⊢ ( ( ( ◡ 𝑜 “ ℕ ) ∈ Fin ∧ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ∈ Fin ) → ( ( ◡ 𝑜 “ ℕ ) ∪ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ) ∈ Fin )
73 44 71 72 sylancl ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( ◡ 𝑜 “ ℕ ) ∪ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ) ∈ Fin )
74 37 73 eqeltrid ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) ∈ Fin )
75 cnvimass ⊢ ( ◡ 𝑜 “ ℕ ) ⊆ dom 𝑜
76 75 11 fssdm ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ 𝑜 “ ℕ ) ⊆ 𝐽 )
77 0ss ⊢ ∅ ⊆ 𝐽
78 69 77 eqsstri ⊢ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ⊆ 𝐽
79 78 a1i ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ⊆ 𝐽 )
80 76 79 unssd ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( ◡ 𝑜 “ ℕ ) ∪ ( ◡ ( ( ℕ ∖ 𝐽 ) × { 0 } ) “ ℕ ) ) ⊆ 𝐽 )
81 37 80 eqsstrid ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) ⊆ 𝐽 )
82 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ⊢ ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) ∈ Fin ∧ ( ◡ ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) “ ℕ ) ⊆ 𝐽 ) )
83 33 74 81 82 syl3anbrc ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( 𝑇 ∩ 𝑅 ) )
84 resundir ⊢ ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ↾ 𝐽 ) = ( ( 𝑜 ↾ 𝐽 ) ∪ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) )
85 ffn ⊢ ( 𝑜 : 𝐽 ⟶ ℕ0 → 𝑜 Fn 𝐽 )
86 fnresdm ⊢ ( 𝑜 Fn 𝐽 → ( 𝑜 ↾ 𝐽 ) = 𝑜 )
87 incom ⊢ ( ( ℕ ∖ 𝐽 ) ∩ 𝐽 ) = ( 𝐽 ∩ ( ℕ ∖ 𝐽 ) )
88 87 15 eqtri ⊢ ( ( ℕ ∖ 𝐽 ) ∩ 𝐽 ) = ∅
89 fnconstg ⊢ ( 0 ∈ ℕ0 → ( ( ℕ ∖ 𝐽 ) × { 0 } ) Fn ( ℕ ∖ 𝐽 ) )
90 fnresdisj ⊢ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) Fn ( ℕ ∖ 𝐽 ) → ( ( ( ℕ ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ↔ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) = ∅ ) )
91 23 89 90 mp2b ⊢ ( ( ( ℕ ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ↔ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) = ∅ )
92 88 91 mpbi ⊢ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) = ∅
93 92 a1i ⊢ ( 𝑜 Fn 𝐽 → ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) = ∅ )
94 86 93 uneq12d ⊢ ( 𝑜 Fn 𝐽 → ( ( 𝑜 ↾ 𝐽 ) ∪ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) ) = ( 𝑜 ∪ ∅ ) )
95 11 85 94 3syl ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( 𝑜 ↾ 𝐽 ) ∪ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) ) = ( 𝑜 ∪ ∅ ) )
96 un0 ⊢ ( 𝑜 ∪ ∅ ) = 𝑜
97 95 96 eqtrdi ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ( ( 𝑜 ↾ 𝐽 ) ∪ ( ( ( ℕ ∖ 𝐽 ) × { 0 } ) ↾ 𝐽 ) ) = 𝑜 )
98 84 97 syl5req ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → 𝑜 = ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ↾ 𝐽 ) )
99 reseq1 ⊢ ( 𝑚 = ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) → ( 𝑚 ↾ 𝐽 ) = ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ↾ 𝐽 ) )
100 99 rspceeqv ⊢ ( ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( ( 𝑜 ∪ ( ( ℕ ∖ 𝐽 ) × { 0 } ) ) ↾ 𝐽 ) ) → ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) )
101 83 98 100 syl2anc ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) → ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) )
102 simpr ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑜 = ( 𝑚 ↾ 𝐽 ) )
103 simpl ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) )
104 1 2 3 4 5 6 7 8 9 eulerpartlemt0 ⊢ ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( 𝑚 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝑚 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑚 “ ℕ ) ⊆ 𝐽 ) )
105 103 104 sylib ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑚 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ 𝑚 “ ℕ ) ∈ Fin ∧ ( ◡ 𝑚 “ ℕ ) ⊆ 𝐽 ) )
106 105 simp1d ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑚 ∈ ( ℕ0 ↑m ℕ ) )
107 30 31 elmap ⊢ ( 𝑚 ∈ ( ℕ0 ↑m ℕ ) ↔ 𝑚 : ℕ ⟶ ℕ0 )
108 106 107 sylib ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑚 : ℕ ⟶ ℕ0 )
109 fssres ⊢ ( ( 𝑚 : ℕ ⟶ ℕ0 ∧ 𝐽 ⊆ ℕ ) → ( 𝑚 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
110 108 20 109 sylancl ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑚 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
111 4 31 rabex2 ⊢ 𝐽 ∈ V
112 30 111 elmap ⊢ ( ( 𝑚 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) ↔ ( 𝑚 ↾ 𝐽 ) : 𝐽 ⟶ ℕ0 )
113 110 112 sylibr ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑚 ↾ 𝐽 ) ∈ ( ℕ0 ↑m 𝐽 ) )
114 102 113 eqeltrd ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) )
115 ffun ⊢ ( 𝑚 : ℕ ⟶ ℕ0 → Fun 𝑚 )
116 respreima ⊢ ( Fun 𝑚 → ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) = ( ( ◡ 𝑚 “ ℕ ) ∩ 𝐽 ) )
117 108 115 116 3syl ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) = ( ( ◡ 𝑚 “ ℕ ) ∩ 𝐽 ) )
118 105 simp2d ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( ◡ 𝑚 “ ℕ ) ∈ Fin )
119 infi ⊢ ( ( ◡ 𝑚 “ ℕ ) ∈ Fin → ( ( ◡ 𝑚 “ ℕ ) ∩ 𝐽 ) ∈ Fin )
120 118 119 syl ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( ( ◡ 𝑚 “ ℕ ) ∩ 𝐽 ) ∈ Fin )
121 117 120 eqeltrd ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) ∈ Fin )
122 vex ⊢ 𝑚 ∈ V
123 122 resex ⊢ ( 𝑚 ↾ 𝐽 ) ∈ V
124 cnveq ⊢ ( 𝑓 = ( 𝑚 ↾ 𝐽 ) → ◡ 𝑓 = ◡ ( 𝑚 ↾ 𝐽 ) )
125 124 imaeq1d ⊢ ( 𝑓 = ( 𝑚 ↾ 𝐽 ) → ( ◡ 𝑓 “ ℕ ) = ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) )
126 125 eleq1d ⊢ ( 𝑓 = ( 𝑚 ↾ 𝐽 ) → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) ∈ Fin ) )
127 123 126 8 elab2 ⊢ ( ( 𝑚 ↾ 𝐽 ) ∈ 𝑅 ↔ ( ◡ ( 𝑚 ↾ 𝐽 ) “ ℕ ) ∈ Fin )
128 121 127 sylibr ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑚 ↾ 𝐽 ) ∈ 𝑅 )
129 102 128 eqeltrd ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → 𝑜 ∈ 𝑅 )
130 114 129 jca ⊢ ( ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ∧ 𝑜 = ( 𝑚 ↾ 𝐽 ) ) → ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) )
131 130 rexlimiva ⊢ ( ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) → ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) )
132 101 131 impbii ⊢ ( ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) ↔ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) )
133 132 abbii ⊢ { 𝑜 ∣ ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) } = { 𝑜 ∣ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) }
134 df-in ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = { 𝑜 ∣ ( 𝑜 ∈ ( ℕ0 ↑m 𝐽 ) ∧ 𝑜 ∈ 𝑅 ) }
135 eqid ⊢ ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) ) = ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) )
136 135 rnmpt ⊢ ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) ) = { 𝑜 ∣ ∃ 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) 𝑜 = ( 𝑚 ↾ 𝐽 ) }
137 133 134 136 3eqtr4i ⊢ ( ( ℕ0 ↑m 𝐽 ) ∩ 𝑅 ) = ran ( 𝑚 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( 𝑚 ↾ 𝐽 ) )