Theorem azssid

Description: The union of the integers and the adjoined complex number are a subset of the adjunction. (Contributed by AV, 31-Oct-2026)

	Ref	Expression
Assertion	azssid	|- ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) )

Proof

Step	Hyp	Ref	Expression
1		cnring	|- CCfld e. Ring
2	1	a1i	|- ( S e. CC -> CCfld e. Ring )
3		cnfldbas	|- CC = ( Base ` CCfld )
4	3	a1i	|- ( S e. CC -> CC = ( Base ` CCfld ) )
5		zsscn	|- ZZ C_ CC
6	5	a1i	|- ( S e. CC -> ZZ C_ CC )
7		snssi	|- ( S e. CC -> { S } C_ CC )
8	6 7	unssd	|- ( S e. CC -> ( ZZ u. { S } ) C_ CC )
9		eqidd	|- ( S e. CC -> ( RingSpan ` CCfld ) = ( RingSpan ` CCfld ) )
10		azval	|- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )
11	2 4 8 9 10	rgspnssid	|- ( S e. CC -> ( ZZ u. { S } ) C_ ( Z[] ` S ) )