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	Could not format assertion : No typesetting found for |- ( ph -> ( F fldGen T ) C_ ( F fldGen S ) ) with typecode |-

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	Could not format ( ph -> ( F fldGen T ) = |^| { a e. ( SubDRing ` F ) | T C_ a } ) : No typesetting found for |- ( ph -> ( F fldGen T ) = |^| { a e. ( SubDRing ` F ) | T C_ a } ) with typecode |-
15	1 2 3	fldgenval	Could not format ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) : No typesetting found for |- ( ph -> ( F fldGen S ) = |^| { a e. ( SubDRing ` F ) | S C_ a } ) with typecode |-
16	12 14 15	3sstr4d	Could not format ( ph -> ( F fldGen T ) C_ ( F fldGen S ) ) : No typesetting found for |- ( ph -> ( F fldGen T ) C_ ( F fldGen S ) ) with typecode |-