ssdec

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

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

Proof

Step	Hyp	Ref	Expression
1		ssdec.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		ssdec.2	$⊢ (φ \land m \in (M ..^N)) \to F (m + 1) \subseteq F (m)$
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		fveq2	$⊢ n = M \to F (n) = F (M)$
15	14	sseq1d	$⊢ n = M \to (F (n) \subseteq F (M) \leftrightarrow F (M) \subseteq F (M))$
16	15	imbi2d	$⊢ n = M \to ((φ \to F (n) \subseteq F (M)) \leftrightarrow (φ \to F (M) \subseteq F (M)))$
17		fveq2	$⊢ n = m \to F (n) = F (m)$
18	17	sseq1d	$⊢ n = m \to (F (n) \subseteq F (M) \leftrightarrow F (m) \subseteq F (M))$
19	18	imbi2d	$⊢ n = m \to ((φ \to F (n) \subseteq F (M)) \leftrightarrow (φ \to F (m) \subseteq F (M)))$
20		fveq2	$⊢ n = m + 1 \to F (n) = F (m + 1)$
21	20	sseq1d	$⊢ n = m + 1 \to (F (n) \subseteq F (M) \leftrightarrow F (m + 1) \subseteq F (M))$
22	21	imbi2d	$⊢ n = m + 1 \to ((φ \to F (n) \subseteq F (M)) \leftrightarrow (φ \to F (m + 1) \subseteq F (M)))$
23		fveq2	$⊢ n = N \to F (n) = F (N)$
24	23	sseq1d	$⊢ n = N \to (F (n) \subseteq F (M) \leftrightarrow F (N) \subseteq F (M))$
25	24	imbi2d	$⊢ n = N \to ((φ \to F (n) \subseteq F (M)) \leftrightarrow (φ \to F (N) \subseteq F (M)))$
26		ssidd	$⊢ φ \to F (M) \subseteq F (M)$
27	26	a1i	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \to (φ \to F (M) \subseteq F (M))$
28		simpr	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to φ$
29		simplll	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to M \in ℤ$
30		simplr1	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to m \in ℤ$
31		simplr2	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to M \leq m$
32	29 30 31	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)$
33		eluz2	$⊢ m \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land m \in ℤ \land M \leq m)$
34	32 33	sylibr	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to m \in ℤ_{\geq M}$
35		simpllr	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to N \in ℤ$
36		simplr3	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to m < N$
37	34 35 36	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)$
38		elfzo2	$⊢ m \in (M ..^N) \leftrightarrow (m \in ℤ_{\geq M} \land N \in ℤ \land m < N)$
39	37 38	sylibr	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to m \in (M ..^N)$
40	28 39 2	syl2anc	$⊢ (((M \in ℤ \land N \in ℤ) \land (m \in ℤ \land M \leq m \land m < N)) \land φ) \to F (m + 1) \subseteq F (m)$
41	40	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 + 1) \subseteq F (m)$
42		simpr	$⊢ ((φ \to F (m) \subseteq F (M)) \land φ) \to φ$
43		simpl	$⊢ ((φ \to F (m) \subseteq F (M)) \land φ) \to (φ \to F (m) \subseteq F (M))$
44		pm3.35	$⊢ (φ \land (φ \to F (m) \subseteq F (M))) \to F (m) \subseteq F (M)$
45	42 43 44	syl2anc	$⊢ ((φ \to F (m) \subseteq F (M)) \land φ) \to F (m) \subseteq F (M)$
46	45	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)$
47	41 46	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 + 1) \subseteq F (M)$
48	47	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 + 1) \subseteq F (M)))$
49	16 19 22 25 27 48	fzind	$⊢ ((M \in ℤ \land N \in ℤ) \land (N \in ℤ \land M \leq N \land N \leq N)) \to (φ \to F (N) \subseteq F (M))$
50	13 49	mpcom	$⊢ φ \to F (N) \subseteq F (M)$

Metamath Proof Explorer

Theorem ssdec

Proof