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 41165
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 12515 . . . . . 6 β„€ ∈ V
2 difexg 5289 . . . . . 6 (β„€ ∈ V β†’ (β„€ βˆ– β„•) ∈ V)
31, 2ax-mp 5 . . . . 5 (β„€ βˆ– β„•) ∈ V
4 ominf 9209 . . . . . 6 Β¬ Ο‰ ∈ Fin
5 nnuz 12813 . . . . . . . . . 10 β„• = (β„€β‰₯β€˜1)
6 0p1e1 12282 . . . . . . . . . . 11 (0 + 1) = 1
76fveq2i 6850 . . . . . . . . . 10 (β„€β‰₯β€˜(0 + 1)) = (β„€β‰₯β€˜1)
85, 7eqtr4i 2768 . . . . . . . . 9 β„• = (β„€β‰₯β€˜(0 + 1))
98difeq2i 4084 . . . . . . . 8 (β„€ βˆ– β„•) = (β„€ βˆ– (β„€β‰₯β€˜(0 + 1)))
10 0z 12517 . . . . . . . . 9 0 ∈ β„€
11 lzenom 41122 . . . . . . . . 9 (0 ∈ β„€ β†’ (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰)
1210, 11ax-mp 5 . . . . . . . 8 (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰
139, 12eqbrtri 5131 . . . . . . 7 (β„€ βˆ– β„•) β‰ˆ Ο‰
14 enfi 9141 . . . . . . 7 ((β„€ βˆ– β„•) β‰ˆ Ο‰ β†’ ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin))
1513, 14ax-mp 5 . . . . . 6 ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin)
164, 15mtbir 323 . . . . 5 Β¬ (β„€ βˆ– β„•) ∈ Fin
17 disjdifr 4437 . . . . 5 ((β„€ βˆ– β„•) ∩ β„•) = βˆ…
183, 16, 17eldioph4b 41163 . . . 4 (𝑆 ∈ (Diophβ€˜π‘) ↔ (𝑁 ∈ β„•0 ∧ βˆƒπ‘ ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}))
19 simpr 486 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ π‘Ž ∈ (β„•0 ↑m (1...𝑀)))
20 simp-4r 783 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
21 ovex 7395 . . . . . . . . . . . . 13 (1...𝑁) ∈ V
2221mapco2 41067 . . . . . . . . . . . 12 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ (π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)))
2319, 20, 22syl2anc 585 . . . . . . . . . . 11 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ (π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)))
24 uneq1 4121 . . . . . . . . . . . . . 14 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (𝑐 βˆͺ 𝑑) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
2524fveqeq2d 6855 . . . . . . . . . . . . 13 (𝑐 = (π‘Ž ∘ 𝐹) β†’ ((π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2625rexbidv 3176 . . . . . . . . . . . 12 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2726elrab3 3651 . . . . . . . . . . 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 785 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
30 simplr 768 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž ∈ (β„•0 ↑m (1...𝑀)))
31 simpr 486 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)))
32 coundi 6204 . . . . . . . . . . . . . . . 16 ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))))
33 coundir 6205 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹))
34 elmapi 8794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ 𝑑:(β„€ βˆ– β„•)βŸΆβ„•0)
35343ad2ant3 1136 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑:(β„€ βˆ– β„•)βŸΆβ„•0)
36 simp1 1137 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
37 incom 4166 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = ((1...𝑀) ∩ (β„€ βˆ– β„•))
38 fz1ssnn 13479 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑀) βŠ† β„•
39 disjdif 4436 . . . . . . . . . . . . . . . . . . . . . . . 24 (β„• ∩ (β„€ βˆ– β„•)) = βˆ…
40 ssdisj 4424 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1...𝑀) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…)
4138, 39, 40mp2an 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…
4237, 41eqtri 2765 . . . . . . . . . . . . . . . . . . . . . 22 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…
4342a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…)
44 coeq0i 41105 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4535, 36, 43, 44syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4645uneq2d 4128 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹)) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
4733, 46eqtrid 2789 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
48 un0 4355 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∘ 𝐹) βˆͺ βˆ…) = (π‘Ž ∘ 𝐹)
4947, 48eqtrdi 2793 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = (π‘Ž ∘ 𝐹))
50 coundir 6205 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))))
51 elmapi 8794 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž ∈ (β„•0 ↑m (1...𝑀)) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
52513ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
53 f1oi 6827 . . . . . . . . . . . . . . . . . . . . . . 23 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•)
54 f1of 6789 . . . . . . . . . . . . . . . . . . . . . . 23 (( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•) β†’ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•))
5553, 54ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•)
56 coeq0i 41105 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž:(1...𝑀)βŸΆβ„•0 ∧ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
5755, 41, 56mp3an23 1454 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž:(1...𝑀)βŸΆβ„•0 β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
5852, 57syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
59 coires1 6221 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (𝑑 β†Ύ (β„€ βˆ– β„•))
60 ffn 6673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 β†’ 𝑑 Fn (β„€ βˆ– β„•))
61 fnresdm 6625 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 Fn (β„€ βˆ– β„•) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6234, 60, 613syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6359, 62eqtrid 2789 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
64633ad2ant3 1136 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
6558, 64uneq12d 4129 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = (βˆ… βˆͺ 𝑑))
6650, 65eqtrid 2789 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (βˆ… βˆͺ 𝑑))
67 uncom 4118 . . . . . . . . . . . . . . . . . . 19 (βˆ… βˆͺ 𝑑) = (𝑑 βˆͺ βˆ…)
68 un0 4355 . . . . . . . . . . . . . . . . . . 19 (𝑑 βˆͺ βˆ…) = 𝑑
6967, 68eqtri 2765 . . . . . . . . . . . . . . . . . 18 (βˆ… βˆͺ 𝑑) = 𝑑
7066, 69eqtrdi 2793 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
7149, 70uneq12d 4129 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
7232, 71eqtr2id 2790 . . . . . . . . . . . . . . 15 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ 𝑑) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
7329, 30, 31, 72syl3anc 1372 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ 𝑑) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
7473fveq2d 6851 . . . . . . . . . . . . 13 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
75 nn0ssz 12529 . . . . . . . . . . . . . . . . 17 β„•0 βŠ† β„€
76 mapss 8834 . . . . . . . . . . . . . . . . 17 ((β„€ ∈ V ∧ β„•0 βŠ† β„€) β†’ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
771, 75, 76mp2an 691 . . . . . . . . . . . . . . . 16 (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
7841reseq2i 5939 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (π‘Ž β†Ύ βˆ…)
79 res0 5946 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ βˆ…) = βˆ…
8078, 79eqtri 2765 . . . . . . . . . . . . . . . . . 18 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8141reseq2i 5939 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ βˆ…)
82 res0 5946 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ βˆ…) = βˆ…
8381, 82eqtri 2765 . . . . . . . . . . . . . . . . . 18 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8480, 83eqtr4i 2768 . . . . . . . . . . . . . . . . 17 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))
85 elmapresaun 8825 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))))
86 uncom 4118 . . . . . . . . . . . . . . . . . . 19 ((1...𝑀) βˆͺ (β„€ βˆ– β„•)) = ((β„€ βˆ– β„•) βˆͺ (1...𝑀))
8786oveq2i 7373 . . . . . . . . . . . . . . . . . 18 (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))) = (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
8885, 87eleqtrdi 2848 . . . . . . . . . . . . . . . . 17 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
8984, 88mp3an3 1451 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
9077, 89sselid 3947 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
9190adantll 713 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
92 coeq1 5818 . . . . . . . . . . . . . . . 16 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
9392fveq2d 6851 . . . . . . . . . . . . . . 15 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
94 eqid 2737 . . . . . . . . . . . . . . 15 (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) = (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
95 fvex 6860 . . . . . . . . . . . . . . 15 (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) ∈ V
9693, 94, 95fvmpt 6953 . . . . . . . . . . . . . 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 2780 . . . . . . . . . . . 12 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)))
9998eqeq1d 2739 . . . . . . . . . . 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 279 . . . . . . . . 9 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ ((π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0))
102101rabbidva 3417 . . . . . . . 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 774 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ 𝑀 ∈ β„•0)
104 ovex 7395 . . . . . . . . . . . 12 (1...𝑀) ∈ V
1053, 104unex 7685 . . . . . . . . . . 11 ((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V
106105a1i 11 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ ((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V)
107 simpr 486 . . . . . . . . . 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 4166 . . . . . . . . . . . . . . 15 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = ((1...𝑁) ∩ (β„€ βˆ– β„•))
111 fz1ssnn 13479 . . . . . . . . . . . . . . . 16 (1...𝑁) βŠ† β„•
112 ssdisj 4424 . . . . . . . . . . . . . . . 16 (((1...𝑁) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…)
113111, 39, 112mp2an 691 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…
114110, 113eqtri 2765 . . . . . . . . . . . . . 14 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…
115114a1i 11 . . . . . . . . . . . . 13 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…)
116 fun 6709 . . . . . . . . . . . . 13 (((( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
117108, 109, 115, 116syl21anc 837 . . . . . . . . . . . 12 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
118 uncom 4118 . . . . . . . . . . . . 13 (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹) = (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))
119118feq1i 6664 . . . . . . . . . . . 12 ((( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ↔ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
120117, 119sylib 217 . . . . . . . . . . 11 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
121120ad3antlr 730 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
122 mzprename 41101 . . . . . . . . . 10 ((((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁))) ∧ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀))) β†’ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
123106, 107, 121, 122syl3anc 1372 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
1243, 16, 17eldioph4i 41164 . . . . . . . . 9 ((𝑀 ∈ β„•0 ∧ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0} ∈ (Diophβ€˜π‘€))
125103, 123, 124syl2anc 585 . . . . . . . 8 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0} ∈ (Diophβ€˜π‘€))
126102, 125eqeltrd 2838 . . . . . . 7 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}} ∈ (Diophβ€˜π‘€))
127 eleq2 2827 . . . . . . . . 9 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ ((π‘Ž ∘ 𝐹) ∈ 𝑆 ↔ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}))
128127rabbidv 3418 . . . . . . . 8 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} = {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}})
129128eleq1d 2823 . . . . . . 7 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ ({π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€) ↔ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}} ∈ (Diophβ€˜π‘€)))
130126, 129syl5ibrcom 247 . . . . . 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 455 . . . 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 409 . 2 ((𝑆 ∈ (Diophβ€˜π‘) ∧ (𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
1351343impb 1116 1 ((𝑆 ∈ (Diophβ€˜π‘) ∧ 𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆƒwrex 3074  {crab 3410  Vcvv 3448   βˆ– cdif 3912   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287   class class class wbr 5110   ↦ cmpt 5193   I cid 5535   β†Ύ cres 5640   ∘ ccom 5642   Fn wfn 6496  βŸΆwf 6497  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501  (class class class)co 7362  Ο‰com 7807   ↑m cmap 8772   β‰ˆ cen 8887  Fincfn 8890  0cc0 11058  1c1 11059   + caddc 11061  β„•cn 12160  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  ...cfz 13431  mzPolycmzp 41074  Diophcdioph 41107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-n0 12421  df-z 12507  df-uz 12771  df-fz 13432  df-hash 14238  df-mzpcl 41075  df-mzp 41076  df-dioph 41108
This theorem is referenced by:  rabrenfdioph  41166
  Copyright terms: Public domain W3C validator