hbtlem3

Description: The leading ideal function is monotone. (Contributed by Stefan O'Rear, 31-Mar-2015)

Step	Hyp	Ref	Expression
1		hbtlem.p	$⊢ P = {Poly}_{1} (R)$
2		hbtlem.u	$⊢ U = LIdeal (P)$
3		hbtlem.s	$⊢ S = ldgIdlSeq (R)$
4		hbtlem3.r	$⊢ φ \to R \in Ring$
5		hbtlem3.i	$⊢ φ \to I \in U$
6		hbtlem3.j	$⊢ φ \to J \in U$
7		hbtlem3.ij	$⊢ φ \to I \subseteq J$
8		hbtlem3.x	$⊢ φ \to X \in ℕ_{0}$
9		ssrexv	$⊢ I \subseteq J \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \to \exists b \in J (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)))$
10	7 9	syl	$⊢ φ \to (\exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)) \to \exists b \in J (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X)))$
11	10	ss2abdv	$⊢ φ \to \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\} \subseteq \{a \| \exists b \in J (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
12		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
13	1 2 3 12	hbtlem1	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to S (I) (X) = \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
14	4 5 8 13	syl3anc	$⊢ φ \to S (I) (X) = \{a \| \exists b \in I (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
15	1 2 3 12	hbtlem1	$⊢ (R \in Ring \land J \in U \land X \in ℕ_{0}) \to S (J) (X) = \{a \| \exists b \in J (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
16	4 6 8 15	syl3anc	$⊢ φ \to S (J) (X) = \{a \| \exists b \in J (\deg_{1} (R) (b) \leq X \land a = {coe}_{1} (b) (X))\}$
17	11 14 16	3sstr4d	$⊢ φ \to S (I) (X) \subseteq S (J) (X)$

Metamath Proof Explorer