ssfzunsnext

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, 13-Nov-2021)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to S \subseteq (M \dots N)$
2		simp3	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to I \in ℤ$
3		simp1	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to M \in ℤ$
4	2 3	ifcld	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to if (I \leq M, I, M) \in ℤ$
5	4	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq M, I, M) \in ℤ$
6		elfzelz	$⊢ k \in (M \dots N) \to k \in ℤ$
7	6	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \in ℤ$
8	4	zred	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to if (I \leq M, I, M) \in ℝ$
9	8	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq M, I, M) \in ℝ$
10		zre	$⊢ M \in ℤ \to M \in ℝ$
11	10	3ad2ant1	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to M \in ℝ$
12	11	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to M \in ℝ$
13	6	zred	$⊢ k \in (M \dots N) \to k \in ℝ$
14	13	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \in ℝ$
15		zre	$⊢ I \in ℤ \to I \in ℝ$
16	10 15	anim12i	$⊢ (M \in ℤ \land I \in ℤ) \to (M \in ℝ \land I \in ℝ)$
17	16	ancomd	$⊢ (M \in ℤ \land I \in ℤ) \to (I \in ℝ \land M \in ℝ)$
18	17	3adant2	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (I \in ℝ \land M \in ℝ)$
19	18	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to (I \in ℝ \land M \in ℝ)$
20		min2	$⊢ (I \in ℝ \land M \in ℝ) \to if (I \leq M, I, M) \leq M$
21	19 20	syl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq M, I, M) \leq M$
22		elfzle1	$⊢ k \in (M \dots N) \to M \leq k$
23	22	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to M \leq k$
24	9 12 14 21 23	letrd	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq M, I, M) \leq k$
25		eluz2	$⊢ k \in ℤ_{\geq if (I \leq M, I, M)} \leftrightarrow (if (I \leq M, I, M) \in ℤ \land k \in ℤ \land if (I \leq M, I, M) \leq k)$
26	5 7 24 25	syl3anbrc	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \in ℤ_{\geq if (I \leq M, I, M)}$
27		simp2	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to N \in ℤ$
28	27 2	ifcld	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to if (I \leq N, N, I) \in ℤ$
29	28	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq N, N, I) \in ℤ$
30		zre	$⊢ N \in ℤ \to N \in ℝ$
31	30	3ad2ant2	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to N \in ℝ$
32	31	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to N \in ℝ$
33	28	zred	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to if (I \leq N, N, I) \in ℝ$
34	33	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq N, N, I) \in ℝ$
35		elfzle2	$⊢ k \in (M \dots N) \to k \leq N$
36	35	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \leq N$
37	30 15	anim12i	$⊢ (N \in ℤ \land I \in ℤ) \to (N \in ℝ \land I \in ℝ)$
38	37	3adant1	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (N \in ℝ \land I \in ℝ)$
39	38	ancomd	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (I \in ℝ \land N \in ℝ)$
40		max2	$⊢ (I \in ℝ \land N \in ℝ) \to N \leq if (I \leq N, N, I)$
41	39 40	syl	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to N \leq if (I \leq N, N, I)$
42	41	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to N \leq if (I \leq N, N, I)$
43	14 32 34 36 42	letrd	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \leq if (I \leq N, N, I)$
44		eluz2	$⊢ if (I \leq N, N, I) \in ℤ_{\geq k} \leftrightarrow (k \in ℤ \land if (I \leq N, N, I) \in ℤ \land k \leq if (I \leq N, N, I))$
45	7 29 43 44	syl3anbrc	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq N, N, I) \in ℤ_{\geq k}$
46		elfzuzb	$⊢ k \in (if (I \leq M, I, M) \dots if (I \leq N, N, I)) \leftrightarrow (k \in ℤ_{\geq if (I \leq M, I, M)} \land if (I \leq N, N, I) \in ℤ_{\geq k})$
47	26 45 46	sylanbrc	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \in (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
48	47	ex	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (k \in (M \dots N) \to k \in (if (I \leq M, I, M) \dots if (I \leq N, N, I)))$
49	48	ssrdv	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (M \dots N) \subseteq (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
50	49	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (M \dots N) \subseteq (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
51	1 50	sstrd	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to S \subseteq (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
52	4	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to if (I \leq M, I, M) \in ℤ$
53	28	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to if (I \leq N, N, I) \in ℤ$
54	2	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to I \in ℤ$
55	52 53 54	3jca	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (if (I \leq M, I, M) \in ℤ \land if (I \leq N, N, I) \in ℤ \land I \in ℤ)$
56	16	3adant2	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (M \in ℝ \land I \in ℝ)$
57	56	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (M \in ℝ \land I \in ℝ)$
58	57	ancomd	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (I \in ℝ \land M \in ℝ)$
59		min1	$⊢ (I \in ℝ \land M \in ℝ) \to if (I \leq M, I, M) \leq I$
60	58 59	syl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to if (I \leq M, I, M) \leq I$
61	38	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (N \in ℝ \land I \in ℝ)$
62	61	ancomd	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (I \in ℝ \land N \in ℝ)$
63		max1	$⊢ (I \in ℝ \land N \in ℝ) \to I \leq if (I \leq N, N, I)$
64	62 63	syl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to I \leq if (I \leq N, N, I)$
65	60 64	jca	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (if (I \leq M, I, M) \leq I \land I \leq if (I \leq N, N, I))$
66		elfz2	$⊢ I \in (if (I \leq M, I, M) \dots if (I \leq N, N, I)) \leftrightarrow ((if (I \leq M, I, M) \in ℤ \land if (I \leq N, N, I) \in ℤ \land I \in ℤ) \land (if (I \leq M, I, M) \leq I \land I \leq if (I \leq N, N, I)))$
67	55 65 66	sylanbrc	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to I \in (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
68	67	snssd	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to \{I\} \subseteq (if (I \leq M, I, M) \dots if (I \leq N, N, I))$
69	51 68	unssd	$⊢ (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))$

Metamath Proof Explorer

Theorem ssfzunsnext

Proof