Metamath Proof Explorer

Theorem tpf1ofv2

Description: The value of a one-to-one function onto a triple at 2. (Contributed by AV, 20-Jul-2025)

Ref Expression
Hypothesis tpf1o.f 
|- F = ( x e. ( 0 ..^ 3 ) |-> if ( x = 0 , A , if ( x = 1 , B , C ) ) )
Assertion tpf1ofv2 
|- ( C e. V -> ( F ` 2 ) = C )

Proof

Step Hyp Ref Expression
1 tpf1o.f 
 |-  F = ( x e. ( 0 ..^ 3 ) |-> if ( x = 0 , A , if ( x = 1 , B , C ) ) )
2 1 a1i 
 |-  ( C e. V -> F = ( x e. ( 0 ..^ 3 ) |-> if ( x = 0 , A , if ( x = 1 , B , C ) ) ) )
3 2ne0 
 |-  2 =/= 0
4 3 neii 
 |-  -. 2 = 0
5 eqeq1 
 |-  ( x = 2 -> ( x = 0 <-> 2 = 0 ) )
6 4 5 mtbiri 
 |-  ( x = 2 -> -. x = 0 )
7 6 iffalsed 
 |-  ( x = 2 -> if ( x = 0 , A , if ( x = 1 , B , C ) ) = if ( x = 1 , B , C ) )
8 1re 
 |-  1 e. RR
9 1lt2 
 |-  1 < 2
10 8 9 gtneii 
 |-  2 =/= 1
11 10 neii 
 |-  -. 2 = 1
12 eqeq1 
 |-  ( x = 2 -> ( x = 1 <-> 2 = 1 ) )
13 11 12 mtbiri 
 |-  ( x = 2 -> -. x = 1 )
14 13 iffalsed 
 |-  ( x = 2 -> if ( x = 1 , B , C ) = C )
15 7 14 eqtrd 
 |-  ( x = 2 -> if ( x = 0 , A , if ( x = 1 , B , C ) ) = C )
16 15 adantl 
 |-  ( ( C e. V /\ x = 2 ) -> if ( x = 0 , A , if ( x = 1 , B , C ) ) = C )
17 2nn0 
 |-  2 e. NN0
18 3nn 
 |-  3 e. NN
19 2lt3 
 |-  2 < 3
20 elfzo0 
 |-  ( 2 e. ( 0 ..^ 3 ) <-> ( 2 e. NN0 /\ 3 e. NN /\ 2 < 3 ) )
21 17 18 19 20 mpbir3an 
 |-  2 e. ( 0 ..^ 3 )
22 21 a1i 
 |-  ( C e. V -> 2 e. ( 0 ..^ 3 ) )
23 id 
 |-  ( C e. V -> C e. V )
24 2 16 22 23 fvmptd 
 |-  ( C e. V -> ( F ` 2 ) = C )