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 e. ( 0 ..^ 3 ) |-> if ( x = 0 , A , if ( x = 1 , B , C ) ) )
tpf.t 
|- T = { A , B , C }
Assertion tpf 
|- ( ( A e. V /\ B e. V /\ C e. V ) -> F : ( 0 ..^ 3 ) --> T )

Proof

Step Hyp Ref Expression
1 tpf1o.f 
 |-  F = ( x e. ( 0 ..^ 3 ) |-> if ( x = 0 , A , if ( x = 1 , B , C ) ) )
2 tpf.t 
 |-  T = { A , B , C }
3 tpid1g 
 |-  ( A e. V -> A e. { A , B , C } )
4 3 3ad2ant1 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> A e. { A , B , C } )
5 tpid2g 
 |-  ( B e. V -> B e. { A , B , C } )
6 5 3ad2ant2 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> B e. { A , B , C } )
7 tpid3g 
 |-  ( C e. V -> C e. { A , B , C } )
8 7 3ad2ant3 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> C e. { A , B , C } )
9 6 8 ifcld 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> if ( x = 1 , B , C ) e. { A , B , C } )
10 4 9 ifcld 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> if ( x = 0 , A , if ( x = 1 , B , C ) ) e. { A , B , C } )
11 10 2 eleqtrrdi 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> if ( x = 0 , A , if ( x = 1 , B , C ) ) e. T )
12 11 adantr 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ x e. ( 0 ..^ 3 ) ) -> if ( x = 0 , A , if ( x = 1 , B , C ) ) e. T )
13 12 1 fmptd 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> F : ( 0 ..^ 3 ) --> T )