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	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
Assertion	tpf1ofv0	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 0 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		tpf1o.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
2	1	a1i	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) ) )
3		iftrue	⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) = 𝐴 )
4	3	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 = 0 ) → if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) = 𝐴 )
5		3nn	⊢ 3 ∈ ℕ
6		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ 3 ) ↔ 3 ∈ ℕ )
7	5 6	mpbir	⊢ 0 ∈ ( 0 ..^ 3 )
8	7	a1i	⊢ ( 𝐴 ∈ 𝑉 → 0 ∈ ( 0 ..^ 3 ) )
9		id	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
10	2 4 8 9	fvmptd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 0 ) = 𝐴 )