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 41536
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 12563 . . . . . 6 β„€ ∈ V
2 difexg 5326 . . . . . 6 (β„€ ∈ V β†’ (β„€ βˆ– β„•) ∈ V)
31, 2ax-mp 5 . . . . 5 (β„€ βˆ– β„•) ∈ V
4 ominf 9254 . . . . . 6 Β¬ Ο‰ ∈ Fin
5 nnuz 12861 . . . . . . . . . 10 β„• = (β„€β‰₯β€˜1)
6 0p1e1 12330 . . . . . . . . . . 11 (0 + 1) = 1
76fveq2i 6891 . . . . . . . . . 10 (β„€β‰₯β€˜(0 + 1)) = (β„€β‰₯β€˜1)
85, 7eqtr4i 2763 . . . . . . . . 9 β„• = (β„€β‰₯β€˜(0 + 1))
98difeq2i 4118 . . . . . . . 8 (β„€ βˆ– β„•) = (β„€ βˆ– (β„€β‰₯β€˜(0 + 1)))
10 0z 12565 . . . . . . . . 9 0 ∈ β„€
11 lzenom 41493 . . . . . . . . 9 (0 ∈ β„€ β†’ (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰)
1210, 11ax-mp 5 . . . . . . . 8 (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰
139, 12eqbrtri 5168 . . . . . . 7 (β„€ βˆ– β„•) β‰ˆ Ο‰
14 enfi 9186 . . . . . . 7 ((β„€ βˆ– β„•) β‰ˆ Ο‰ β†’ ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin))
1513, 14ax-mp 5 . . . . . 6 ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin)
164, 15mtbir 322 . . . . 5 Β¬ (β„€ βˆ– β„•) ∈ Fin
17 disjdifr 4471 . . . . 5 ((β„€ βˆ– β„•) ∩ β„•) = βˆ…
183, 16, 17eldioph4b 41534 . . . 4 (𝑆 ∈ (Diophβ€˜π‘) ↔ (𝑁 ∈ β„•0 ∧ βˆƒπ‘ ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}))
19 simpr 485 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ π‘Ž ∈ (β„•0 ↑m (1...𝑀)))
20 simp-4r 782 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
21 ovex 7438 . . . . . . . . . . . . 13 (1...𝑁) ∈ V
2221mapco2 41438 . . . . . . . . . . . 12 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ (π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)))
2319, 20, 22syl2anc 584 . . . . . . . . . . 11 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ (π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)))
24 uneq1 4155 . . . . . . . . . . . . . 14 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (𝑐 βˆͺ 𝑑) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
2524fveqeq2d 6896 . . . . . . . . . . . . 13 (𝑐 = (π‘Ž ∘ 𝐹) β†’ ((π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2625rexbidv 3178 . . . . . . . . . . . 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 784 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
30 simplr 767 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž ∈ (β„•0 ↑m (1...𝑀)))
31 simpr 485 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)))
32 coundi 6243 . . . . . . . . . . . . . . . 16 ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))))
33 coundir 6244 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹))
34 elmapi 8839 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ 𝑑:(β„€ βˆ– β„•)βŸΆβ„•0)
35343ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑:(β„€ βˆ– β„•)βŸΆβ„•0)
36 simp1 1136 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
37 incom 4200 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = ((1...𝑀) ∩ (β„€ βˆ– β„•))
38 fz1ssnn 13528 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑀) βŠ† β„•
39 disjdif 4470 . . . . . . . . . . . . . . . . . . . . . . . 24 (β„• ∩ (β„€ βˆ– β„•)) = βˆ…
40 ssdisj 4458 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1...𝑀) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…)
4138, 39, 40mp2an 690 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…
4237, 41eqtri 2760 . . . . . . . . . . . . . . . . . . . . . 22 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…
4342a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…)
44 coeq0i 41476 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4535, 36, 43, 44syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4645uneq2d 4162 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹)) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
4733, 46eqtrid 2784 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
48 un0 4389 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∘ 𝐹) βˆͺ βˆ…) = (π‘Ž ∘ 𝐹)
4947, 48eqtrdi 2788 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = (π‘Ž ∘ 𝐹))
50 coundir 6244 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))))
51 elmapi 8839 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž ∈ (β„•0 ↑m (1...𝑀)) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
52513ad2ant2 1134 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
53 f1oi 6868 . . . . . . . . . . . . . . . . . . . . . . 23 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•)
54 f1of 6830 . . . . . . . . . . . . . . . . . . . . . . 23 (( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•) β†’ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•))
5553, 54ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•)
56 coeq0i 41476 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž:(1...𝑀)βŸΆβ„•0 ∧ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
5755, 41, 56mp3an23 1453 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž:(1...𝑀)βŸΆβ„•0 β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
5852, 57syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
59 coires1 6260 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (𝑑 β†Ύ (β„€ βˆ– β„•))
60 ffn 6714 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 β†’ 𝑑 Fn (β„€ βˆ– β„•))
61 fnresdm 6666 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 Fn (β„€ βˆ– β„•) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6234, 60, 613syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6359, 62eqtrid 2784 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
64633ad2ant3 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
6558, 64uneq12d 4163 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = (βˆ… βˆͺ 𝑑))
6650, 65eqtrid 2784 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (βˆ… βˆͺ 𝑑))
67 uncom 4152 . . . . . . . . . . . . . . . . . . 19 (βˆ… βˆͺ 𝑑) = (𝑑 βˆͺ βˆ…)
68 un0 4389 . . . . . . . . . . . . . . . . . . 19 (𝑑 βˆͺ βˆ…) = 𝑑
6967, 68eqtri 2760 . . . . . . . . . . . . . . . . . 18 (βˆ… βˆͺ 𝑑) = 𝑑
7066, 69eqtrdi 2788 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
7149, 70uneq12d 4163 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
7232, 71eqtr2id 2785 . . . . . . . . . . . . . . 15 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ 𝑑) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
7329, 30, 31, 72syl3anc 1371 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ 𝑑) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
7473fveq2d 6892 . . . . . . . . . . . . 13 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
75 nn0ssz 12577 . . . . . . . . . . . . . . . . 17 β„•0 βŠ† β„€
76 mapss 8879 . . . . . . . . . . . . . . . . 17 ((β„€ ∈ V ∧ β„•0 βŠ† β„€) β†’ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
771, 75, 76mp2an 690 . . . . . . . . . . . . . . . 16 (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
7841reseq2i 5976 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (π‘Ž β†Ύ βˆ…)
79 res0 5983 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ βˆ…) = βˆ…
8078, 79eqtri 2760 . . . . . . . . . . . . . . . . . 18 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8141reseq2i 5976 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ βˆ…)
82 res0 5983 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ βˆ…) = βˆ…
8381, 82eqtri 2760 . . . . . . . . . . . . . . . . . 18 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8480, 83eqtr4i 2763 . . . . . . . . . . . . . . . . 17 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))
85 elmapresaun 8870 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))))
86 uncom 4152 . . . . . . . . . . . . . . . . . . 19 ((1...𝑀) βˆͺ (β„€ βˆ– β„•)) = ((β„€ βˆ– β„•) βˆͺ (1...𝑀))
8786oveq2i 7416 . . . . . . . . . . . . . . . . . 18 (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))) = (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
8885, 87eleqtrdi 2843 . . . . . . . . . . . . . . . . 17 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
8984, 88mp3an3 1450 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
9077, 89sselid 3979 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
9190adantll 712 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
92 coeq1 5855 . . . . . . . . . . . . . . . 16 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
9392fveq2d 6892 . . . . . . . . . . . . . . 15 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
94 eqid 2732 . . . . . . . . . . . . . . 15 (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) = (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
95 fvex 6901 . . . . . . . . . . . . . . 15 (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) ∈ V
9693, 94, 95fvmpt 6995 . . . . . . . . . . . . . 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 2775 . . . . . . . . . . . 12 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)))
9998eqeq1d 2734 . . . . . . . . . . 11 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0 ↔ ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0))
10099rexbidva 3176 . . . . . . . . . 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 3439 . . . . . . . 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 773 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ 𝑀 ∈ β„•0)
104 ovex 7438 . . . . . . . . . . . 12 (1...𝑀) ∈ V
1053, 104unex 7729 . . . . . . . . . . 11 ((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V
106105a1i 11 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ ((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V)
107 simpr 485 . . . . . . . . . 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 13528 . . . . . . . . . . . . . . . 16 (1...𝑁) βŠ† β„•
112 ssdisj 4458 . . . . . . . . . . . . . . . 16 (((1...𝑁) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…)
113111, 39, 112mp2an 690 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…
114110, 113eqtri 2760 . . . . . . . . . . . . . 14 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…
115114a1i 11 . . . . . . . . . . . . 13 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…)
116 fun 6750 . . . . . . . . . . . . 13 (((( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
117108, 109, 115, 116syl21anc 836 . . . . . . . . . . . 12 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
118 uncom 4152 . . . . . . . . . . . . 13 (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹) = (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))
119118feq1i 6705 . . . . . . . . . . . 12 ((( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ↔ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
120117, 119sylib 217 . . . . . . . . . . 11 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
121120ad3antlr 729 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
122 mzprename 41472 . . . . . . . . . 10 ((((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁))) ∧ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀))) β†’ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
123106, 107, 121, 122syl3anc 1371 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
1243, 16, 17eldioph4i 41535 . . . . . . . . 9 ((𝑀 ∈ β„•0 ∧ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0} ∈ (Diophβ€˜π‘€))
125103, 123, 124syl2anc 584 . . . . . . . 8 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0} ∈ (Diophβ€˜π‘€))
126102, 125eqeltrd 2833 . . . . . . 7 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}} ∈ (Diophβ€˜π‘€))
127 eleq2 2822 . . . . . . . . 9 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ ((π‘Ž ∘ 𝐹) ∈ 𝑆 ↔ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}))
128127rabbidv 3440 . . . . . . . 8 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} = {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}})
129128eleq1d 2818 . . . . . . 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 3155 . . . . 5 (((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) β†’ (βˆƒπ‘ ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€)))
132131expimpd 454 . . . 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 408 . 2 ((𝑆 ∈ (Diophβ€˜π‘) ∧ (𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
1351343impb 1115 1 ((𝑆 ∈ (Diophβ€˜π‘) ∧ 𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βˆ– 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 6535  βŸΆwf 6536  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7405  Ο‰com 7851   ↑m cmap 8816   β‰ˆ cen 8932  Fincfn 8935  0cc0 11106  1c1 11107   + caddc 11109  β„•cn 12208  β„•0cn0 12468  β„€cz 12554  β„€β‰₯cuz 12818  ...cfz 13480  mzPolycmzp 41445  Diophcdioph 41478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  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 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-oadd 8466  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819  df-fz 13481  df-hash 14287  df-mzpcl 41446  df-mzp 41447  df-dioph 41479
This theorem is referenced by:  rabrenfdioph  41537
  Copyright terms: Public domain W3C validator