Theorem tpf1o

Description: A bijection onto a (proper) triple. (Contributed by AV, 21-Jul-2025)

	Ref	Expression
Hypotheses	tpf1o.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
	tpf.t	⊢ 𝑇 = { 𝐴 , 𝐵 , 𝐶 }
Assertion	tpf1o	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		tpf1o.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
2		tpf.t	⊢ 𝑇 = { 𝐴 , 𝐵 , 𝐶 }
3	1 2	tpfo	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐹 : ( 0 ..^ 3 ) –onto→ 𝑇 )
4	3	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → 𝐹 : ( 0 ..^ 3 ) –onto→ 𝑇 )
5		3nn0	⊢ 3 ∈ ℕ0
6		hashfzo0	⊢ ( 3 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 3 ) ) = 3 )
7	5 6	ax-mp	⊢ ( ♯ ‘ ( 0 ..^ 3 ) ) = 3
8		eqcom	⊢ ( ( ♯ ‘ 𝑇 ) = 3 ↔ 3 = ( ♯ ‘ 𝑇 ) )
9	8	biimpi	⊢ ( ( ♯ ‘ 𝑇 ) = 3 → 3 = ( ♯ ‘ 𝑇 ) )
10	9	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → 3 = ( ♯ ‘ 𝑇 ) )
11	7 10	eqtrid	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) )
12		fzofi	⊢ ( 0 ..^ 3 ) ∈ Fin
13	12	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 0 ..^ 3 ) ∈ Fin )
14		tpfi	⊢ { 𝐴 , 𝐵 , 𝐶 } ∈ Fin
15	2 14	eqeltri	⊢ 𝑇 ∈ Fin
16	15	a1i	⊢ ( ( ♯ ‘ 𝑇 ) = 3 → 𝑇 ∈ Fin )
17		hashen	⊢ ( ( ( 0 ..^ 3 ) ∈ Fin ∧ 𝑇 ∈ Fin ) → ( ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) ↔ ( 0 ..^ 3 ) ≈ 𝑇 ) )
18	13 16 17	syl2an	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) ↔ ( 0 ..^ 3 ) ≈ 𝑇 ) )
19	11 18	mpbid	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( 0 ..^ 3 ) ≈ 𝑇 )
20	15	a1i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → 𝑇 ∈ Fin )
21		fofinf1o	⊢ ( ( 𝐹 : ( 0 ..^ 3 ) –onto→ 𝑇 ∧ ( 0 ..^ 3 ) ≈ 𝑇 ∧ 𝑇 ∈ Fin ) → 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )
22	4 19 20 21	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )