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		simp2	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to N \in ℤ$
7	6 2	ifcld	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to if (I \leq N, N, I) \in ℤ$
8	7	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq N, N, I) \in ℤ$
9		elfzelz	$⊢ k \in (M \dots N) \to k \in ℤ$
10	9	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \in ℤ$
11	4	zred	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to if (I \leq M, I, M) \in ℝ$
12	11	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq M, I, M) \in ℝ$
13		zre	$⊢ M \in ℤ \to M \in ℝ$
14	13	3ad2ant1	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to M \in ℝ$
15	14	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to M \in ℝ$
16	9	zred	$⊢ k \in (M \dots N) \to k \in ℝ$
17	16	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \in ℝ$
18		zre	$⊢ I \in ℤ \to I \in ℝ$
19	13 18	anim12i	$⊢ (M \in ℤ \land I \in ℤ) \to (M \in ℝ \land I \in ℝ)$
20	19	ancomd	$⊢ (M \in ℤ \land I \in ℤ) \to (I \in ℝ \land M \in ℝ)$
21	20	3adant2	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (I \in ℝ \land M \in ℝ)$
22	21	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to (I \in ℝ \land M \in ℝ)$
23		min2	$⊢ (I \in ℝ \land M \in ℝ) \to if (I \leq M, I, M) \leq M$
24	22 23	syl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq M, I, M) \leq M$
25		elfzle1	$⊢ k \in (M \dots N) \to M \leq k$
26	25	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to M \leq k$
27	12 15 17 24 26	letrd	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq M, I, M) \leq k$
28		zre	$⊢ N \in ℤ \to N \in ℝ$
29	28	3ad2ant2	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to N \in ℝ$
30	29	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to N \in ℝ$
31	7	zred	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to if (I \leq N, N, I) \in ℝ$
32	31	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to if (I \leq N, N, I) \in ℝ$
33		elfzle2	$⊢ k \in (M \dots N) \to k \leq N$
34	33	adantl	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \leq N$
35	28 18	anim12i	$⊢ (N \in ℤ \land I \in ℤ) \to (N \in ℝ \land I \in ℝ)$
36	35	3adant1	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (N \in ℝ \land I \in ℝ)$
37	36	ancomd	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (I \in ℝ \land N \in ℝ)$
38		max2	$⊢ (I \in ℝ \land N \in ℝ) \to N \leq if (I \leq N, N, I)$
39	37 38	syl	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to N \leq if (I \leq N, N, I)$
40	39	adantr	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to N \leq if (I \leq N, N, I)$
41	17 30 32 34 40	letrd	$⊢ ((M \in ℤ \land N \in ℤ \land I \in ℤ) \land k \in (M \dots N)) \to k \leq if (I \leq N, N, I)$
42	5 8 10 27 41	elfzd	$⊢ ((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))$
43	42	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)))$
44	43	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))$
45	44	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))$
46	1 45	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))$
47	4	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to if (I \leq M, I, M) \in ℤ$
48	7	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to if (I \leq N, N, I) \in ℤ$
49	2	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to I \in ℤ$
50	19	3adant2	$⊢ (M \in ℤ \land N \in ℤ \land I \in ℤ) \to (M \in ℝ \land I \in ℝ)$
51	50	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (M \in ℝ \land I \in ℝ)$
52	51	ancomd	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (I \in ℝ \land M \in ℝ)$
53		min1	$⊢ (I \in ℝ \land M \in ℝ) \to if (I \leq M, I, M) \leq I$
54	52 53	syl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to if (I \leq M, I, M) \leq I$
55	36	adantl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (N \in ℝ \land I \in ℝ)$
56	55	ancomd	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to (I \in ℝ \land N \in ℝ)$
57		max1	$⊢ (I \in ℝ \land N \in ℝ) \to I \leq if (I \leq N, N, I)$
58	56 57	syl	$⊢ (S \subseteq (M \dots N) \land (M \in ℤ \land N \in ℤ \land I \in ℤ)) \to I \leq if (I \leq N, N, I)$
59	47 48 49 54 58	elfzd	$⊢ (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))$
60	59	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))$
61	46 60	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