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

Metamath Proof Explorer

Theorem ssfzunsn

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, 8-Jun-2021) (Proof shortened by AV, 13-Nov-2021)

Ref Expression
Assertion ssfzunsn ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑆 ∪ { 𝐼 } ) ⊆ ( 𝑀 ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑆 ⊆ ( 𝑀 ... 𝑁 ) )
2 eluzel2 ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
3 2 3ad2ant3 ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 ∈ ℤ )
4 simp2 ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ ℤ )
5 eluzelz ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐼 ∈ ℤ )
6 5 3ad2ant3 ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐼 ∈ ℤ )
7 ssfzunsnext ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℤ ) ) → ( 𝑆 ∪ { 𝐼 } ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
8 1 3 4 6 7 syl13anc ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑆 ∪ { 𝐼 } ) ⊆ ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
9 eluz2 ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) )
10 zre ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
11 10 rexrd ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ* )
12 11 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → 𝐼 ∈ ℝ* )
13 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
14 13 rexrd ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ* )
15 14 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → 𝑀 ∈ ℝ* )
16 simp3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → 𝑀 ≤ 𝐼 )
17 xrmineq ⊢ ( ( 𝐼 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝐼 ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) = 𝑀 )
18 12 15 16 17 syl3anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) = 𝑀 )
19 18 eqcomd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝑀 ≤ 𝐼 ) → 𝑀 = if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) )
20 9 19 sylbi ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 = if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) )
21 20 3ad2ant3 ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑀 = if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) )
22 21 oveq1d ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) = ( if ( 𝐼 ≤ 𝑀 , 𝐼 , 𝑀 ) ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )
23 8 22 sseqtrrd ⊢ ( ( 𝑆 ⊆ ( 𝑀 ... 𝑁 ) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑆 ∪ { 𝐼 } ) ⊆ ( 𝑀 ... if ( 𝐼 ≤ 𝑁 , 𝑁 , 𝐼 ) ) )