Theorem fz1nntr

Description: NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020)

	Ref	Expression
Assertion	fz1nntr	⊢ ( ( ( 𝐴 = ℕ ∨ 𝐴 = ( 1 ..^ 𝑀 ) ) ∧ 𝑁 ∈ 𝐴 ) → ( 1 ..^ 𝑁 ) ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fzossnn	⊢ ( 1 ..^ 𝑁 ) ⊆ ℕ
2		sseq2	⊢ ( 𝐴 = ℕ → ( ( 1 ..^ 𝑁 ) ⊆ 𝐴 ↔ ( 1 ..^ 𝑁 ) ⊆ ℕ ) )
3	1 2	mpbiri	⊢ ( 𝐴 = ℕ → ( 1 ..^ 𝑁 ) ⊆ 𝐴 )
4	3	adantr	⊢ ( ( 𝐴 = ℕ ∧ 𝑁 ∈ 𝐴 ) → ( 1 ..^ 𝑁 ) ⊆ 𝐴 )
5		elfzouz2	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
6		fzoss2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 1 ..^ 𝑁 ) ⊆ ( 1 ..^ 𝑀 ) )
7	5 6	syl	⊢ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) → ( 1 ..^ 𝑁 ) ⊆ ( 1 ..^ 𝑀 ) )
8		eleq2	⊢ ( 𝐴 = ( 1 ..^ 𝑀 ) → ( 𝑁 ∈ 𝐴 ↔ 𝑁 ∈ ( 1 ..^ 𝑀 ) ) )
9		sseq2	⊢ ( 𝐴 = ( 1 ..^ 𝑀 ) → ( ( 1 ..^ 𝑁 ) ⊆ 𝐴 ↔ ( 1 ..^ 𝑁 ) ⊆ ( 1 ..^ 𝑀 ) ) )
10	8 9	imbi12d	⊢ ( 𝐴 = ( 1 ..^ 𝑀 ) → ( ( 𝑁 ∈ 𝐴 → ( 1 ..^ 𝑁 ) ⊆ 𝐴 ) ↔ ( 𝑁 ∈ ( 1 ..^ 𝑀 ) → ( 1 ..^ 𝑁 ) ⊆ ( 1 ..^ 𝑀 ) ) ) )
11	7 10	mpbiri	⊢ ( 𝐴 = ( 1 ..^ 𝑀 ) → ( 𝑁 ∈ 𝐴 → ( 1 ..^ 𝑁 ) ⊆ 𝐴 ) )
12	11	imp	⊢ ( ( 𝐴 = ( 1 ..^ 𝑀 ) ∧ 𝑁 ∈ 𝐴 ) → ( 1 ..^ 𝑁 ) ⊆ 𝐴 )
13	4 12	jaoian	⊢ ( ( ( 𝐴 = ℕ ∨ 𝐴 = ( 1 ..^ 𝑀 ) ) ∧ 𝑁 ∈ 𝐴 ) → ( 1 ..^ 𝑁 ) ⊆ 𝐴 )