hbtlem6

Description: There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	hbtlem.p	$⊢ P = {Poly}_{1} (R)$
	hbtlem.u	$⊢ U = LIdeal (P)$
	hbtlem.s	$⊢ S = ldgIdlSeq (R)$
	hbtlem6.n	$⊢ N = RSpan (P)$
	hbtlem6.r	$⊢ φ \to R \in LNoeR$
	hbtlem6.i	$⊢ φ \to I \in U$
	hbtlem6.x	$⊢ φ \to X \in ℕ_{0}$
Assertion	hbtlem6	$⊢ φ \to \exists k \in (𝒫 I \cap Fin) S (I) (X) \subseteq S (N (k)) (X)$

Proof

Step	Hyp	Ref	Expression
1		hbtlem.p	$⊢ P = {Poly}_{1} (R)$
2		hbtlem.u	$⊢ U = LIdeal (P)$
3		hbtlem.s	$⊢ S = ldgIdlSeq (R)$
4		hbtlem6.n	$⊢ N = RSpan (P)$
5		hbtlem6.r	$⊢ φ \to R \in LNoeR$
6		hbtlem6.i	$⊢ φ \to I \in U$
7		hbtlem6.x	$⊢ φ \to X \in ℕ_{0}$
8		lnrring	$⊢ R \in LNoeR \to R \in Ring$
9	5 8	syl	$⊢ φ \to R \in Ring$
10		eqid	$⊢ LIdeal (R) = LIdeal (R)$
11	1 2 3 10	hbtlem2	$⊢ (R \in Ring \land I \in U \land X \in ℕ_{0}) \to S (I) (X) \in LIdeal (R)$
12	9 6 7 11	syl3anc	$⊢ φ \to S (I) (X) \in LIdeal (R)$
13		eqid	$⊢ RSpan (R) = RSpan (R)$
14	10 13	lnr2i	$⊢ (R \in LNoeR \land S (I) (X) \in LIdeal (R)) \to \exists a \in (𝒫 S (I) (X) \cap Fin) S (I) (X) = RSpan (R) (a)$
15	5 12 14	syl2anc	$⊢ φ \to \exists a \in (𝒫 S (I) (X) \cap Fin) S (I) (X) = RSpan (R) (a)$
16		elfpw	$⊢ a \in (𝒫 S (I) (X) \cap Fin) \leftrightarrow (a \subseteq S (I) (X) \land a \in Fin)$
17		fvex	$⊢ {coe}_{1} (b) (X) \in V$
18		eqid	$⊢ (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) = (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
19	17 18	fnmpti	$⊢ (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) Fn \{c \in I \| \deg_{1} (R) (c) \leq X\}$
20	19	a1i	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) Fn \{c \in I \| \deg_{1} (R) (c) \leq X\}$
21		simprl	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to a \subseteq S (I) (X)$
22		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
23	1 2 3 22	hbtlem1	$⊢ (R \in LNoeR \land I \in U \land X \in ℕ_{0}) \to S (I) (X) = \{d \| \exists b \in I (\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X))\}$
24	5 6 7 23	syl3anc	$⊢ φ \to S (I) (X) = \{d \| \exists b \in I (\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X))\}$
25	18	rnmpt	$⊢ ran (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) = \{d \| \exists b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} d = {coe}_{1} (b) (X)\}$
26		fveq2	$⊢ c = b \to \deg_{1} (R) (c) = \deg_{1} (R) (b)$
27	26	breq1d	$⊢ c = b \to (\deg_{1} (R) (c) \leq X \leftrightarrow \deg_{1} (R) (b) \leq X)$
28	27	rexrab	$⊢ \exists b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} d = {coe}_{1} (b) (X) \leftrightarrow \exists b \in I (\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X))$
29	28	abbii	$⊢ \{d \| \exists b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} d = {coe}_{1} (b) (X)\} = \{d \| \exists b \in I (\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X))\}$
30	25 29	eqtri	$⊢ ran (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) = \{d \| \exists b \in I (\deg_{1} (R) (b) \leq X \land d = {coe}_{1} (b) (X))\}$
31	24 30	eqtr4di	$⊢ φ \to S (I) (X) = ran (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
32	31	adantr	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to S (I) (X) = ran (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
33	21 32	sseqtrd	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to a \subseteq ran (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
34		simprr	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to a \in Fin$
35		fipreima	$⊢ ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) Fn \{c \in I \| \deg_{1} (R) (c) \leq X\} \land a \subseteq ran (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) \land a \in Fin) \to \exists k \in (𝒫 \{c \in I \| \deg_{1} (R) (c) \leq X\} \cap Fin) (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a$
36	20 33 34 35	syl3anc	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to \exists k \in (𝒫 \{c \in I \| \deg_{1} (R) (c) \leq X\} \cap Fin) (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a$
37		elfpw	$⊢ k \in (𝒫 \{c \in I \| \deg_{1} (R) (c) \leq X\} \cap Fin) \leftrightarrow (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)$
38		ssrab2	$⊢ \{c \in I \| \deg_{1} (R) (c) \leq X\} \subseteq I$
39		sstr2	$⊢ k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \to (\{c \in I \| \deg_{1} (R) (c) \leq X\} \subseteq I \to k \subseteq I)$
40	38 39	mpi	$⊢ k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \to k \subseteq I$
41	40	adantl	$⊢ (φ \land k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\}) \to k \subseteq I$
42		velpw	$⊢ k \in 𝒫 I \leftrightarrow k \subseteq I$
43	41 42	sylibr	$⊢ (φ \land k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\}) \to k \in 𝒫 I$
44	43	adantrr	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to k \in 𝒫 I$
45		simprr	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to k \in Fin$
46	44 45	elind	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to k \in (𝒫 I \cap Fin)$
47	9	adantr	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to R \in Ring$
48	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
49	9 48	syl	$⊢ φ \to P \in Ring$
50	49	adantr	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to P \in Ring$
51		simprl	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\}$
52	51 38	sstrdi	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to k \subseteq I$
53		eqid	$⊢ {Base}_{P} = {Base}_{P}$
54	53 2	lidlss	$⊢ I \in U \to I \subseteq {Base}_{P}$
55	6 54	syl	$⊢ φ \to I \subseteq {Base}_{P}$
56	55	adantr	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to I \subseteq {Base}_{P}$
57	52 56	sstrd	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to k \subseteq {Base}_{P}$
58	4 53 2	rspcl	$⊢ (P \in Ring \land k \subseteq {Base}_{P}) \to N (k) \in U$
59	50 57 58	syl2anc	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to N (k) \in U$
60	7	adantr	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to X \in ℕ_{0}$
61	1 2 3 10	hbtlem2	$⊢ (R \in Ring \land N (k) \in U \land X \in ℕ_{0}) \to S (N (k)) (X) \in LIdeal (R)$
62	47 59 60 61	syl3anc	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to S (N (k)) (X) \in LIdeal (R)$
63		df-ima	$⊢ (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = ran ({(b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k})$
64	4 53	rspssid	$⊢ (P \in Ring \land k \subseteq {Base}_{P}) \to k \subseteq N (k)$
65	50 57 64	syl2anc	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to k \subseteq N (k)$
66		ssrab	$⊢ k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \leftrightarrow (k \subseteq I \land \forall c \in k \deg_{1} (R) (c) \leq X)$
67	66	simprbi	$⊢ k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \to \forall c \in k \deg_{1} (R) (c) \leq X$
68	67	ad2antrl	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to \forall c \in k \deg_{1} (R) (c) \leq X$
69		ssrab	$⊢ k \subseteq \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} \leftrightarrow (k \subseteq N (k) \land \forall c \in k \deg_{1} (R) (c) \leq X)$
70	65 68 69	sylanbrc	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to k \subseteq \{c \in N (k) \| \deg_{1} (R) (c) \leq X\}$
71	70	resmptd	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to {(b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k} = (b \in k ⟼ {coe}_{1} (b) (X))$
72		resmpt	$⊢ k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \to {(b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k} = (b \in k ⟼ {coe}_{1} (b) (X))$
73	72	ad2antrl	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to {(b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k} = (b \in k ⟼ {coe}_{1} (b) (X))$
74	71 73	eqtr4d	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to {(b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k} = {(b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k}$
75		resss	$⊢ {(b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k} \subseteq (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
76	74 75	eqsstrrdi	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to {(b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k} \subseteq (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
77		rnss	$⊢ {(b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k} \subseteq (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) \to ran ({(b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k}) \subseteq ran (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
78	76 77	syl	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to ran ({(b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) ↾}_{k}) \subseteq ran (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
79	63 78	eqsstrid	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] \subseteq ran (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
80	1 2 3 22	hbtlem1	$⊢ (R \in Ring \land N (k) \in U \land X \in ℕ_{0}) \to S (N (k)) (X) = \{e \| \exists b \in N (k) (\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X))\}$
81	47 59 60 80	syl3anc	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to S (N (k)) (X) = \{e \| \exists b \in N (k) (\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X))\}$
82		eqid	$⊢ (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) = (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
83	82	rnmpt	$⊢ ran (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) = \{e \| \exists b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} e = {coe}_{1} (b) (X)\}$
84	27	rexrab	$⊢ \exists b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} e = {coe}_{1} (b) (X) \leftrightarrow \exists b \in N (k) (\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X))$
85	84	abbii	$⊢ \{e \| \exists b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} e = {coe}_{1} (b) (X)\} = \{e \| \exists b \in N (k) (\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X))\}$
86	83 85	eqtri	$⊢ ran (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) = \{e \| \exists b \in N (k) (\deg_{1} (R) (b) \leq X \land e = {coe}_{1} (b) (X))\}$
87	81 86	eqtr4di	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to S (N (k)) (X) = ran (b \in \{c \in N (k) \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X))$
88	79 87	sseqtrrd	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] \subseteq S (N (k)) (X)$
89	13 10	rspssp	$⊢ (R \in Ring \land S (N (k)) (X) \in LIdeal (R) \land (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] \subseteq S (N (k)) (X)) \to RSpan (R) ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k]) \subseteq S (N (k)) (X)$
90	47 62 88 89	syl3anc	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to RSpan (R) ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k]) \subseteq S (N (k)) (X)$
91	46 90	jca	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to (k \in (𝒫 I \cap Fin) \land RSpan (R) ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k]) \subseteq S (N (k)) (X))$
92		fveq2	$⊢ (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a \to RSpan (R) ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k]) = RSpan (R) (a)$
93	92	sseq1d	$⊢ (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a \to (RSpan (R) ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k]) \subseteq S (N (k)) (X) \leftrightarrow RSpan (R) (a) \subseteq S (N (k)) (X))$
94	93	anbi2d	$⊢ (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a \to ((k \in (𝒫 I \cap Fin) \land RSpan (R) ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k]) \subseteq S (N (k)) (X)) \leftrightarrow (k \in (𝒫 I \cap Fin) \land RSpan (R) (a) \subseteq S (N (k)) (X)))$
95	91 94	syl5ibcom	$⊢ (φ \land (k \subseteq \{c \in I \| \deg_{1} (R) (c) \leq X\} \land k \in Fin)) \to ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a \to (k \in (𝒫 I \cap Fin) \land RSpan (R) (a) \subseteq S (N (k)) (X)))$
96	37 95	sylan2b	$⊢ (φ \land k \in (𝒫 \{c \in I \| \deg_{1} (R) (c) \leq X\} \cap Fin)) \to ((b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a \to (k \in (𝒫 I \cap Fin) \land RSpan (R) (a) \subseteq S (N (k)) (X)))$
97	96	expimpd	$⊢ φ \to ((k \in (𝒫 \{c \in I \| \deg_{1} (R) (c) \leq X\} \cap Fin) \land (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a) \to (k \in (𝒫 I \cap Fin) \land RSpan (R) (a) \subseteq S (N (k)) (X)))$
98	97	adantr	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to ((k \in (𝒫 \{c \in I \| \deg_{1} (R) (c) \leq X\} \cap Fin) \land (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a) \to (k \in (𝒫 I \cap Fin) \land RSpan (R) (a) \subseteq S (N (k)) (X)))$
99	98	reximdv2	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to (\exists k \in (𝒫 \{c \in I \| \deg_{1} (R) (c) \leq X\} \cap Fin) (b \in \{c \in I \| \deg_{1} (R) (c) \leq X\} ⟼ {coe}_{1} (b) (X)) [k] = a \to \exists k \in (𝒫 I \cap Fin) RSpan (R) (a) \subseteq S (N (k)) (X))$
100	36 99	mpd	$⊢ (φ \land (a \subseteq S (I) (X) \land a \in Fin)) \to \exists k \in (𝒫 I \cap Fin) RSpan (R) (a) \subseteq S (N (k)) (X)$
101	16 100	sylan2b	$⊢ (φ \land a \in (𝒫 S (I) (X) \cap Fin)) \to \exists k \in (𝒫 I \cap Fin) RSpan (R) (a) \subseteq S (N (k)) (X)$
102		sseq1	$⊢ S (I) (X) = RSpan (R) (a) \to (S (I) (X) \subseteq S (N (k)) (X) \leftrightarrow RSpan (R) (a) \subseteq S (N (k)) (X))$
103	102	rexbidv	$⊢ S (I) (X) = RSpan (R) (a) \to (\exists k \in (𝒫 I \cap Fin) S (I) (X) \subseteq S (N (k)) (X) \leftrightarrow \exists k \in (𝒫 I \cap Fin) RSpan (R) (a) \subseteq S (N (k)) (X))$
104	101 103	syl5ibrcom	$⊢ (φ \land a \in (𝒫 S (I) (X) \cap Fin)) \to (S (I) (X) = RSpan (R) (a) \to \exists k \in (𝒫 I \cap Fin) S (I) (X) \subseteq S (N (k)) (X))$
105	104	rexlimdva	$⊢ φ \to (\exists a \in (𝒫 S (I) (X) \cap Fin) S (I) (X) = RSpan (R) (a) \to \exists k \in (𝒫 I \cap Fin) S (I) (X) \subseteq S (N (k)) (X))$
106	15 105	mpd	$⊢ φ \to \exists k \in (𝒫 I \cap Fin) S (I) (X) \subseteq S (N (k)) (X)$

Metamath Proof Explorer

Theorem hbtlem6

Proof