Theorem tpf

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

	Ref	Expression
Hypotheses	tpf1o.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
	tpf.t	⊢ 𝑇 = { 𝐴 , 𝐵 , 𝐶 }
Assertion	tpf	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐹 : ( 0 ..^ 3 ) ⟶ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		tpf1o.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ 3 ) ↦ if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) )
2		tpf.t	⊢ 𝑇 = { 𝐴 , 𝐵 , 𝐶 }
3		tpid1g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } )
4	3	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } )
5		tpid2g	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } )
6	5	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐵 ∈ { 𝐴 , 𝐵 , 𝐶 } )
7		tpid3g	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
8	7	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ { 𝐴 , 𝐵 , 𝐶 } )
9	6 8	ifcld	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ∈ { 𝐴 , 𝐵 , 𝐶 } )
10	4 9	ifcld	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) ∈ { 𝐴 , 𝐵 , 𝐶 } )
11	10 2	eleqtrrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) ∈ 𝑇 )
12	11	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 0 ..^ 3 ) ) → if ( 𝑥 = 0 , 𝐴 , if ( 𝑥 = 1 , 𝐵 , 𝐶 ) ) ∈ 𝑇 )
13	12 1	fmptd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 𝐹 : ( 0 ..^ 3 ) ⟶ 𝑇 )