Metamath Proof Explorer

Theorem tpf

Description: A function into a (proper) triple. (Contributed by AV, 20-Jul-2025)

Ref Expression
Hypotheses tpf1o.f ⊢ F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
tpf.t ⊢ T = A B C
Assertion tpf ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → F : 0 ..^ 3 ⟶ T

Proof

Step Hyp Ref Expression
1 tpf1o.f ⊢ F = x ∈ 0 ..^ 3 ⟼ if x = 0 A if x = 1 B C
2 tpf.t ⊢ T = A B C
3 tpid1g ⊢ A ∈ V → A ∈ A B C
4 3 3ad2ant1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ A B C
5 tpid2g ⊢ B ∈ V → B ∈ A B C
6 5 3ad2ant2 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → B ∈ A B C
7 tpid3g ⊢ C ∈ V → C ∈ A B C
8 7 3ad2ant3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ A B C
9 6 8 ifcld ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → if x = 1 B C ∈ A B C
10 4 9 ifcld ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → if x = 0 A if x = 1 B C ∈ A B C
11 10 2 eleqtrrdi ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → if x = 0 A if x = 1 B C ∈ T
12 11 adantr ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ x ∈ 0 ..^ 3 → if x = 0 A if x = 1 B C ∈ T
13 12 1 fmptd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → F : 0 ..^ 3 ⟶ T