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 ⊢ F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
Assertion tpf1ofv2 ⊢ C ∈ V → F ⁡ 2 = C

Proof

Step Hyp Ref Expression
1 tpf1o.f ⊢ F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
2 1 a1i ⊢ C ∈ V → F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
3 2ne0 ⊢ 2 ≠ 0
4 3 neii ⊢ ¬ 2 = 0
5 eqeq1 ⊢ x = 2 → x = 0 ↔ 2 = 0
6 4 5 mtbiri ⊢ x = 2 → ¬ x = 0
7 6 iffalsed ⊢ x = 2 → if x = 0 A if x = 1 B C = if x = 1 B C
8 1re ⊢ 1 ∈ ℝ
9 1lt2 ⊢ 1 < 2
10 8 9 gtneii ⊢ 2 ≠ 1
11 10 neii ⊢ ¬ 2 = 1
12 eqeq1 ⊢ x = 2 → x = 1 ↔ 2 = 1
13 11 12 mtbiri ⊢ x = 2 → ¬ x = 1
14 13 iffalsed ⊢ x = 2 → if x = 1 B C = C
15 7 14 eqtrd ⊢ x = 2 → if x = 0 A if x = 1 B C = C
16 15 adantl ⊢ C ∈ V ∧ x = 2 → if x = 0 A if x = 1 B C = C
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 ⊢ C ∈ V → 2 ∈ 0 ..^ 3
23 id ⊢ C ∈ V → C ∈ V
24 2 16 22 23 fvmptd ⊢ C ∈ V → F ⁡ 2 = C