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 elfzelz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℤ )
7 6 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℤ )
8 4 zred ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℝ )
9 8 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℝ )
10 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
11 10 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑀 ∈ ℝ )
12 11 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
13 6 zred ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℝ )
14 13 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ℝ )
15 zre ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
16 10 15 anim12i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
17 16 ancomd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
18 17 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
19 18 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
20 min2 ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑀 )
21 19 20 syl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑀 )
22 elfzle1 ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝑘 )
23 22 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝑘 )
24 9 12 14 21 23 letrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑘 )
25 eluz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ) ↔ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝑘 ) )
26 5 7 24 25 syl3anbrc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ) )
27 simp2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℤ )
28 27 2 ifcld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ )
29 28 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ )
30 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
31 30 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ∈ ℝ )
32 31 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
33 28 zred ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℝ )
34 33 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℝ )
35 elfzle2 ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ≤ 𝑁 )
36 35 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ≤ 𝑁 )
37 30 15 anim12i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
38 37 3adant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
39 38 ancomd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
40 max2 ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
41 39 40 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
42 41 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑁 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
43 14 32 34 36 42 letrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
44 eluz2 ⊢ ( if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ( ℤ≥ ‘ 𝑘 ) ↔ ( 𝑘 ∈ ℤ ∧ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ∧ 𝑘 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
45 7 29 43 44 syl3anbrc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ( ℤ≥ ‘ 𝑘 ) )
46 elfzuzb ⊢ ( 𝑘 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ) ∧ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ( ℤ≥ ‘ 𝑘 ) ) )
47 26 45 46 sylanbrc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑘 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
48 47 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) )
49 48 ssrdv ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
50 49 adantl ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑀 ... 𝑁 ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
51 1 50 sstrd ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝑆 ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
52 4 adantl ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ )
53 28 adantl ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ )
54 2 adantl ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ∈ ℤ )
55 52 53 54 3jca ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ∧ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ∧ 𝐼 ∈ ℤ ) )
56 16 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
57 56 adantl ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑀 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
58 57 ancomd ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
59 min1 ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 )
60 58 59 syl ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 )
61 38 adantl ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ ) )
62 61 ancomd ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
63 max1 ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
64 62 63 syl ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) )
65 60 64 jca ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 ∧ 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
66 elfz2 ⊢ ( 𝐼 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ↔ ( ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ∈ ℤ ∧ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ∈ ℤ ∧ 𝐼 ∈ ℤ ) ∧ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ≤ 𝐼 ∧ 𝐼 ≤ if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) ) )
67 55 65 66 sylanbrc ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → 𝐼 ∈ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
68 67 snssd ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → { 𝐼 } ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
69 51 68 unssd ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑆 ∪ { 𝐼 } ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )