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

Proof

Step Hyp Ref Expression
1 tpf1o.f ⊢ F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
2 1 a1i ⊢ B ∈ V → F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
3 ax-1ne0 ⊢ 1 ≠ 0
4 3 neii ⊢ ¬ 1 = 0
5 eqeq1 ⊢ x = 1 → x = 0 ↔ 1 = 0
6 4 5 mtbiri ⊢ x = 1 → ¬ x = 0
7 6 iffalsed ⊢ x = 1 → if x = 0 A if x = 1 B C = if x = 1 B C
8 iftrue ⊢ x = 1 → if x = 1 B C = B
9 7 8 eqtrd ⊢ x = 1 → if x = 0 A if x = 1 B C = B
10 9 adantl ⊢ B ∈ V ∧ x = 1 → if x = 0 A if x = 1 B C = B
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 ⊢ B ∈ V → 1 ∈ 0 ..^ 3
17 id ⊢ B ∈ V → B ∈ V
18 2 10 16 17 fvmptd ⊢ B ∈ V → F ⁡ 1 = B