Theorem 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	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑆 ∪ { 𝐼 } ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝑆 ⊆ ( 𝑀 ... 𝑁 ) )
2		simp3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝐼 ∈ ℤ )
3		simp1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑀 ∈ ℤ )
4	2 3	ifcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ )
5	4	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ )
6		simp2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℤ )
7	6 2	ifcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ )
8	7	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ )
9		elfzelz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℤ )
10	9	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
11	4	zred	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℝ )
12	11	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℝ )
13		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
14	13	3ad2ant1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑀 ∈ ℝ )
15	14	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
16	9	zred	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℝ )
17	16	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
18		zre	⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
19	13 18	anim12i	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
20	19	ancomd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
21	20	3adant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
22	21	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
23		min2	⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑀 )
24	22 23	syl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑀 )
25		elfzle1	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝑘 )
26	25	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝑘 )
27	12 15 17 24 26	letrd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑘 )
28		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
29	28	3ad2ant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℝ )
30	29	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
31	7	zred	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℝ )
32	31	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℝ )
33		elfzle2	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ≤ 𝑁 )
34	33	adantl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ≤ 𝑁 )
35	28 18	anim12i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
36	35	3adant1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
37	36	ancomd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
38		max2	⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
39	37 38	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
40	39	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
41	17 30 32 34 40	letrd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
42	5 8 10 27 41	elfzd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
43	42	ex	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) )
44	43	ssrdv	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
45	44	adantl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑀 ... 𝑁 ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
46	1 45	sstrd	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝑆 ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
47	4	adantl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ )
48	7	adantl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ )
49	2	adantl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ∈ ℤ )
50	19	3adant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
51	50	adantl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
52	51	ancomd	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
53		min1	⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 )
54	52 53	syl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 )
55	36	adantl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
56	55	ancomd	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
57		max1	⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
58	56 57	syl	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
59	47 48 49 54 58	elfzd	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
60	59	snssd	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → { 𝐼 } ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
61	46 60	unssd	⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑆 ∪ { 𝐼 } ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )