Theorem tpf1ofv2

Description: The value of a one-to-one function onto a triple at 2. (Contributed by AV, 20-Jul-2025)

	Ref	Expression
Hypothesis	tpf1o.f	$$⊢F=\left(x\in \left(0..^3\right)⟼if\left(x=0,A,if\left(x=1,B,C\right)\right)\right)$$
Assertion	tpf1ofv2	$$⊢C\in V\to F\left(2\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		tpf1o.f	$$⊢F=\left(x\in \left(0..^3\right)⟼if\left(x=0,A,if\left(x=1,B,C\right)\right)\right)$$
2	1	a1i	$$⊢C\in V\to F=\left(x\in \left(0..^3\right)⟼if\left(x=0,A,if\left(x=1,B,C\right)\right)\right)$$
3		2ne0	$$⊢2\ne 0$$
4	3	neii	$$⊢\neg 2=0$$
5		eqeq1	$$⊢x=2\to \left(x=0\leftrightarrow 2=0\right)$$
6	4 5	mtbiri	$$⊢x=2\to \neg x=0$$
7	6	iffalsed	$$⊢x=2\to if\left(x=0,A,if\left(x=1,B,C\right)\right)=if\left(x=1,B,C\right)$$
8		1re	$$⊢1\in ℝ$$
9		1lt2	$$⊢1<2$$
10	8 9	gtneii	$$⊢2\ne 1$$
11	10	neii	$$⊢\neg 2=1$$
12		eqeq1	$$⊢x=2\to \left(x=1\leftrightarrow 2=1\right)$$
13	11 12	mtbiri	$$⊢x=2\to \neg x=1$$
14	13	iffalsed	$$⊢x=2\to if\left(x=1,B,C\right)=C$$
15	7 14	eqtrd	$$⊢x=2\to if\left(x=0,A,if\left(x=1,B,C\right)\right)=C$$
16	15	adantl	$$⊢\left(C\in V\wedge x=2\right)\to if\left(x=0,A,if\left(x=1,B,C\right)\right)=C$$
17		2nn0	$$⊢2\in {\mathbb{N}}_0$$
18		3nn	$$⊢3\in \mathbb{N}$$
19		2lt3	$$⊢2<3$$
20		elfzo0	$$⊢2\in \left(0..^3\right)\leftrightarrow \left(2\in {\mathbb{N}}_0\wedge 3\in \mathbb{N}\wedge 2<3\right)$$
21	17 18 19 20	mpbir3an	$$⊢2\in \left(0..^3\right)$$
22	21	a1i	$$⊢C\in V\to 2\in \left(0..^3\right)$$
23		id	$$⊢C\in V\to C\in V$$
24	2 16 22 23	fvmptd	$$⊢C\in V\to F\left(2\right)=C$$