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

Proof

Step Hyp Ref Expression
1 tpf1o.f ⊢ F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
2 1 a1i ⊢ A ∈ V → F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
3 iftrue ⊢ x = 0 → if x = 0 A if x = 1 B C = A
4 3 adantl ⊢ A ∈ V ∧ x = 0 → if x = 0 A if x = 1 B C = A
5 3nn ⊢ 3 ∈ ℕ
6 lbfzo0 ⊢ 0 ∈ 0 ..^ 3 ↔ 3 ∈ ℕ
7 5 6 mpbir ⊢ 0 ∈ 0 ..^ 3
8 7 a1i ⊢ A ∈ V → 0 ∈ 0 ..^ 3
9 id ⊢ A ∈ V → A ∈ V
10 2 4 8 9 fvmptd ⊢ A ∈ V → F ⁡ 0 = A