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