# 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 ${⊢}\left({S}\subseteq \left({M}\dots {N}\right)\wedge \left({M}\in ℤ\wedge {N}\in ℤ\wedge {I}\in ℤ\right)\right)\to {S}\cup \left\{{I}\right\}\subseteq \left(if\left({I}\le {M},{I},{M}\right)\dots if\left({I}\le {N},{N},{I}\right)\right)$

### Proof

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