Theorem plyssc

Description: Every polynomial ring is contained in the ring of polynomials over CC . (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ ( Poly ‘ ℂ )
2		sseq1	⊢ ( ( Poly ‘ 𝑆 ) = ∅ → ( ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) ↔ ∅ ⊆ ( Poly ‘ ℂ ) ) )
3	1 2	mpbiri	⊢ ( ( Poly ‘ 𝑆 ) = ∅ → ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) )
4		n0	⊢ ( ( Poly ‘ 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( Poly ‘ 𝑆 ) )
5		plybss	⊢ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
6		ssid	⊢ ℂ ⊆ ℂ
7		plyss	⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) )
8	5 6 7	sylancl	⊢ ( 𝑓 ∈ ( Poly ‘ 𝑆 ) → ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) )
9	8	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( Poly ‘ 𝑆 ) → ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) )
10	4 9	sylbi	⊢ ( ( Poly ‘ 𝑆 ) ≠ ∅ → ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ ) )
11	3 10	pm2.61ine	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )