This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) = 𝐴 )