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 = NN \/ A = ( 1 ..^ M ) ) /\ N e. A ) -> ( 1 ..^ N ) C_ A )

Proof

Step	Hyp	Ref	Expression
1		fzossnn	|- ( 1 ..^ N ) C_ NN
2		sseq2	|- ( A = NN -> ( ( 1 ..^ N ) C_ A <-> ( 1 ..^ N ) C_ NN ) )
3	1 2	mpbiri	|- ( A = NN -> ( 1 ..^ N ) C_ A )
4	3	adantr	|- ( ( A = NN /\ N e. A ) -> ( 1 ..^ N ) C_ A )
5		elfzouz2	|- ( N e. ( 1 ..^ M ) -> M e. ( ZZ>= ` N ) )
6		fzoss2	|- ( M e. ( ZZ>= ` N ) -> ( 1 ..^ N ) C_ ( 1 ..^ M ) )
7	5 6	syl	|- ( N e. ( 1 ..^ M ) -> ( 1 ..^ N ) C_ ( 1 ..^ M ) )
8		eleq2	|- ( A = ( 1 ..^ M ) -> ( N e. A <-> N e. ( 1 ..^ M ) ) )
9		sseq2	|- ( A = ( 1 ..^ M ) -> ( ( 1 ..^ N ) C_ A <-> ( 1 ..^ N ) C_ ( 1 ..^ M ) ) )
10	8 9	imbi12d	|- ( A = ( 1 ..^ M ) -> ( ( N e. A -> ( 1 ..^ N ) C_ A ) <-> ( N e. ( 1 ..^ M ) -> ( 1 ..^ N ) C_ ( 1 ..^ M ) ) ) )
11	7 10	mpbiri	|- ( A = ( 1 ..^ M ) -> ( N e. A -> ( 1 ..^ N ) C_ A ) )
12	11	imp	|- ( ( A = ( 1 ..^ M ) /\ N e. A ) -> ( 1 ..^ N ) C_ A )
13	4 12	jaoian	|- ( ( ( A = NN \/ A = ( 1 ..^ M ) ) /\ N e. A ) -> ( 1 ..^ N ) C_ A )