This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )