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 42282
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 12607 . . . . . 6 β„€ ∈ V
2 difexg 5333 . . . . . 6 (β„€ ∈ V β†’ (β„€ βˆ– β„•) ∈ V)
31, 2ax-mp 5 . . . . 5 (β„€ βˆ– β„•) ∈ V
4 ominf 9291 . . . . . 6 Β¬ Ο‰ ∈ Fin
5 nnuz 12905 . . . . . . . . . 10 β„• = (β„€β‰₯β€˜1)
6 0p1e1 12374 . . . . . . . . . . 11 (0 + 1) = 1
76fveq2i 6905 . . . . . . . . . 10 (β„€β‰₯β€˜(0 + 1)) = (β„€β‰₯β€˜1)
85, 7eqtr4i 2759 . . . . . . . . 9 β„• = (β„€β‰₯β€˜(0 + 1))
98difeq2i 4119 . . . . . . . 8 (β„€ βˆ– β„•) = (β„€ βˆ– (β„€β‰₯β€˜(0 + 1)))
10 0z 12609 . . . . . . . . 9 0 ∈ β„€
11 lzenom 42239 . . . . . . . . 9 (0 ∈ β„€ β†’ (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰)
1210, 11ax-mp 5 . . . . . . . 8 (β„€ βˆ– (β„€β‰₯β€˜(0 + 1))) β‰ˆ Ο‰
139, 12eqbrtri 5173 . . . . . . 7 (β„€ βˆ– β„•) β‰ˆ Ο‰
14 enfi 9223 . . . . . . 7 ((β„€ βˆ– β„•) β‰ˆ Ο‰ β†’ ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin))
1513, 14ax-mp 5 . . . . . 6 ((β„€ βˆ– β„•) ∈ Fin ↔ Ο‰ ∈ Fin)
164, 15mtbir 322 . . . . 5 Β¬ (β„€ βˆ– β„•) ∈ Fin
17 disjdifr 4476 . . . . 5 ((β„€ βˆ– β„•) ∩ β„•) = βˆ…
183, 16, 17eldioph4b 42280 . . . 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 782 . . . . . . . . . . . 12 (((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) β†’ 𝐹:(1...𝑁)⟢(1...𝑀))
21 ovex 7459 . . . . . . . . . . . . 13 (1...𝑁) ∈ V
2221mapco2 42184 . . . . . . . . . . . 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 4157 . . . . . . . . . . . . . 14 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (𝑐 βˆͺ 𝑑) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
2524fveqeq2d 6910 . . . . . . . . . . . . 13 (𝑐 = (π‘Ž ∘ 𝐹) β†’ ((π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2625rexbidv 3176 . . . . . . . . . . . 12 (𝑐 = (π‘Ž ∘ 𝐹) β†’ (βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0 ↔ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = 0))
2726elrab3 3685 . . . . . . . . . . 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 483 . . . . . . . . . . . . . . 15 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)))
32 coundi 6256 . . . . . . . . . . . . . . . 16 ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))))
33 coundir 6257 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹))
34 elmapi 8876 . . . . . . . . . . . . . . . . . . . . . 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 4203 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = ((1...𝑀) ∩ (β„€ βˆ– β„•))
38 fz1ssnn 13574 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑀) βŠ† β„•
39 disjdif 4475 . . . . . . . . . . . . . . . . . . . . . . . 24 (β„• ∩ (β„€ βˆ– β„•)) = βˆ…
40 ssdisj 4463 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1...𝑀) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…)
4138, 39, 40mp2an 690 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑀) ∩ (β„€ βˆ– β„•)) = βˆ…
4237, 41eqtri 2756 . . . . . . . . . . . . . . . . . . . . . 22 ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…
4342a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…)
44 coeq0i 42222 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑀)) = βˆ…) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4535, 36, 43, 44syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ 𝐹) = βˆ…)
4645uneq2d 4164 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ 𝐹) βˆͺ (𝑑 ∘ 𝐹)) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
4733, 46eqtrid 2780 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = ((π‘Ž ∘ 𝐹) βˆͺ βˆ…))
48 un0 4394 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∘ 𝐹) βˆͺ βˆ…) = (π‘Ž ∘ 𝐹)
4947, 48eqtrdi 2784 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ 𝐹) = (π‘Ž ∘ 𝐹))
50 coundir 6257 . . . . . . . . . . . . . . . . . . 19 ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))))
51 elmapi 8876 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž ∈ (β„•0 ↑m (1...𝑀)) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
52513ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ π‘Ž:(1...𝑀)βŸΆβ„•0)
53 f1oi 6882 . . . . . . . . . . . . . . . . . . . . . . 23 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•)
54 f1of 6844 . . . . . . . . . . . . . . . . . . . . . . 23 (( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)–1-1-ontoβ†’(β„€ βˆ– β„•) β†’ ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•))
5553, 54ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•)
56 coeq0i 42222 . . . . . . . . . . . . . . . . . . . . . 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 6273 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (𝑑 β†Ύ (β„€ βˆ– β„•))
60 ffn 6727 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑:(β„€ βˆ– β„•)βŸΆβ„•0 β†’ 𝑑 Fn (β„€ βˆ– β„•))
61 fnresdm 6679 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 Fn (β„€ βˆ– β„•) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6234, 60, 613syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 β†Ύ (β„€ βˆ– β„•)) = 𝑑)
6359, 62eqtrid 2780 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
64633ad2ant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
6558, 64uneq12d 4165 . . . . . . . . . . . . . . . . . . 19 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž ∘ ( I β†Ύ (β„€ βˆ– β„•))) βˆͺ (𝑑 ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = (βˆ… βˆͺ 𝑑))
6650, 65eqtrid 2780 . . . . . . . . . . . . . . . . . 18 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = (βˆ… βˆͺ 𝑑))
67 uncom 4154 . . . . . . . . . . . . . . . . . . 19 (βˆ… βˆͺ 𝑑) = (𝑑 βˆͺ βˆ…)
68 un0 4394 . . . . . . . . . . . . . . . . . . 19 (𝑑 βˆͺ βˆ…) = 𝑑
6967, 68eqtri 2756 . . . . . . . . . . . . . . . . . 18 (βˆ… βˆͺ 𝑑) = 𝑑
7066, 69eqtrdi 2784 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•))) = 𝑑)
7149, 70uneq12d 4165 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑁)⟢(1...𝑀) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (((π‘Ž βˆͺ 𝑑) ∘ 𝐹) βˆͺ ((π‘Ž βˆͺ 𝑑) ∘ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž ∘ 𝐹) βˆͺ 𝑑))
7232, 71eqtr2id 2781 . . . . . . . . . . . . . . 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 6906 . . . . . . . . . . . . 13 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
75 nn0ssz 12621 . . . . . . . . . . . . . . . . 17 β„•0 βŠ† β„€
76 mapss 8916 . . . . . . . . . . . . . . . . 17 ((β„€ ∈ V ∧ β„•0 βŠ† β„€) β†’ (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))))
771, 75, 76mp2an 690 . . . . . . . . . . . . . . . 16 (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) βŠ† (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
7841reseq2i 5986 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (π‘Ž β†Ύ βˆ…)
79 res0 5993 . . . . . . . . . . . . . . . . . . 19 (π‘Ž β†Ύ βˆ…) = βˆ…
8078, 79eqtri 2756 . . . . . . . . . . . . . . . . . 18 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8141reseq2i 5986 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ βˆ…)
82 res0 5993 . . . . . . . . . . . . . . . . . . 19 (𝑑 β†Ύ βˆ…) = βˆ…
8381, 82eqtri 2756 . . . . . . . . . . . . . . . . . 18 (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = βˆ…
8480, 83eqtr4i 2759 . . . . . . . . . . . . . . . . 17 (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))
85 elmapresaun 8907 . . . . . . . . . . . . . . . . . 18 ((π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•)) ∧ (π‘Ž β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•))) = (𝑑 β†Ύ ((1...𝑀) ∩ (β„€ βˆ– β„•)))) β†’ (π‘Ž βˆͺ 𝑑) ∈ (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))))
86 uncom 4154 . . . . . . . . . . . . . . . . . . 19 ((1...𝑀) βˆͺ (β„€ βˆ– β„•)) = ((β„€ βˆ– β„•) βˆͺ (1...𝑀))
8786oveq2i 7437 . . . . . . . . . . . . . . . . . 18 (β„•0 ↑m ((1...𝑀) βˆͺ (β„€ βˆ– β„•))) = (β„•0 ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
8885, 87eleqtrdi 2839 . . . . . . . . . . . . . . . . 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 3980 . . . . . . . . . . . . . . 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 5864 . . . . . . . . . . . . . . . 16 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))) = ((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))
9392fveq2d 6906 . . . . . . . . . . . . . . 15 (𝑒 = (π‘Ž βˆͺ 𝑑) β†’ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) = (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
94 eqid 2728 . . . . . . . . . . . . . . 15 (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))))) = (𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))
95 fvex 6915 . . . . . . . . . . . . . . 15 (π‘β€˜((π‘Ž βˆͺ 𝑑) ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))) ∈ V
9693, 94, 95fvmpt 7010 . . . . . . . . . . . . . 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 2771 . . . . . . . . . . . 12 ((((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) ∧ π‘Ž ∈ (β„•0 ↑m (1...𝑀))) ∧ 𝑑 ∈ (β„•0 ↑m (β„€ βˆ– β„•))) β†’ (π‘β€˜((π‘Ž ∘ 𝐹) βˆͺ 𝑑)) = ((𝑒 ∈ (β„€ ↑m ((β„€ βˆ– β„•) βˆͺ (1...𝑀))) ↦ (π‘β€˜(𝑒 ∘ (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•))))))β€˜(π‘Ž βˆͺ 𝑑)))
9998eqeq1d 2730 . . . . . . . . . . 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 773 . . . . . . . . 9 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ 𝑀 ∈ β„•0)
104 ovex 7459 . . . . . . . . . . . 12 (1...𝑀) ∈ V
1053, 104unex 7756 . . . . . . . . . . 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 4203 . . . . . . . . . . . . . . 15 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = ((1...𝑁) ∩ (β„€ βˆ– β„•))
111 fz1ssnn 13574 . . . . . . . . . . . . . . . 16 (1...𝑁) βŠ† β„•
112 ssdisj 4463 . . . . . . . . . . . . . . . 16 (((1...𝑁) βŠ† β„• ∧ (β„• ∩ (β„€ βˆ– β„•)) = βˆ…) β†’ ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…)
113111, 39, 112mp2an 690 . . . . . . . . . . . . . . 15 ((1...𝑁) ∩ (β„€ βˆ– β„•)) = βˆ…
114110, 113eqtri 2756 . . . . . . . . . . . . . 14 ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…
115114a1i 11 . . . . . . . . . . . . 13 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…)
116 fun 6764 . . . . . . . . . . . . 13 (((( I β†Ύ (β„€ βˆ– β„•)):(β„€ βˆ– β„•)⟢(β„€ βˆ– β„•) ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ ((β„€ βˆ– β„•) ∩ (1...𝑁)) = βˆ…) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
117108, 109, 115, 116syl21anc 836 . . . . . . . . . . . 12 (𝐹:(1...𝑁)⟢(1...𝑀) β†’ (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹):((β„€ βˆ– β„•) βˆͺ (1...𝑁))⟢((β„€ βˆ– β„•) βˆͺ (1...𝑀)))
118 uncom 4154 . . . . . . . . . . . . 13 (( I β†Ύ (β„€ βˆ– β„•)) βˆͺ 𝐹) = (𝐹 βˆͺ ( I β†Ύ (β„€ βˆ– β„•)))
119118feq1i 6718 . . . . . . . . . . . 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 42218 . . . . . . . . . 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 42281 . . . . . . . . 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 2829 . . . . . . 7 ((((𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) ∧ 𝑁 ∈ β„•0) ∧ 𝑏 ∈ (mzPolyβ€˜((β„€ βˆ– β„•) βˆͺ (1...𝑁)))) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ {𝑐 ∈ (β„•0 ↑m (1...𝑁)) ∣ βˆƒπ‘‘ ∈ (β„•0 ↑m (β„€ βˆ– β„•))(π‘β€˜(𝑐 βˆͺ 𝑑)) = 0}} ∈ (Diophβ€˜π‘€))
127 eleq2 2818 . . . . . . . . 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 2814 . . . . . . 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 3152 . . . . 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 1112 1 ((𝑆 ∈ (Diophβ€˜π‘) ∧ 𝑀 ∈ β„•0 ∧ 𝐹:(1...𝑁)⟢(1...𝑀)) β†’ {π‘Ž ∈ (β„•0 ↑m (1...𝑀)) ∣ (π‘Ž ∘ 𝐹) ∈ 𝑆} ∈ (Diophβ€˜π‘€))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆƒwrex 3067  {crab 3430  Vcvv 3473   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4326   class class class wbr 5152   ↦ cmpt 5235   I cid 5579   β†Ύ cres 5684   ∘ ccom 5686   Fn wfn 6548  βŸΆwf 6549  β€“1-1-ontoβ†’wf1o 6552  β€˜cfv 6553  (class class class)co 7426  Ο‰com 7878   ↑m cmap 8853   β‰ˆ cen 8969  Fincfn 8972  0cc0 11148  1c1 11149   + caddc 11151  β„•cn 12252  β„•0cn0 12512  β„€cz 12598  β„€β‰₯cuz 12862  ...cfz 13526  mzPolycmzp 42191  Diophcdioph 42224
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 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-inf2 9674  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7692  df-om 7879  df-1st 8001  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-oadd 8499  df-er 8733  df-map 8855  df-en 8973  df-dom 8974  df-sdom 8975  df-fin 8976  df-dju 9934  df-card 9972  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-nn 12253  df-n0 12513  df-z 12599  df-uz 12863  df-fz 13527  df-hash 14332  df-mzpcl 42192  df-mzp 42193  df-dioph 42225
This theorem is referenced by:  rabrenfdioph  42283
  Copyright terms: Public domain W3C validator