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 evalSub 1 R
Assertion ply1frcl ⊢ X ∈ Q → S ∈ V ∧ R ∈ 𝒫 Base S

Proof

Step Hyp Ref Expression
1 ply1frcl.q ⊢ Q = ran ⁡ S evalSub 1 R
2 ne0i ⊢ X ∈ ran ⁡ S evalSub 1 R → ran ⁡ S evalSub 1 R ≠ ∅
3 2 1 eleq2s ⊢ X ∈ Q → ran ⁡ S evalSub 1 R ≠ ∅
4 rneq ⊢ S evalSub 1 R = ∅ → ran ⁡ S evalSub 1 R = ran ⁡ ∅
5 rn0 ⊢ ran ⁡ ∅ = ∅
6 4 5 eqtrdi ⊢ S evalSub 1 R = ∅ → ran ⁡ S evalSub 1 R = ∅
7 6 necon3i ⊢ ran ⁡ S evalSub 1 R ≠ ∅ → S evalSub 1 R ≠ ∅
8 n0 ⊢ S evalSub 1 R ≠ ∅ ↔ ∃ e e ∈ S evalSub 1 R
9 df-evls1 ⊢ evalSub 1 = s ∈ V , r ∈ 𝒫 Base s ⟼ ⦋ Base s / b⦌ x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y ∘ 1 𝑜 evalSub s ⁡ r
10 9 dmmpossx ⊢ dom ⁡ evalSub 1 ⊆ ⋃ s ∈ V s × 𝒫 Base s
11 elfvdm ⊢ e ∈ evalSub 1 ⁡ S R → S R ∈ dom ⁡ evalSub 1
12 df-ov ⊢ S evalSub 1 R = evalSub 1 ⁡ S R
13 11 12 eleq2s ⊢ e ∈ S evalSub 1 R → S R ∈ dom ⁡ evalSub 1
14 10 13 sselid ⊢ e ∈ S evalSub 1 R → S R ∈ ⋃ s ∈ V s × 𝒫 Base s
15 fveq2 ⊢ s = S → Base s = Base S
16 15 pweqd ⊢ s = S → 𝒫 Base s = 𝒫 Base S
17 16 opeliunxp2 ⊢ S R ∈ ⋃ s ∈ V s × 𝒫 Base s ↔ S ∈ V ∧ R ∈ 𝒫 Base S
18 14 17 sylib ⊢ e ∈ S evalSub 1 R → S ∈ V ∧ R ∈ 𝒫 Base S
19 18 exlimiv ⊢ ∃ e e ∈ S evalSub 1 R → S ∈ V ∧ R ∈ 𝒫 Base S
20 8 19 sylbi ⊢ S evalSub 1 R ≠ ∅ → S ∈ V ∧ R ∈ 𝒫 Base S
21 3 7 20 3syl ⊢ X ∈ Q → S ∈ V ∧ R ∈ 𝒫 Base S