Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  diophren Structured version   Visualization version   GIF version
Theorem diophren 41853
Description: Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
Assertion
Ref Expression
diophren ((𝑆 ∈ (Diophβ€˜π‘) ∧ 𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
Distinct variable groups:   𝑆,π‘Ž   𝑀,π‘Ž   𝑁,π‘Ž   𝐹,π‘Ž
Proof of Theorem diophren
Dummy variables 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zex 12571 . . . . . 6 β„€ ∈ V
2 difexg 5326 . . . . . 6 (β„€ ∈ V β†’ (β„€ βˆ– β„•) ∈ V)
31, 2ax-mp 5 . . . . 5 (β„€ βˆ– β„•) ∈ V
4 ominf 9260 . . . . . 6 Β¬ Ο‰ ∈ Fin
5 nnuz 12869 . . . . . . . . . 10 β„• = (β„€β‰₯β€˜1)
6 0p1e1 12338 . . . . . . . . . . 11 (0 + 1) = 1
76fveq2i 6893 . . . . . . . . . 10 (β„€β‰₯β€˜(0 + 1)) = (β„€β‰₯β€˜1)
85, 7eqtr4i 2761 . . . . . . . . 9 β„• = (β„€β‰₯β€˜(0 + 1))
98difeq2i 4118 . . . . . . . 8 (β„€ βˆ– β„•) = (β„€ βˆ– (β„€β‰₯β€˜(0 + 1)))
10 0z 12573 . . . . . . . . 9 0 ∈ β„€
11 lzenom 41810 . . . . . . . . 9 (0 ∈ β„€ β†’ (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰)
1210, 11ax-mp 5 . . . . . . . 8 (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰
139, 12eqbrtri 5168 . . . . . . 7 (β„€ βˆ– β„•) β‰ˆ Ο‰
14 enfi 9192 . . . . . . 7 ((β„€ βˆ– β„•) β‰ˆ Ο‰ β†’ ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin))
1513, 14ax-mp 5 . . . . . 6 ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin)
164, 15mtbir 322 . . . . 5 Β¬ (β„€ βˆ– β„•) ∈ Fin
17 disjdifr 4471 . . . . 5 ((β„€ βˆ– β„•) ∩ β„•) = βˆ…
183, 16, 17eldioph4b 41851 . . . 4 (𝑆 ∈ (Diophβ€˜π‘) ↔ (𝑁 ∈ β„•0 ∧ βˆƒπ‘ ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}))
19 simpr 483 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ π‘Ž ∈ (β„•0 ↑m (1...𝑀)))
20 simp-4r 780 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
21 ovex 7444 . . . . . . . . . . . . 13 (1...𝑁) ∈ V
2221mapco2 41755 . . . . . . . . . . . 12 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ (π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)))
2319, 20, 22syl2anc 582 . . . . . . . . . . 11 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ (π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)))
24 uneq1 4155 . . . . . . . . . . . . . 14 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (𝑐 βˆͺ 𝑑) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
2524fveqeq2d 6898 . . . . . . . . . . . . 13 (𝑐 = (π‘Ž ∘ 𝐹) β†’ ((π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2625rexbidv 3176 . . . . . . . . . . . 12 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2726elrab3 3683 . . . . . . . . . . 11 ((π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)) β†’ ((π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2823, 27syl 17 . . . . . . . . . 10 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ ((π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
29 simp-5r 782 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
30 simplr 765 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž ∈ (β„•0 ↑m (1...𝑀)))
31 simpr 483 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)))
32 coundi 6245 . . . . . . . . . . . . . . . 16 ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))))
33 coundir 6246 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹))
34 elmapi 8845 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ 𝑑:(β„€ βˆ– β„•)βŸΆβ„•0)
35343ad2ant3 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑:(β„€ βˆ– β„•)βŸΆβ„•0)
36 simp1 1134 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
37 incom 4200 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = ((1...𝑀) ∩ (β„€ βˆ– β„•))
38 fz1ssnn 13536 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑀) βŠ† β„•
39 disjdif 4470 . . . . . . . . . . . . . . . . . . . . . . . 24 (β„• ∩ (β„€ βˆ– β„•)) = βˆ…
40 ssdisj 4458 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1...𝑀) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…)
4138, 39, 40mp2an 688 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…
4237, 41eqtri 2758 . . . . . . . . . . . . . . . . . . . . . 22 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…
4342a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…)
44 coeq0i 41793 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4535, 36, 43, 44syl3anc 1369 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4645uneq2d 4162 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹)) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
4733, 46eqtrid 2782 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
48 un0 4389 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∘ 𝐹) βˆͺ βˆ…) = (π‘Ž ∘ 𝐹)
4947, 48eqtrdi 2786 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = (π‘Ž ∘ 𝐹))
50 coundir 6246 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))))
51 elmapi 8845 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž ∈ (β„•0 ↑m (1...𝑀)) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
52513ad2ant2 1132 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
53 f1oi 6870 . . . . . . . . . . . . . . . . . . . . . . 23 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•)
54 f1of 6832 . . . . . . . . . . . . . . . . . . . . . . 23 (( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•) β†’ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•))
5553, 54ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•)
56 coeq0i 41793 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž:(1...𝑀)βŸΆβ„•0 ∧ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
5755, 41, 56mp3an23 1451 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž:(1...𝑀)βŸΆβ„•0 β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
5852, 57syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
59 coires1 6262 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (𝑑 β†Ύ (β„€ βˆ– β„•))
60 ffn 6716 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 β†’ 𝑑 Fn (β„€ βˆ– β„•))
61 fnresdm 6668 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 Fn (β„€ βˆ– β„•) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6234, 60, 613syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6359, 62eqtrid 2782 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
64633ad2ant3 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
6558, 64uneq12d 4163 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = (βˆ… βˆͺ 𝑑))
6650, 65eqtrid 2782 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (βˆ… βˆͺ 𝑑))
67 uncom 4152 . . . . . . . . . . . . . . . . . . 19 (βˆ… βˆͺ 𝑑) = (𝑑 βˆͺ βˆ…)
68 un0 4389 . . . . . . . . . . . . . . . . . . 19 (𝑑 βˆͺ βˆ…) = 𝑑
6967, 68eqtri 2758 . . . . . . . . . . . . . . . . . 18 (βˆ… βˆͺ 𝑑) = 𝑑
7066, 69eqtrdi 2786 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
7149, 70uneq12d 4163 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
7232, 71eqtr2id 2783 . . . . . . . . . . . . . . 15 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ 𝑑) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
7329, 30, 31, 72syl3anc 1369 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ 𝑑) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
7473fveq2d 6894 . . . . . . . . . . . . 13 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
75 nn0ssz 12585 . . . . . . . . . . . . . . . . 17 β„•0 βŠ† β„€
76 mapss 8885 . . . . . . . . . . . . . . . . 17 ((β„€ ∈ V ∧ β„•0 βŠ† β„€) β†’ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
771, 75, 76mp2an 688 . . . . . . . . . . . . . . . 16 (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
7841reseq2i 5977 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (π‘Ž β†Ύ βˆ…)
79 res0 5984 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ βˆ…) = βˆ…
8078, 79eqtri 2758 . . . . . . . . . . . . . . . . . 18 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8141reseq2i 5977 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ βˆ…)
82 res0 5984 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ βˆ…) = βˆ…
8381, 82eqtri 2758 . . . . . . . . . . . . . . . . . 18 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8480, 83eqtr4i 2761 . . . . . . . . . . . . . . . . 17 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))
85 elmapresaun 8876 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))))
86 uncom 4152 . . . . . . . . . . . . . . . . . . 19 ((1...𝑀) βˆͺ (β„€ βˆ– β„•)) = ((β„€ βˆ– β„•) βˆͺ (1...𝑀))
8786oveq2i 7422 . . . . . . . . . . . . . . . . . 18 (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))) = (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
8885, 87eleqtrdi 2841 . . . . . . . . . . . . . . . . 17 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
8984, 88mp3an3 1448 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
9077, 89sselid 3979 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
9190adantll 710 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
92 coeq1 5856 . . . . . . . . . . . . . . . 16 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
9392fveq2d 6894 . . . . . . . . . . . . . . 15 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
94 eqid 2730 . . . . . . . . . . . . . . 15 (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) = (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
95 fvex 6903 . . . . . . . . . . . . . . 15 (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) ∈ V
9693, 94, 95fvmpt 6997 . . . . . . . . . . . . . 14 ((π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) β†’ ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
9791, 96syl 17 . . . . . . . . . . . . 13 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
9874, 97eqtr4d 2773 . . . . . . . . . . . 12 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)))
9998eqeq1d 2732 . . . . . . . . . . 11 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0 ↔ ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0))
10099rexbidva 3174 . . . . . . . . . 10 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ (βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0 ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0))
10128, 100bitrd 278 . . . . . . . . 9 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ ((π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0))
102101rabbidva 3437 . . . . . . . 8 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}} = {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0})
103 simplll 771 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ 𝑀 ∈ β„•0)
104 ovex 7444 . . . . . . . . . . . 12 (1...𝑀) ∈ V
1053, 104unex 7735 . . . . . . . . . . 11 ((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V
106105a1i 11 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ ((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V)
107 simpr 483 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁))))
10855a1i 11 . . . . . . . . . . . . 13 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•))
109 id 22 . . . . . . . . . . . . 13 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
110 incom 4200 . . . . . . . . . . . . . . 15 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = ((1...𝑁) ∩ (β„€ βˆ– β„•))
111 fz1ssnn 13536 . . . . . . . . . . . . . . . 16 (1...𝑁) βŠ† β„•
112 ssdisj 4458 . . . . . . . . . . . . . . . 16 (((1...𝑁) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…)
113111, 39, 112mp2an 688 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…
114110, 113eqtri 2758 . . . . . . . . . . . . . 14 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…
115114a1i 11 . . . . . . . . . . . . 13 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…)
116 fun 6752 . . . . . . . . . . . . 13 (((( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
117108, 109, 115, 116syl21anc 834 . . . . . . . . . . . 12 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
118 uncom 4152 . . . . . . . . . . . . 13 (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹) = (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))
119118feq1i 6707 . . . . . . . . . . . 12 ((( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ↔ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
120117, 119sylib 217 . . . . . . . . . . 11 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
121120ad3antlr 727 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
122 mzprename 41789 . . . . . . . . . 10 ((((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁))) ∧ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀))) β†’ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
123106, 107, 121, 122syl3anc 1369 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
1243, 16, 17eldioph4i 41852 . . . . . . . . 9 ((𝑀 ∈ β„•0 ∧ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0} ∈ (Diophβ€˜π‘€))
125103, 123, 124syl2anc 582 . . . . . . . 8 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0} ∈ (Diophβ€˜π‘€))
126102, 125eqeltrd 2831 . . . . . . 7 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}} ∈ (Diophβ€˜π‘€))
127 eleq2 2820 . . . . . . . . 9 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ ((π‘Ž ∘ 𝐹) ∈ 𝑆 ↔ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}))
128127rabbidv 3438 . . . . . . . 8 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} = {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}})
129128eleq1d 2816 . . . . . . 7 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ ({π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€) ↔ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}} ∈ (Diophβ€˜π‘€)))
130126, 129syl5ibrcom 246 . . . . . 6 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€)))
131130rexlimdva 3153 . . . . 5 (((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) β†’ (βˆƒπ‘ ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€)))
132131expimpd 452 . . . 4 ((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ ((𝑁 ∈ β„•0 ∧ βˆƒπ‘ ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€)))
13318, 132biimtrid 241 . . 3 ((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ (𝑆 ∈ (Diophβ€˜π‘) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€)))
134133impcom 406 . 2 ((𝑆 ∈ (Diophβ€˜π‘) ∧ (𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
1351343impb 1113 1 ((𝑆 ∈ (Diophβ€˜π‘) ∧ 𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321   class class class wbr 5147   ↦ cmpt 5230   I cid 5572   β†Ύ cres 5677   ∘ ccom 5679   Fn wfn 6537  βŸΆwf 6538  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  (class class class)co 7411  Ο‰com 7857   ↑m cmap 8822   β‰ˆ cen 8938  Fincfn 8941  0cc0 11112  1c1 11113   + caddc 11115  β„•cn 12216  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  ...cfz 13488  mzPolycmzp 41762  Diophcdioph 41795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-n0 12477  df-z 12563  df-uz 12827  df-fz 13489  df-hash 14295  df-mzpcl 41763  df-mzp 41764  df-dioph 41796
This theorem is referenced by:  rabrenfdioph  41854
  Copyright terms: Public domain W3C validator