Metamath Proof Explorer

Theorem diophrw

Description: Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014)

Ref Expression
Assertion diophrw 
|- ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> { a | E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) } = { a | E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) } )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) -> b e. ( NN0 ^m S ) )
2 nn0ex 
 |-  NN0 e. _V
3 simp1 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> S e. _V )
4 3 adantr 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) -> S e. _V )
5 elmapg 
 |-  ( ( NN0 e. _V /\ S e. _V ) -> ( b e. ( NN0 ^m S ) <-> b : S --> NN0 ) )
6 2 4 5 sylancr 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) -> ( b e. ( NN0 ^m S ) <-> b : S --> NN0 ) )
7 1 6 mpbid 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) -> b : S --> NN0 )
8 7 adantr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> b : S --> NN0 )
9 simp2 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> M : T -1-1-> S )
10 f1f 
 |-  ( M : T -1-1-> S -> M : T --> S )
11 9 10 syl 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> M : T --> S )
12 11 ad2antrr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> M : T --> S )
13 fco 
 |-  ( ( b : S --> NN0 /\ M : T --> S ) -> ( b o. M ) : T --> NN0 )
14 8 12 13 syl2anc 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( b o. M ) : T --> NN0 )
15 f1dmex 
 |-  ( ( M : T -1-1-> S /\ S e. _V ) -> T e. _V )
16 9 3 15 syl2anc 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> T e. _V )
17 16 ad2antrr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> T e. _V )
18 elmapg 
 |-  ( ( NN0 e. _V /\ T e. _V ) -> ( ( b o. M ) e. ( NN0 ^m T ) <-> ( b o. M ) : T --> NN0 ) )
19 2 17 18 sylancr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( ( b o. M ) e. ( NN0 ^m T ) <-> ( b o. M ) : T --> NN0 ) )
20 14 19 mpbird 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( b o. M ) e. ( NN0 ^m T ) )
21 simprl 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> a = ( b |` O ) )
22 resco 
 |-  ( ( b o. M ) |` O ) = ( b o. ( M |` O ) )
23 simpll3 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( M |` O ) = ( _I |` O ) )
24 23 coeq2d 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( b o. ( M |` O ) ) = ( b o. ( _I |` O ) ) )
25 coires1 
 |-  ( b o. ( _I |` O ) ) = ( b |` O )
26 24 25 eqtrdi 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( b o. ( M |` O ) ) = ( b |` O ) )
27 22 26 syl5eq 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( ( b o. M ) |` O ) = ( b |` O ) )
28 21 27 eqtr4d 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> a = ( ( b o. M ) |` O ) )
29 simpll1 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> S e. _V )
30 oveq2 
 |-  ( a = S -> ( NN0 ^m a ) = ( NN0 ^m S ) )
31 oveq2 
 |-  ( a = S -> ( ZZ ^m a ) = ( ZZ ^m S ) )
32 30 31 sseq12d 
 |-  ( a = S -> ( ( NN0 ^m a ) C_ ( ZZ ^m a ) <-> ( NN0 ^m S ) C_ ( ZZ ^m S ) ) )
33 zex 
 |-  ZZ e. _V
34 nn0ssz 
 |-  NN0 C_ ZZ
35 mapss 
 |-  ( ( ZZ e. _V /\ NN0 C_ ZZ ) -> ( NN0 ^m a ) C_ ( ZZ ^m a ) )
36 33 34 35 mp2an 
 |-  ( NN0 ^m a ) C_ ( ZZ ^m a )
37 32 36 vtoclg 
 |-  ( S e. _V -> ( NN0 ^m S ) C_ ( ZZ ^m S ) )
38 29 37 syl 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( NN0 ^m S ) C_ ( ZZ ^m S ) )
39 simplr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> b e. ( NN0 ^m S ) )
40 38 39 sseldd 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> b e. ( ZZ ^m S ) )
41 coeq1 
 |-  ( d = b -> ( d o. M ) = ( b o. M ) )
42 41 fveq2d 
 |-  ( d = b -> ( P ` ( d o. M ) ) = ( P ` ( b o. M ) ) )
43 eqid 
 |-  ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) = ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) )
44 fvex 
 |-  ( P ` ( b o. M ) ) e. _V
45 42 43 44 fvmpt 
 |-  ( b e. ( ZZ ^m S ) -> ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = ( P ` ( b o. M ) ) )
46 40 45 syl 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = ( P ` ( b o. M ) ) )
47 simprr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 )
48 46 47 eqtr3d 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> ( P ` ( b o. M ) ) = 0 )
49 reseq1 
 |-  ( c = ( b o. M ) -> ( c |` O ) = ( ( b o. M ) |` O ) )
50 49 eqeq2d 
 |-  ( c = ( b o. M ) -> ( a = ( c |` O ) <-> a = ( ( b o. M ) |` O ) ) )
51 fveqeq2 
 |-  ( c = ( b o. M ) -> ( ( P ` c ) = 0 <-> ( P ` ( b o. M ) ) = 0 ) )
52 50 51 anbi12d 
 |-  ( c = ( b o. M ) -> ( ( a = ( c |` O ) /\ ( P ` c ) = 0 ) <-> ( a = ( ( b o. M ) |` O ) /\ ( P ` ( b o. M ) ) = 0 ) ) )
53 52 rspcev 
 |-  ( ( ( b o. M ) e. ( NN0 ^m T ) /\ ( a = ( ( b o. M ) |` O ) /\ ( P ` ( b o. M ) ) = 0 ) ) -> E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) )
54 20 28 48 53 syl12anc 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ b e. ( NN0 ^m S ) ) /\ ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) -> E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) )
55 54 rexlimdva2 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> ( E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) -> E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) )
56 simpr 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> c e. ( NN0 ^m T ) )
57 16 adantr 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> T e. _V )
58 elmapg 
 |-  ( ( NN0 e. _V /\ T e. _V ) -> ( c e. ( NN0 ^m T ) <-> c : T --> NN0 ) )
59 2 57 58 sylancr 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( c e. ( NN0 ^m T ) <-> c : T --> NN0 ) )
60 56 59 mpbid 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> c : T --> NN0 )
61 60 adantr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> c : T --> NN0 )
62 9 ad2antrr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> M : T -1-1-> S )
63 f1cnv 
 |-  ( M : T -1-1-> S -> `' M : ran M -1-1-onto-> T )
64 f1of 
 |-  ( `' M : ran M -1-1-onto-> T -> `' M : ran M --> T )
65 62 63 64 3syl 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> `' M : ran M --> T )
66 fco 
 |-  ( ( c : T --> NN0 /\ `' M : ran M --> T ) -> ( c o. `' M ) : ran M --> NN0 )
67 61 65 66 syl2anc 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( c o. `' M ) : ran M --> NN0 )
68 c0ex 
 |-  0 e. _V
69 68 fconst 
 |-  ( ( S \ ran M ) X. { 0 } ) : ( S \ ran M ) --> { 0 }
70 69 a1i 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( S \ ran M ) X. { 0 } ) : ( S \ ran M ) --> { 0 } )
71 disjdif 
 |-  ( ran M i^i ( S \ ran M ) ) = (/)
72 71 a1i 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ran M i^i ( S \ ran M ) ) = (/) )
73 fun 
 |-  ( ( ( ( c o. `' M ) : ran M --> NN0 /\ ( ( S \ ran M ) X. { 0 } ) : ( S \ ran M ) --> { 0 } ) /\ ( ran M i^i ( S \ ran M ) ) = (/) ) -> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : ( ran M u. ( S \ ran M ) ) --> ( NN0 u. { 0 } ) )
74 67 70 72 73 syl21anc 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : ( ran M u. ( S \ ran M ) ) --> ( NN0 u. { 0 } ) )
75 frn 
 |-  ( M : T --> S -> ran M C_ S )
76 9 10 75 3syl 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> ran M C_ S )
77 76 ad2antrr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ran M C_ S )
78 undif 
 |-  ( ran M C_ S <-> ( ran M u. ( S \ ran M ) ) = S )
79 77 78 sylib 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ran M u. ( S \ ran M ) ) = S )
80 0nn0 
 |-  0 e. NN0
81 snssi 
 |-  ( 0 e. NN0 -> { 0 } C_ NN0 )
82 80 81 ax-mp 
 |-  { 0 } C_ NN0
83 ssequn2 
 |-  ( { 0 } C_ NN0 <-> ( NN0 u. { 0 } ) = NN0 )
84 82 83 mpbi 
 |-  ( NN0 u. { 0 } ) = NN0
85 84 a1i 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( NN0 u. { 0 } ) = NN0 )
86 79 85 feq23d 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : ( ran M u. ( S \ ran M ) ) --> ( NN0 u. { 0 } ) <-> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> NN0 ) )
87 74 86 mpbid 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> NN0 )
88 elmapg 
 |-  ( ( NN0 e. _V /\ S e. _V ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( NN0 ^m S ) <-> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> NN0 ) )
89 2 3 88 sylancr 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( NN0 ^m S ) <-> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> NN0 ) )
90 89 ad2antrr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( NN0 ^m S ) <-> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> NN0 ) )
91 87 90 mpbird 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( NN0 ^m S ) )
92 simprl 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> a = ( c |` O ) )
93 resundir 
 |-  ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) = ( ( ( c o. `' M ) |` O ) u. ( ( ( S \ ran M ) X. { 0 } ) |` O ) )
94 resco 
 |-  ( ( c o. `' M ) |` O ) = ( c o. ( `' M |` O ) )
95 simpl2 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> M : T -1-1-> S )
96 df-f1 
 |-  ( M : T -1-1-> S <-> ( M : T --> S /\ Fun `' M ) )
97 96 simprbi 
 |-  ( M : T -1-1-> S -> Fun `' M )
98 funcnvres 
 |-  ( Fun `' M -> `' ( M |` O ) = ( `' M |` ( M " O ) ) )
99 95 97 98 3syl 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> `' ( M |` O ) = ( `' M |` ( M " O ) ) )
100 simpl3 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( M |` O ) = ( _I |` O ) )
101 100 cnveqd 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> `' ( M |` O ) = `' ( _I |` O ) )
102 df-ima 
 |-  ( M " O ) = ran ( M |` O )
103 100 rneqd 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ran ( M |` O ) = ran ( _I |` O ) )
104 rnresi 
 |-  ran ( _I |` O ) = O
105 103 104 eqtrdi 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ran ( M |` O ) = O )
106 102 105 syl5eq 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( M " O ) = O )
107 106 reseq2d 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( `' M |` ( M " O ) ) = ( `' M |` O ) )
108 99 101 107 3eqtr3d 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> `' ( _I |` O ) = ( `' M |` O ) )
109 cnvresid 
 |-  `' ( _I |` O ) = ( _I |` O )
110 108 109 eqtr3di 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( `' M |` O ) = ( _I |` O ) )
111 110 coeq2d 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( c o. ( `' M |` O ) ) = ( c o. ( _I |` O ) ) )
112 coires1 
 |-  ( c o. ( _I |` O ) ) = ( c |` O )
113 111 112 eqtrdi 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( c o. ( `' M |` O ) ) = ( c |` O ) )
114 94 113 syl5eq 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( ( c o. `' M ) |` O ) = ( c |` O ) )
115 dmres 
 |-  dom ( ( ( S \ ran M ) X. { 0 } ) |` O ) = ( O i^i dom ( ( S \ ran M ) X. { 0 } ) )
116 68 snnz 
 |-  { 0 } =/= (/)
117 dmxp 
 |-  ( { 0 } =/= (/) -> dom ( ( S \ ran M ) X. { 0 } ) = ( S \ ran M ) )
118 116 117 ax-mp 
 |-  dom ( ( S \ ran M ) X. { 0 } ) = ( S \ ran M )
119 118 ineq2i 
 |-  ( O i^i dom ( ( S \ ran M ) X. { 0 } ) ) = ( O i^i ( S \ ran M ) )
120 inss1 
 |-  ( O i^i S ) C_ O
121 103 104 eqtr2di 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> O = ran ( M |` O ) )
122 resss 
 |-  ( M |` O ) C_ M
123 rnss 
 |-  ( ( M |` O ) C_ M -> ran ( M |` O ) C_ ran M )
124 122 123 mp1i 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ran ( M |` O ) C_ ran M )
125 121 124 eqsstrd 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> O C_ ran M )
126 120 125 sstrid 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( O i^i S ) C_ ran M )
127 inssdif0 
 |-  ( ( O i^i S ) C_ ran M <-> ( O i^i ( S \ ran M ) ) = (/) )
128 126 127 sylib 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( O i^i ( S \ ran M ) ) = (/) )
129 119 128 syl5eq 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( O i^i dom ( ( S \ ran M ) X. { 0 } ) ) = (/) )
130 115 129 syl5eq 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> dom ( ( ( S \ ran M ) X. { 0 } ) |` O ) = (/) )
131 relres 
 |-  Rel ( ( ( S \ ran M ) X. { 0 } ) |` O )
132 reldm0 
 |-  ( Rel ( ( ( S \ ran M ) X. { 0 } ) |` O ) -> ( ( ( ( S \ ran M ) X. { 0 } ) |` O ) = (/) <-> dom ( ( ( S \ ran M ) X. { 0 } ) |` O ) = (/) ) )
133 131 132 ax-mp 
 |-  ( ( ( ( S \ ran M ) X. { 0 } ) |` O ) = (/) <-> dom ( ( ( S \ ran M ) X. { 0 } ) |` O ) = (/) )
134 130 133 sylibr 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( ( ( S \ ran M ) X. { 0 } ) |` O ) = (/) )
135 114 134 uneq12d 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( ( ( c o. `' M ) |` O ) u. ( ( ( S \ ran M ) X. { 0 } ) |` O ) ) = ( ( c |` O ) u. (/) ) )
136 93 135 syl5eq 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) = ( ( c |` O ) u. (/) ) )
137 un0 
 |-  ( ( c |` O ) u. (/) ) = ( c |` O )
138 136 137 eqtr2di 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> ( c |` O ) = ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) )
139 138 adantr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( c |` O ) = ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) )
140 92 139 eqtrd 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> a = ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) )
141 fss 
 |-  ( ( c : T --> NN0 /\ NN0 C_ ZZ ) -> c : T --> ZZ )
142 60 34 141 sylancl 
 |-  ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) -> c : T --> ZZ )
143 142 adantr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> c : T --> ZZ )
144 fco 
 |-  ( ( c : T --> ZZ /\ `' M : ran M --> T ) -> ( c o. `' M ) : ran M --> ZZ )
145 143 65 144 syl2anc 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( c o. `' M ) : ran M --> ZZ )
146 fun 
 |-  ( ( ( ( c o. `' M ) : ran M --> ZZ /\ ( ( S \ ran M ) X. { 0 } ) : ( S \ ran M ) --> { 0 } ) /\ ( ran M i^i ( S \ ran M ) ) = (/) ) -> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : ( ran M u. ( S \ ran M ) ) --> ( ZZ u. { 0 } ) )
147 145 70 72 146 syl21anc 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : ( ran M u. ( S \ ran M ) ) --> ( ZZ u. { 0 } ) )
148 0z 
 |-  0 e. ZZ
149 snssi 
 |-  ( 0 e. ZZ -> { 0 } C_ ZZ )
150 148 149 ax-mp 
 |-  { 0 } C_ ZZ
151 ssequn2 
 |-  ( { 0 } C_ ZZ <-> ( ZZ u. { 0 } ) = ZZ )
152 150 151 mpbi 
 |-  ( ZZ u. { 0 } ) = ZZ
153 152 a1i 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ZZ u. { 0 } ) = ZZ )
154 79 153 feq23d 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : ( ran M u. ( S \ ran M ) ) --> ( ZZ u. { 0 } ) <-> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> ZZ ) )
155 147 154 mpbid 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> ZZ )
156 elmapg 
 |-  ( ( ZZ e. _V /\ S e. _V ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( ZZ ^m S ) <-> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> ZZ ) )
157 33 3 156 sylancr 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( ZZ ^m S ) <-> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> ZZ ) )
158 157 ad2antrr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( ZZ ^m S ) <-> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) : S --> ZZ ) )
159 155 158 mpbird 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( ZZ ^m S ) )
160 coeq1 
 |-  ( d = ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) -> ( d o. M ) = ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) o. M ) )
161 160 fveq2d 
 |-  ( d = ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) -> ( P ` ( d o. M ) ) = ( P ` ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) o. M ) ) )
162 fvex 
 |-  ( P ` ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) o. M ) ) e. _V
163 161 43 162 fvmpt 
 |-  ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( ZZ ^m S ) -> ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) ) = ( P ` ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) o. M ) ) )
164 159 163 syl 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) ) = ( P ` ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) o. M ) ) )
165 coundir 
 |-  ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) o. M ) = ( ( ( c o. `' M ) o. M ) u. ( ( ( S \ ran M ) X. { 0 } ) o. M ) )
166 coass 
 |-  ( ( c o. `' M ) o. M ) = ( c o. ( `' M o. M ) )
167 f1cocnv1 
 |-  ( M : T -1-1-> S -> ( `' M o. M ) = ( _I |` T ) )
168 167 coeq2d 
 |-  ( M : T -1-1-> S -> ( c o. ( `' M o. M ) ) = ( c o. ( _I |` T ) ) )
169 62 168 syl 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( c o. ( `' M o. M ) ) = ( c o. ( _I |` T ) ) )
170 166 169 syl5eq 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( c o. `' M ) o. M ) = ( c o. ( _I |` T ) ) )
171 118 ineq1i 
 |-  ( dom ( ( S \ ran M ) X. { 0 } ) i^i ran M ) = ( ( S \ ran M ) i^i ran M )
172 incom 
 |-  ( ( S \ ran M ) i^i ran M ) = ( ran M i^i ( S \ ran M ) )
173 171 172 71 3eqtri 
 |-  ( dom ( ( S \ ran M ) X. { 0 } ) i^i ran M ) = (/)
174 coeq0 
 |-  ( ( ( ( S \ ran M ) X. { 0 } ) o. M ) = (/) <-> ( dom ( ( S \ ran M ) X. { 0 } ) i^i ran M ) = (/) )
175 173 174 mpbir 
 |-  ( ( ( S \ ran M ) X. { 0 } ) o. M ) = (/)
176 175 a1i 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( ( S \ ran M ) X. { 0 } ) o. M ) = (/) )
177 170 176 uneq12d 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( ( c o. `' M ) o. M ) u. ( ( ( S \ ran M ) X. { 0 } ) o. M ) ) = ( ( c o. ( _I |` T ) ) u. (/) ) )
178 un0 
 |-  ( ( c o. ( _I |` T ) ) u. (/) ) = ( c o. ( _I |` T ) )
179 fcoi1 
 |-  ( c : T --> NN0 -> ( c o. ( _I |` T ) ) = c )
180 61 179 syl 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( c o. ( _I |` T ) ) = c )
181 178 180 syl5eq 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( c o. ( _I |` T ) ) u. (/) ) = c )
182 177 181 eqtrd 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( ( c o. `' M ) o. M ) u. ( ( ( S \ ran M ) X. { 0 } ) o. M ) ) = c )
183 165 182 syl5eq 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) o. M ) = c )
184 183 fveq2d 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( P ` ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) o. M ) ) = ( P ` c ) )
185 simprr 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( P ` c ) = 0 )
186 164 184 185 3eqtrd 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) ) = 0 )
187 reseq1 
 |-  ( b = ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) -> ( b |` O ) = ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) )
188 187 eqeq2d 
 |-  ( b = ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) -> ( a = ( b |` O ) <-> a = ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) ) )
189 fveqeq2 
 |-  ( b = ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) -> ( ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 <-> ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) ) = 0 ) )
190 188 189 anbi12d 
 |-  ( b = ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) -> ( ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) <-> ( a = ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) ) = 0 ) ) )
191 190 rspcev 
 |-  ( ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) e. ( NN0 ^m S ) /\ ( a = ( ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` ( ( c o. `' M ) u. ( ( S \ ran M ) X. { 0 } ) ) ) = 0 ) ) -> E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) )
192 91 140 186 191 syl12anc 
 |-  ( ( ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) /\ c e. ( NN0 ^m T ) ) /\ ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) -> E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) )
193 192 rexlimdva2 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> ( E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) -> E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) ) )
194 55 193 impbid 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> ( E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) <-> E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) ) )
195 194 abbidv 
 |-  ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> { a | E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) } = { a | E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) } )