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

Metamath Proof Explorer

Theorem tpf1ofv1

Description: The value of a one-to-one function onto a triple at 1. (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 tpf1ofv1 
|- ( B e. V -> ( F ` 1 ) = B )

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 
 |-  ( B e. V -> F = ( x e. ( 0 ..^ 3 ) |-> if ( x = 0 , A , if ( x = 1 , B , C ) ) ) )
3 ax-1ne0 
 |-  1 =/= 0
4 3 neii 
 |-  -. 1 = 0
5 eqeq1 
 |-  ( x = 1 -> ( x = 0 <-> 1 = 0 ) )
6 4 5 mtbiri 
 |-  ( x = 1 -> -. x = 0 )
7 6 iffalsed 
 |-  ( x = 1 -> if ( x = 0 , A , if ( x = 1 , B , C ) ) = if ( x = 1 , B , C ) )
8 iftrue 
 |-  ( x = 1 -> if ( x = 1 , B , C ) = B )
9 7 8 eqtrd 
 |-  ( x = 1 -> if ( x = 0 , A , if ( x = 1 , B , C ) ) = B )
10 9 adantl 
 |-  ( ( B e. V /\ x = 1 ) -> if ( x = 0 , A , if ( x = 1 , B , C ) ) = B )
11 1nn0 
 |-  1 e. NN0
12 3nn 
 |-  3 e. NN
13 1lt3 
 |-  1 < 3
14 elfzo0 
 |-  ( 1 e. ( 0 ..^ 3 ) <-> ( 1 e. NN0 /\ 3 e. NN /\ 1 < 3 ) )
15 11 12 13 14 mpbir3an 
 |-  1 e. ( 0 ..^ 3 )
16 15 a1i 
 |-  ( B e. V -> 1 e. ( 0 ..^ 3 ) )
17 id 
 |-  ( B e. V -> B e. V )
18 2 10 16 17 fvmptd 
 |-  ( B e. V -> ( F ` 1 ) = B )