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 ∈ ℤ
2		fzoval	⊢ ( 4 ∈ ℤ → ( 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 ∈ ℂ
7		ax-1cn	⊢ 1 ∈ ℂ
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 ∈ ℤ
12		fztp	⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
13		eqidd	⊢ ( 1 ∈ ℤ → 1 = 1 )
14		1p1e2	⊢ ( 1 + 1 ) = 2
15	14	a1i	⊢ ( 1 ∈ ℤ → ( 1 + 1 ) = 2 )
16		1p2e3	⊢ ( 1 + 2 ) = 3
17	16	a1i	⊢ ( 1 ∈ ℤ → ( 1 + 2 ) = 3 )
18	13 15 17	tpeq123d	⊢ ( 1 ∈ ℤ → { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 } )
19	12 18	eqtrd	⊢ ( 1 ∈ ℤ → ( 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 }