| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-mnc 43150 | . . . . 5
⊢  Monic =
(𝑠 ∈ 𝒫 ℂ
↦ {𝑝 ∈
(Poly‘𝑠) ∣
((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | 
| 2 | 1 | dmmptss 6260 | . . . 4
⊢ dom Monic
⊆ 𝒫 ℂ | 
| 3 |  | elfvdm 6942 | . . . 4
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑆 ∈ dom Monic ) | 
| 4 | 2, 3 | sselid 3980 | . . 3
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑆 ∈ 𝒫 ℂ) | 
| 5 | 4 | elpwid 4608 | . 2
⊢ (𝑃 ∈ ( Monic ‘𝑆) → 𝑆 ⊆ ℂ) | 
| 6 |  | plybss 26234 | . . 3
⊢ (𝑃 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) | 
| 7 | 6 | adantr 480 | . 2
⊢ ((𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1) → 𝑆 ⊆ ℂ) | 
| 8 |  | cnex 11237 | . . . . . 6
⊢ ℂ
∈ V | 
| 9 | 8 | elpw2 5333 | . . . . 5
⊢ (𝑆 ∈ 𝒫 ℂ ↔
𝑆 ⊆
ℂ) | 
| 10 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑠 = 𝑆 → (Poly‘𝑠) = (Poly‘𝑆)) | 
| 11 |  | rabeq 3450 | . . . . . . 7
⊢
((Poly‘𝑠) =
(Poly‘𝑆) →
{𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1} = {𝑝 ∈ (Poly‘𝑆) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | 
| 12 | 10, 11 | syl 17 | . . . . . 6
⊢ (𝑠 = 𝑆 → {𝑝 ∈ (Poly‘𝑠) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1} = {𝑝 ∈ (Poly‘𝑆) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | 
| 13 |  | fvex 6918 | . . . . . . 7
⊢
(Poly‘𝑆)
∈ V | 
| 14 | 13 | rabex 5338 | . . . . . 6
⊢ {𝑝 ∈ (Poly‘𝑆) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1} ∈
V | 
| 15 | 12, 1, 14 | fvmpt 7015 | . . . . 5
⊢ (𝑆 ∈ 𝒫 ℂ →
( Monic ‘𝑆) = {𝑝 ∈ (Poly‘𝑆) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | 
| 16 | 9, 15 | sylbir 235 | . . . 4
⊢ (𝑆 ⊆ ℂ → ( Monic
‘𝑆) = {𝑝 ∈ (Poly‘𝑆) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1}) | 
| 17 | 16 | eleq2d 2826 | . . 3
⊢ (𝑆 ⊆ ℂ → (𝑃 ∈ ( Monic ‘𝑆) ↔ 𝑃 ∈ {𝑝 ∈ (Poly‘𝑆) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1})) | 
| 18 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = 𝑃 → (coeff‘𝑝) = (coeff‘𝑃)) | 
| 19 |  | fveq2 6905 | . . . . . 6
⊢ (𝑝 = 𝑃 → (deg‘𝑝) = (deg‘𝑃)) | 
| 20 | 18, 19 | fveq12d 6912 | . . . . 5
⊢ (𝑝 = 𝑃 → ((coeff‘𝑝)‘(deg‘𝑝)) = ((coeff‘𝑃)‘(deg‘𝑃))) | 
| 21 | 20 | eqeq1d 2738 | . . . 4
⊢ (𝑝 = 𝑃 → (((coeff‘𝑝)‘(deg‘𝑝)) = 1 ↔ ((coeff‘𝑃)‘(deg‘𝑃)) = 1)) | 
| 22 | 21 | elrab 3691 | . . 3
⊢ (𝑃 ∈ {𝑝 ∈ (Poly‘𝑆) ∣ ((coeff‘𝑝)‘(deg‘𝑝)) = 1} ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1)) | 
| 23 | 17, 22 | bitrdi 287 | . 2
⊢ (𝑆 ⊆ ℂ → (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1))) | 
| 24 | 5, 7, 23 | pm5.21nii 378 | 1
⊢ (𝑃 ∈ ( Monic ‘𝑆) ↔ (𝑃 ∈ (Poly‘𝑆) ∧ ((coeff‘𝑃)‘(deg‘𝑃)) = 1)) |