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 42129
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 5320 . . . . . 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 6888 . . . . . . . . . 10 (β„€β‰₯β€˜(0 + 1)) = (β„€β‰₯β€˜1)
85, 7eqtr4i 2757 . . . . . . . . 9 β„• = (β„€β‰₯β€˜(0 + 1))
98difeq2i 4114 . . . . . . . 8 (β„€ βˆ– β„•) = (β„€ βˆ– (β„€β‰₯β€˜(0 + 1)))
10 0z 12573 . . . . . . . . 9 0 ∈ β„€
11 lzenom 42086 . . . . . . . . 9 (0 ∈ β„€ β†’ (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰)
1210, 11ax-mp 5 . . . . . . . 8 (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰
139, 12eqbrtri 5162 . . . . . . 7 (β„€ βˆ– β„•) β‰ˆ Ο‰
14 enfi 9192 . . . . . . 7 ((β„€ βˆ– β„•) β‰ˆ Ο‰ β†’ ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin))
1513, 14ax-mp 5 . . . . . 6 ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin)
164, 15mtbir 323 . . . . 5 Β¬ (β„€ βˆ– β„•) ∈ Fin
17 disjdifr 4467 . . . . 5 ((β„€ βˆ– β„•) ∩ β„•) = βˆ…
183, 16, 17eldioph4b 42127 . . . 4 (𝑆 ∈ (Diophβ€˜π‘) ↔ (𝑁 ∈ β„•0 ∧ βˆƒπ‘ ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}))
19 simpr 484 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ π‘Ž ∈ (β„•0 ↑m (1...𝑀)))
20 simp-4r 781 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
21 ovex 7438 . . . . . . . . . . . . 13 (1...𝑁) ∈ V
2221mapco2 42031 . . . . . . . . . . . 12 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ (π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)))
2319, 20, 22syl2anc 583 . . . . . . . . . . 11 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ (π‘Ž ∘ 𝐹) ∈ (β„•0 ↑m (1...𝑁)))
24 uneq1 4151 . . . . . . . . . . . . . 14 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (𝑐 βˆͺ 𝑑) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
2524fveqeq2d 6893 . . . . . . . . . . . . 13 (𝑐 = (π‘Ž ∘ 𝐹) β†’ ((π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2625rexbidv 3172 . . . . . . . . . . . 12 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2726elrab3 3679 . . . . . . . . . . 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 783 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
30 simplr 766 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž ∈ (β„•0 ↑m (1...𝑀)))
31 simpr 484 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)))
32 coundi 6240 . . . . . . . . . . . . . . . 16 ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))))
33 coundir 6241 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹))
34 elmapi 8845 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ 𝑑:(β„€ βˆ– β„•)βŸΆβ„•0)
35343ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑:(β„€ βˆ– β„•)βŸΆβ„•0)
36 simp1 1133 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
37 incom 4196 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = ((1...𝑀) ∩ (β„€ βˆ– β„•))
38 fz1ssnn 13538 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑀) βŠ† β„•
39 disjdif 4466 . . . . . . . . . . . . . . . . . . . . . . . 24 (β„• ∩ (β„€ βˆ– β„•)) = βˆ…
40 ssdisj 4454 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1...𝑀) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…)
4138, 39, 40mp2an 689 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…
4237, 41eqtri 2754 . . . . . . . . . . . . . . . . . . . . . 22 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…
4342a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…)
44 coeq0i 42069 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4535, 36, 43, 44syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4645uneq2d 4158 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹)) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
4733, 46eqtrid 2778 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
48 un0 4385 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∘ 𝐹) βˆͺ βˆ…) = (π‘Ž ∘ 𝐹)
4947, 48eqtrdi 2782 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = (π‘Ž ∘ 𝐹))
50 coundir 6241 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))))
51 elmapi 8845 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž ∈ (β„•0 ↑m (1...𝑀)) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
52513ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
53 f1oi 6865 . . . . . . . . . . . . . . . . . . . . . . 23 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•)
54 f1of 6827 . . . . . . . . . . . . . . . . . . . . . . 23 (( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•) β†’ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•))
5553, 54ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•)
56 coeq0i 42069 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ž:(1...𝑀)βŸΆβ„•0 ∧ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
5755, 41, 56mp3an23 1449 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž:(1...𝑀)βŸΆβ„•0 β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
5852, 57syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) = βˆ…)
59 coires1 6257 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (𝑑 β†Ύ (β„€ βˆ– β„•))
60 ffn 6711 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 β†’ 𝑑 Fn (β„€ βˆ– β„•))
61 fnresdm 6663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 Fn (β„€ βˆ– β„•) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6234, 60, 613syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6359, 62eqtrid 2778 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
64633ad2ant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
6558, 64uneq12d 4159 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = (βˆ… βˆͺ 𝑑))
6650, 65eqtrid 2778 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (βˆ… βˆͺ 𝑑))
67 uncom 4148 . . . . . . . . . . . . . . . . . . 19 (βˆ… βˆͺ 𝑑) = (𝑑 βˆͺ βˆ…)
68 un0 4385 . . . . . . . . . . . . . . . . . . 19 (𝑑 βˆͺ βˆ…) = 𝑑
6967, 68eqtri 2754 . . . . . . . . . . . . . . . . . 18 (βˆ… βˆͺ 𝑑) = 𝑑
7066, 69eqtrdi 2782 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
7149, 70uneq12d 4159 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
7232, 71eqtr2id 2779 . . . . . . . . . . . . . . 15 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ 𝑑) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
7329, 30, 31, 72syl3anc 1368 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ 𝑑) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
7473fveq2d 6889 . . . . . . . . . . . . 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 689 . . . . . . . . . . . . . . . 16 (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
7841reseq2i 5972 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (π‘Ž β†Ύ βˆ…)
79 res0 5979 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ βˆ…) = βˆ…
8078, 79eqtri 2754 . . . . . . . . . . . . . . . . . 18 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8141reseq2i 5972 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ βˆ…)
82 res0 5979 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ βˆ…) = βˆ…
8381, 82eqtri 2754 . . . . . . . . . . . . . . . . . 18 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8480, 83eqtr4i 2757 . . . . . . . . . . . . . . . . 17 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))
85 elmapresaun 8876 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))))
86 uncom 4148 . . . . . . . . . . . . . . . . . . 19 ((1...𝑀) βˆͺ (β„€ βˆ– β„•)) = ((β„€ βˆ– β„•) βˆͺ (1...𝑀))
8786oveq2i 7416 . . . . . . . . . . . . . . . . . 18 (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))) = (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
8885, 87eleqtrdi 2837 . . . . . . . . . . . . . . . . 17 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
8984, 88mp3an3 1446 . . . . . . . . . . . . . . . 16 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
9077, 89sselid 3975 . . . . . . . . . . . . . . 15 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
9190adantll 711 . . . . . . . . . . . . . 14 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
92 coeq1 5851 . . . . . . . . . . . . . . . 16 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
9392fveq2d 6889 . . . . . . . . . . . . . . 15 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
94 eqid 2726 . . . . . . . . . . . . . . 15 (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) = (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
95 fvex 6898 . . . . . . . . . . . . . . 15 (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) ∈ V
9693, 94, 95fvmpt 6992 . . . . . . . . . . . . . 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 2769 . . . . . . . . . . . 12 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)))
9998eqeq1d 2728 . . . . . . . . . . 11 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0 ↔ ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0))
10099rexbidva 3170 . . . . . . . . . 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 3433 . . . . . . . 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 772 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ 𝑀 ∈ β„•0)
104 ovex 7438 . . . . . . . . . . . 12 (1...𝑀) ∈ V
1053, 104unex 7730 . . . . . . . . . . 11 ((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V
106105a1i 11 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ ((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V)
107 simpr 484 . . . . . . . . . 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 4196 . . . . . . . . . . . . . . 15 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = ((1...𝑁) ∩ (β„€ βˆ– β„•))
111 fz1ssnn 13538 . . . . . . . . . . . . . . . 16 (1...𝑁) βŠ† β„•
112 ssdisj 4454 . . . . . . . . . . . . . . . 16 (((1...𝑁) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…)
113111, 39, 112mp2an 689 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…
114110, 113eqtri 2754 . . . . . . . . . . . . . 14 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…
115114a1i 11 . . . . . . . . . . . . 13 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…)
116 fun 6747 . . . . . . . . . . . . 13 (((( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
117108, 109, 115, 116syl21anc 835 . . . . . . . . . . . 12 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
118 uncom 4148 . . . . . . . . . . . . 13 (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹) = (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))
119118feq1i 6702 . . . . . . . . . . . 12 ((( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ↔ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
120117, 119sylib 217 . . . . . . . . . . 11 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
121120ad3antlr 728 . . . . . . . . . 10 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
122 mzprename 42065 . . . . . . . . . 10 ((((β„€ βˆ– β„•) βˆͺ (1...𝑀)) ∈ V ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁))) ∧ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀))) β†’ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
123106, 107, 121, 122syl3anc 1368 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
1243, 16, 17eldioph4i 42128 . . . . . . . . 9 ((𝑀 ∈ β„•0 ∧ (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑀)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0} ∈ (Diophβ€˜π‘€))
125103, 123, 124syl2anc 583 . . . . . . . 8 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)) = 0} ∈ (Diophβ€˜π‘€))
126102, 125eqeltrd 2827 . . . . . . 7 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}} ∈ (Diophβ€˜π‘€))
127 eleq2 2816 . . . . . . . . 9 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ ((π‘Ž ∘ 𝐹) ∈ 𝑆 ↔ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}))
128127rabbidv 3434 . . . . . . . 8 (𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} = {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}})
129128eleq1d 2812 . . . . . . 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 3149 . . . . 5 (((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) β†’ (βˆƒπ‘ ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))𝑆 = {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0} β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€)))
132131expimpd 453 . . . 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 407 . 2 ((𝑆 ∈ (Diophβ€˜π‘) ∧ (𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
1351343impb 1112 1 ((𝑆 ∈ (Diophβ€˜π‘) ∧ 𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆƒwrex 3064  {crab 3426  Vcvv 3468   βˆ– cdif 3940   βˆͺ cun 3941   ∩ cin 3942   βŠ† wss 3943  βˆ…c0 4317   class class class wbr 5141   ↦ cmpt 5224   I cid 5566   β†Ύ cres 5671   ∘ ccom 5673   Fn wfn 6532  βŸΆwf 6533  β€“1-1-ontoβ†’wf1o 6536  β€˜cfv 6537  (class class class)co 7405  Ο‰com 7852   ↑m cmap 8822   β‰ˆ cen 8938  Fincfn 8941  0cc0 11112  1c1 11113   + caddc 11115  β„•cn 12216  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  ...cfz 13490  mzPolycmzp 42038  Diophcdioph 42071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  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 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-oadd 8471  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 13491  df-hash 14296  df-mzpcl 42039  df-mzp 42040  df-dioph 42072
This theorem is referenced by:  rabrenfdioph  42130
  Copyright terms: Public domain W3C validator