Metamath Proof Explorer

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 ⊢ A = ℕ ∨ A = 1 ..^ M ∧ N ∈ A → 1 ..^ N ⊆ A

Proof

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