# Metamath Proof Explorer

## Theorem ply1frcl

Description: Reverse closure for the set of univariate polynomial functions. (Contributed by AV, 9-Sep-2019)

Ref Expression
Hypothesis ply1frcl.q
`|- Q = ran ( S evalSub1 R )`
Assertion ply1frcl
`|- ( X e. Q -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )`

### Proof

Step Hyp Ref Expression
1 ply1frcl.q
` |-  Q = ran ( S evalSub1 R )`
2 ne0i
` |-  ( X e. ran ( S evalSub1 R ) -> ran ( S evalSub1 R ) =/= (/) )`
3 2 1 eleq2s
` |-  ( X e. Q -> ran ( S evalSub1 R ) =/= (/) )`
4 rneq
` |-  ( ( S evalSub1 R ) = (/) -> ran ( S evalSub1 R ) = ran (/) )`
5 rn0
` |-  ran (/) = (/)`
6 4 5 syl6eq
` |-  ( ( S evalSub1 R ) = (/) -> ran ( S evalSub1 R ) = (/) )`
7 6 necon3i
` |-  ( ran ( S evalSub1 R ) =/= (/) -> ( S evalSub1 R ) =/= (/) )`
8 n0
` |-  ( ( S evalSub1 R ) =/= (/) <-> E. e e e. ( S evalSub1 R ) )`
9 df-evls1
` |-  evalSub1 = ( s e. _V , r e. ~P ( Base ` s ) |-> [_ ( Base ` s ) / b ]_ ( ( x e. ( b ^m ( b ^m 1o ) ) |-> ( x o. ( y e. b |-> ( 1o X. { y } ) ) ) ) o. ( ( 1o evalSub s ) ` r ) ) )`
10 9 dmmpossx
` |-  dom evalSub1 C_ U_ s e. _V ( { s } X. ~P ( Base ` s ) )`
11 elfvdm
` |-  ( e e. ( evalSub1 ` <. S , R >. ) -> <. S , R >. e. dom evalSub1 )`
12 df-ov
` |-  ( S evalSub1 R ) = ( evalSub1 ` <. S , R >. )`
13 11 12 eleq2s
` |-  ( e e. ( S evalSub1 R ) -> <. S , R >. e. dom evalSub1 )`
14 10 13 sseldi
` |-  ( e e. ( S evalSub1 R ) -> <. S , R >. e. U_ s e. _V ( { s } X. ~P ( Base ` s ) ) )`
15 fveq2
` |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )`
16 15 pweqd
` |-  ( s = S -> ~P ( Base ` s ) = ~P ( Base ` S ) )`
17 16 opeliunxp2
` |-  ( <. S , R >. e. U_ s e. _V ( { s } X. ~P ( Base ` s ) ) <-> ( S e. _V /\ R e. ~P ( Base ` S ) ) )`
18 14 17 sylib
` |-  ( e e. ( S evalSub1 R ) -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )`
19 18 exlimiv
` |-  ( E. e e e. ( S evalSub1 R ) -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )`
20 8 19 sylbi
` |-  ( ( S evalSub1 R ) =/= (/) -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )`
21 3 7 20 3syl
` |-  ( X e. Q -> ( S e. _V /\ R e. ~P ( Base ` S ) ) )`