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

Metamath Proof Explorer

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