Theorem fzo1to4tp

Description: A half-open integer range from 1 to 4 is an unordered triple. (Contributed by AV, 28-Jul-2021)

	Ref	Expression
Assertion	fzo1to4tp	|- ( 1 ..^ 4 ) = { 1 , 2 , 3 }

Proof

Step	Hyp	Ref	Expression
1		4z	|- 4 e. ZZ
2		fzoval	|- ( 4 e. ZZ -> ( 1 ..^ 4 ) = ( 1 ... ( 4 - 1 ) ) )
3	1 2	ax-mp	|- ( 1 ..^ 4 ) = ( 1 ... ( 4 - 1 ) )
4		4m1e3	|- ( 4 - 1 ) = 3
5		df-3	|- 3 = ( 2 + 1 )
6		2cn	|- 2 e. CC
7		ax-1cn	|- 1 e. CC
8	6 7	addcomi	|- ( 2 + 1 ) = ( 1 + 2 )
9	4 5 8	3eqtri	|- ( 4 - 1 ) = ( 1 + 2 )
10	9	oveq2i	|- ( 1 ... ( 4 - 1 ) ) = ( 1 ... ( 1 + 2 ) )
11		1z	|- 1 e. ZZ
12		fztp	|- ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
13		eqidd	|- ( 1 e. ZZ -> 1 = 1 )
14		1p1e2	|- ( 1 + 1 ) = 2
15	14	a1i	|- ( 1 e. ZZ -> ( 1 + 1 ) = 2 )
16		1p2e3	|- ( 1 + 2 ) = 3
17	16	a1i	|- ( 1 e. ZZ -> ( 1 + 2 ) = 3 )
18	13 15 17	tpeq123d	|- ( 1 e. ZZ -> { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 } )
19	12 18	eqtrd	|- ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , 2 , 3 } )
20	11 19	ax-mp	|- ( 1 ... ( 1 + 2 ) ) = { 1 , 2 , 3 }
21	3 10 20	3eqtri	|- ( 1 ..^ 4 ) = { 1 , 2 , 3 }