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

Metamath Proof Explorer

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