Theorem tpf1ofv0

Description: The value of a one-to-one function onto a triple at 0. (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	tpf1ofv0	$$⊢A\in V\to F\left(0\right)=A$$

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	$$⊢A\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		iftrue	$$⊢x=0\to if\left(x=0,A,if\left(x=1,B,C\right)\right)=A$$
4	3	adantl	$$⊢\left(A\in V\wedge x=0\right)\to if\left(x=0,A,if\left(x=1,B,C\right)\right)=A$$
5		3nn	$$⊢3\in \mathbb{N}$$
6		lbfzo0	$$⊢0\in \left(0..^3\right)\leftrightarrow 3\in \mathbb{N}$$
7	5 6	mpbir	$$⊢0\in \left(0..^3\right)$$
8	7	a1i	$$⊢A\in V\to 0\in \left(0..^3\right)$$
9		id	$$⊢A\in V\to A\in V$$
10	2 4 8 9	fvmptd	$$⊢A\in V\to F\left(0\right)=A$$