Theorem tpf1ofv1

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

	Ref	Expression
Hypothesis	tpf1o.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
Assertion	tpf1ofv1	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐹 ‘ 1 ) = 𝐵 )

Proof

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