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	$⊢ φ \to F \in DivRing$
	fldgenval.3	$⊢ φ \to S \subseteq B$
	fldgenss.t	$⊢ φ \to T \subseteq S$
Assertion	fldgenss	$⊢ φ \to F fldGen T \subseteq F fldGen S$

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

Metamath Proof Explorer