Theorem tpf1o

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

	Ref	Expression
Hypotheses	tpf1o.f	|- F = ( x e. ( 0 ..^ 3 ) |-> if ( x = 0 , A , if ( x = 1 , B , C ) ) )
	tpf.t	|- T = { A , B , C }
Assertion	tpf1o	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( # ` T ) = 3 ) -> F : ( 0 ..^ 3 ) -1-1-onto-> T )

Proof

Step	Hyp	Ref	Expression
1		tpf1o.f	|- F = ( x e. ( 0 ..^ 3 ) |-> if ( x = 0 , A , if ( x = 1 , B , C ) ) )
2		tpf.t	|- T = { A , B , C }
3	1 2	tpfo	|- ( ( A e. V /\ B e. V /\ C e. V ) -> F : ( 0 ..^ 3 ) -onto-> T )
4	3	adantr	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( # ` T ) = 3 ) -> F : ( 0 ..^ 3 ) -onto-> T )
5		3nn0	|- 3 e. NN0
6		hashfzo0	|- ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 )
7	5 6	ax-mp	|- ( # ` ( 0 ..^ 3 ) ) = 3
8		eqcom	|- ( ( # ` T ) = 3 <-> 3 = ( # ` T ) )
9	8	biimpi	|- ( ( # ` T ) = 3 -> 3 = ( # ` T ) )
10	9	adantl	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( # ` T ) = 3 ) -> 3 = ( # ` T ) )
11	7 10	eqtrid	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( # ` T ) = 3 ) -> ( # ` ( 0 ..^ 3 ) ) = ( # ` T ) )
12		fzofi	|- ( 0 ..^ 3 ) e. Fin
13	12	a1i	|- ( ( A e. V /\ B e. V /\ C e. V ) -> ( 0 ..^ 3 ) e. Fin )
14		tpfi	|- { A , B , C } e. Fin
15	2 14	eqeltri	|- T e. Fin
16	15	a1i	|- ( ( # ` T ) = 3 -> T e. Fin )
17		hashen	|- ( ( ( 0 ..^ 3 ) e. Fin /\ T e. Fin ) -> ( ( # ` ( 0 ..^ 3 ) ) = ( # ` T ) <-> ( 0 ..^ 3 ) ~~ T ) )
18	13 16 17	syl2an	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( # ` T ) = 3 ) -> ( ( # ` ( 0 ..^ 3 ) ) = ( # ` T ) <-> ( 0 ..^ 3 ) ~~ T ) )
19	11 18	mpbid	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( # ` T ) = 3 ) -> ( 0 ..^ 3 ) ~~ T )
20	15	a1i	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( # ` T ) = 3 ) -> T e. Fin )
21		fofinf1o	|- ( ( F : ( 0 ..^ 3 ) -onto-> T /\ ( 0 ..^ 3 ) ~~ T /\ T e. Fin ) -> F : ( 0 ..^ 3 ) -1-1-onto-> T )
22	4 19 20 21	syl3anc	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( # ` T ) = 3 ) -> F : ( 0 ..^ 3 ) -1-1-onto-> T )