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

Proof

Step	Hyp	Ref	Expression
1		tpf1o.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
2	1	a1i	⊢ ( 𝐶 ∈ 𝑉 → 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) ) )
3		2ne0	⊢ 2 ≠ 0
4	3	neii	⊢ ¬ 2 = 0
5		eqeq1	⊢ ( 𝑥 = 2 → ( 𝑥 = 0 ↔ 2 = 0 ) )
6	4 5	mtbiri	⊢ ( 𝑥 = 2 → ¬ 𝑥 = 0 )
7	6	iffalsed	⊢ ( 𝑥 = 2 → if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) = if ( 𝑥 = 1 , 𝐵 , 𝐶 ) )
8		1re	⊢ 1 ∈ ℝ
9		1lt2	⊢ 1 < 2
10	8 9	gtneii	⊢ 2 ≠ 1
11	10	neii	⊢ ¬ 2 = 1
12		eqeq1	⊢ ( 𝑥 = 2 → ( 𝑥 = 1 ↔ 2 = 1 ) )
13	11 12	mtbiri	⊢ ( 𝑥 = 2 → ¬ 𝑥 = 1 )
14	13	iffalsed	⊢ ( 𝑥 = 2 → if ( 𝑥 = 1 , 𝐵 , 𝐶 ) = 𝐶 )
15	7 14	eqtrd	⊢ ( 𝑥 = 2 → if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) = 𝐶 )
16	15	adantl	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝑥 = 2 ) → if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) = 𝐶 )
17		2nn0	⊢ 2 ∈ ℕ0
18		3nn	⊢ 3 ∈ ℕ
19		2lt3	⊢ 2 < 3
20		elfzo0	⊢ ( 2 ∈ ( 0 ..^ 3 ) ↔ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2 < 3 ) )
21	17 18 19 20	mpbir3an	⊢ 2 ∈ ( 0 ..^ 3 )
22	21	a1i	⊢ ( 𝐶 ∈ 𝑉 → 2 ∈ ( 0 ..^ 3 ) )
23		id	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ 𝑉 )
24	2 16 22 23	fvmptd	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐹 ‘ 2 ) = 𝐶 )