Theorem fldgenss

Description: Generated subfields preserve subset ordering. ( see lspss and spanss ) (Contributed by Thierry Arnoux, 15-Jan-2025)

	Ref	Expression
Hypotheses	fldgenval.1	|- B = ( Base ` F )
	fldgenval.2	|- ( ph -> F e. DivRing )
	fldgenval.3	|- ( ph -> S C_ B )
	fldgenss.t	|- ( ph -> T C_ S )
Assertion	fldgenss	|- ( ph -> ( F fldGen T ) C_ ( F fldGen S ) )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	|- B = ( Base ` F )
2		fldgenval.2	|- ( ph -> F e. DivRing )
3		fldgenval.3	|- ( ph -> S C_ B )
4		fldgenss.t	|- ( ph -> T C_ S )
5	4	adantr	|- ( ( ph /\ S C_ a ) -> T C_ S )
6		simpr	|- ( ( ph /\ S C_ a ) -> S C_ a )
7	5 6	sstrd	|- ( ( ph /\ S C_ a ) -> T C_ a )
8	7	ex	|- ( ph -> ( S C_ a -> T C_ a ) )
9	8	adantr	|- ( ( ph /\ a e. ( SubDRing ` F ) ) -> ( S C_ a -> T C_ a ) )
10	9	ss2rabdv	|- ( ph -> { a e. ( SubDRing ` F ) | S C_ a } C_ { a e. ( SubDRing ` F ) | T C_ a } )
11		intss	|- ( { a e. ( SubDRing ` F ) | S C_ a } C_ { a e. ( SubDRing ` F ) | T C_ a } -> |^| { a e. ( SubDRing ` F ) | T C_ a } C_ |^| { a e. ( SubDRing ` F ) | S C_ a } )
12	10 11	syl	|- ( ph -> |^| { a e. ( SubDRing ` F ) | T C_ a } C_ |^| { a e. ( SubDRing ` F ) | S C_ a } )
13	4 3	sstrd	|- ( ph -> T C_ B )
14	1 2 13	fldgenval	|- ( ph -> ( F fldGen T ) = |^| { a e. ( SubDRing ` F ) | T C_ a } )
15	1 2 3	fldgenval	|- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } )
16	12 14 15	3sstr4d	|- ( ph -> ( F fldGen T ) C_ ( F fldGen S ) )