ssinc

Description: Inclusion relation for a monotonic sequence of sets. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	ssinc.1	$⊢ φ \to N \in ℤ_{\geq M}$
	ssinc.2	$⊢ (φ \land m \in (M ..^N)) \to F (m) \subseteq F (m + 1)$
Assertion	ssinc	$⊢ φ \to F (M) \subseteq F (N)$

Proof

Step	Hyp	Ref	Expression
1		ssinc.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		ssinc.2	$⊢ (φ \land m \in (M ..^N)) \to F (m) \subseteq F (m + 1)$
3		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
4	1 3	syl	$⊢ φ \to M \in ℤ$
5		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
6	1 5	syl	$⊢ φ \to N \in ℤ$
7	4 6	jca	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
8		eluzle	$⊢ N \in ℤ_{\geq M} \to M \leq N$
9	1 8	syl	$⊢ φ \to M \leq N$
10	6	zred	$⊢ φ \to N \in ℝ$
11	10	leidd	$⊢ φ \to N \leq N$
12	6 9 11	3jca	$⊢ φ \to (N \in ℤ \land M \leq N \land N \leq N)$
13	7 12	jca	$⊢ φ \to ((M \in ℤ \land N \in ℤ) \land (N \in ℤ \land M \leq N \land N \leq N))$
14		id	$⊢ φ \to φ$
15		fveq2	$⊢ n = M \to F (n) = F (M)$
16	15	sseq2d	$⊢ n = M \to (F (M) \subseteq F (n) \leftrightarrow F (M) \subseteq F (M))$
17	16	imbi2d	$⊢ n = M \to ((φ \to F (M) \subseteq F (n)) \leftrightarrow (φ \to F (M) \subseteq F (M)))$
18		fveq2	$⊢ n = m \to F (n) = F (m)$
19	18	sseq2d	$⊢ n = m \to (F (M) \subseteq F (n) \leftrightarrow F (M) \subseteq F (m))$
20	19	imbi2d	$⊢ n = m \to ((φ \to F (M) \subseteq F (n)) \leftrightarrow (φ \to F (M) \subseteq F (m)))$
21		fveq2	$⊢ n = m + 1 \to F (n) = F (m + 1)$
22	21	sseq2d	$⊢ n = m + 1 \to (F (M) \subseteq F (n) \leftrightarrow F (M) \subseteq F (m + 1))$
23	22	imbi2d	$⊢ n = m + 1 \to ((φ \to F (M) \subseteq F (n)) \leftrightarrow (φ \to F (M) \subseteq F (m + 1)))$
24		fveq2	$⊢ n = N \to F (n) = F (N)$
25	24	sseq2d	$⊢ n = N \to (F (M) \subseteq F (n) \leftrightarrow F (M) \subseteq F (N))$
26	25	imbi2d	$⊢ n = N \to ((φ \to F (M) \subseteq F (n)) \leftrightarrow (φ \to F (M) \subseteq F (N)))$
27		ssidd	$⊢ φ \to F (M) \subseteq F (M)$
28	27	a1i	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to (φ \to F (M) \subseteq F (M))$
29		simpr	$⊢ ((φ \to F (M) \subseteq F (m)) \land φ) \to φ$
30		simpl	$⊢ ((φ \to F (M) \subseteq F (m)) \land φ) \to (φ \to F (M) \subseteq F (m))$
31		pm3.35	$⊢ (φ \land (φ \to F (M) \subseteq F (m))) \to F (M) \subseteq F (m)$
32	29 30 31	syl2anc	$⊢ ((φ \to F (M) \subseteq F (m)) \land φ) \to F (M) \subseteq F (m)$
33	32	3adant1	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land (φ \to F (M) \subseteq F (m)) \land φ) \to F (M) \subseteq F (m)$
34		simpr	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to φ$
35		simplll	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to M \in ℤ$
36		simplr1	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to m \in ℤ$
37		simplr2	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to M \leq m$
38	35 36 37	3jca	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to (M \in ℤ \land m \in ℤ \land M \leq m)$
39		eluz2	$⊢ m \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land m \in ℤ \land M \leq m)$
40	38 39	sylibr	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to m \in ℤ_{\geq M}$
41		simpllr	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to N \in ℤ$
42		simplr3	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to m < N$
43	40 41 42	3jca	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to (m \in ℤ_{\geq M} \land N \in ℤ \land m < N)$
44		elfzo2	$⊢ m \in (M ..^N) \leftrightarrow (m \in ℤ_{\geq M} \land N \in ℤ \land m < N)$
45	43 44	sylibr	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to m \in (M ..^N)$
46	34 45 2	syl2anc	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to F (m) \subseteq F (m + 1)$
47	46	3adant2	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land (φ \to F (M) \subseteq F (m)) \land φ) \to F (m) \subseteq F (m + 1)$
48	33 47	sstrd	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land (φ \to F (M) \subseteq F (m)) \land φ) \to F (M) \subseteq F (m + 1)$
49	48	3exp	$⊢ ((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \to ((φ \to F (M) \subseteq F (m)) \to (φ \to F (M) \subseteq F (m + 1)))$
50	17 20 23 26 28 49	fzind	$⊢ ((M \in ℤ \land N \in ℤ) \land (N \in ℤ \land M \leq N \land N \leq N)) \to (φ \to F (M) \subseteq F (N))$
51	13 14 50	sylc	$⊢ φ \to F (M) \subseteq F (N)$

Metamath Proof Explorer

Theorem ssinc

Proof