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	bilani	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → 3 = ( ♯ ‘ 𝑇 ) )
10	7 9	eqtrid	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) )
11		fzofi	⊢ ( 0 ..^ 3 ) ∈ Fin
12	11	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 0 ..^ 3 ) ∈ Fin )
13		tpfi	⊢ { 𝐴 , 𝐵 , 𝐶 } ∈ Fin
14	2 13	eqeltri	⊢ 𝑇 ∈ Fin
15	14	a1i	⊢ ( ( ♯ ‘ 𝑇 ) = 3 → 𝑇 ∈ Fin )
16		hashen	⊢ ( ( ( 0 ..^ 3 ) ∈ Fin ∧ 𝑇 ∈ Fin ) → ( ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) ↔ ( 0 ..^ 3 ) ≈ 𝑇 ) )
17	12 15 16	syl2an	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( ( ♯ ‘ ( 0 ..^ 3 ) ) = ( ♯ ‘ 𝑇 ) ↔ ( 0 ..^ 3 ) ≈ 𝑇 ) )
18	10 17	mpbid	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → ( 0 ..^ 3 ) ≈ 𝑇 )
19	14	a1i	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → 𝑇 ∈ Fin )
20		fofinf1o	⊢ ( ( 𝐹 : ( 0 ..^ 3 ) –onto→ 𝑇 ∧ ( 0 ..^ 3 ) ≈ 𝑇 ∧ 𝑇 ∈ Fin ) → 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )
21	4 18 19 20	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑇 ) = 3 ) → 𝐹 : ( 0 ..^ 3 ) –1-1-onto→ 𝑇 )