This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ⟶ 𝑇 )