ssfzunsn

Description: A subset of a finite sequence of integers extended by an integer is a subset of a (possibly extended) finite sequence of integers. (Contributed by AV, 8-Jun-2021) (Proof shortened by AV, 13-Nov-2021)

		Ref	Expression
	Assertion	ssfzunsn	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to S \cup \{I\} \subseteq (M \dots if (I \leq N, N, I))$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to S \subseteq (M \dots N)$
2		eluzel2	$⊢ I \in ℤ_{\geq M} \to M \in ℤ$
3	2	3ad2ant3	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to M \in ℤ$
4		simp2	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to N \in ℤ$
5		eluzelz	$⊢ I \in ℤ_{\geq M} \to I \in ℤ$
6	5	3ad2ant3	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to I \in ℤ$
7		ssfzunsnext	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to S \cup \{I\} \subseteq (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
8	1 3 4 6 7	syl13anc	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to S \cup \{I\} \subseteq (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
9		eluz2	$⊢ I \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land I \in ℤ \land M \leq I)$
10		zre	$⊢ I \in ℤ \to I \in ℝ$
11	10	rexrd	$⊢ I \in ℤ \to I \in ℝ^{*}$
12	11	3ad2ant2	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to I \in ℝ^{*}$
13		zre	$⊢ M \in ℤ \to M \in ℝ$
14	13	rexrd	$⊢ M \in ℤ \to M \in ℝ^{*}$
15	14	3ad2ant1	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to M \in ℝ^{*}$
16		simp3	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to M \leq I$
17		xrmineq	$⊢ (I \in ℝ^{} \land M \in ℝ^{} \land M \leq I) \to if (I \leq M, I, M) = M$
18	12 15 16 17	syl3anc	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to if (I \leq M, I, M) = M$
19	18	eqcomd	$⊢ (M \in ℤ \land I \in ℤ \land M \leq I) \to M = if (I \leq M, I, M)$
20	9 19	sylbi	$⊢ I \in ℤ_{\geq M} \to M = if (I \leq M, I, M)$
21	20	3ad2ant3	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to M = if (I \leq M, I, M)$
22	21	oveq1d	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to (M \dots if (I \leq N, N, I)) = (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
23	8 22	sseqtrrd	$⊢ (S \subseteq (M \dots N) \land N \in ℤ \land I \in ℤ_{\geq M}) \to S \cup \{I\} \subseteq (M \dots if (I \leq N, N, I))$

Metamath Proof Explorer

Theorem ssfzunsn

Proof