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={\mathrm{Base}}_F$$
	fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
	fldgenval.3	$$⊢\phi \to S\subseteq B$$
	fldgenss.t	$$⊢\phi \to T\subseteq S$$
Assertion	fldgenss	$$⊢\phi \to F\mathrm{fldGen}T\subseteq F\mathrm{fldGen}S$$

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
2		fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
3		fldgenval.3	$$⊢\phi \to S\subseteq B$$
4		fldgenss.t	$$⊢\phi \to T\subseteq S$$
5	4	adantr	$$⊢\left(\phi \wedge S\subseteq a\right)\to T\subseteq S$$
6		simpr	$$⊢\left(\phi \wedge S\subseteq a\right)\to S\subseteq a$$
7	5 6	sstrd	$$⊢\left(\phi \wedge S\subseteq a\right)\to T\subseteq a$$
8	7	ex	$$⊢\phi \to \left(S\subseteq a\to T\subseteq a\right)$$
9	8	adantr	$$⊢\left(\phi \wedge a\in \mathrm{SubDRing}\left(F\right)\right)\to \left(S\subseteq a\to T\subseteq a\right)$$
10	9	ss2rabdv	$$⊢\phi \to \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}\subseteq \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}$$
11		intss	$$⊢\left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}\subseteq \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}\to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}\subseteq \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
12	10 11	syl	$$⊢\phi \to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}\subseteq \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
13	4 3	sstrd	$$⊢\phi \to T\subseteq B$$
14	1 2 13	fldgenval	$$⊢\phi \to F\mathrm{fldGen}T=\bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}$$
15	1 2 3	fldgenval	$$⊢\phi \to F\mathrm{fldGen}S=\bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
16	12 14 15	3sstr4d	$$⊢\phi \to F\mathrm{fldGen}T\subseteq F\mathrm{fldGen}S$$