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

Metamath Proof Explorer

Theorem tpfo

Description: A function onto 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 tpfo 
|- ( ( A e. V /\ B e. V /\ C e. V ) -> F : ( 0 ..^ 3 ) -onto-> 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 1 2 tpf 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> F : ( 0 ..^ 3 ) --> T )
4 eltpi 
 |-  ( t e. { A , B , C } -> ( t = A \/ t = B \/ t = C ) )
5 3nn 
 |-  3 e. NN
6 lbfzo0 
 |-  ( 0 e. ( 0 ..^ 3 ) <-> 3 e. NN )
7 5 6 mpbir 
 |-  0 e. ( 0 ..^ 3 )
8 7 a1i 
 |-  ( A e. V -> 0 e. ( 0 ..^ 3 ) )
9 fveq2 
 |-  ( i = 0 -> ( F ` i ) = ( F ` 0 ) )
10 9 eqeq2d 
 |-  ( i = 0 -> ( A = ( F ` i ) <-> A = ( F ` 0 ) ) )
11 10 adantl 
 |-  ( ( A e. V /\ i = 0 ) -> ( A = ( F ` i ) <-> A = ( F ` 0 ) ) )
12 1 tpf1ofv0 
 |-  ( A e. V -> ( F ` 0 ) = A )
13 12 eqcomd 
 |-  ( A e. V -> A = ( F ` 0 ) )
14 8 11 13 rspcedvd 
 |-  ( A e. V -> E. i e. ( 0 ..^ 3 ) A = ( F ` i ) )
15 eqeq1 
 |-  ( t = A -> ( t = ( F ` i ) <-> A = ( F ` i ) ) )
16 15 rexbidv 
 |-  ( t = A -> ( E. i e. ( 0 ..^ 3 ) t = ( F ` i ) <-> E. i e. ( 0 ..^ 3 ) A = ( F ` i ) ) )
17 14 16 syl5ibrcom 
 |-  ( A e. V -> ( t = A -> E. i e. ( 0 ..^ 3 ) t = ( F ` i ) ) )
18 1nn0 
 |-  1 e. NN0
19 1lt3 
 |-  1 < 3
20 elfzo0 
 |-  ( 1 e. ( 0 ..^ 3 ) <-> ( 1 e. NN0 /\ 3 e. NN /\ 1 < 3 ) )
21 18 5 19 20 mpbir3an 
 |-  1 e. ( 0 ..^ 3 )
22 21 a1i 
 |-  ( B e. V -> 1 e. ( 0 ..^ 3 ) )
23 fveq2 
 |-  ( i = 1 -> ( F ` i ) = ( F ` 1 ) )
24 23 eqeq2d 
 |-  ( i = 1 -> ( B = ( F ` i ) <-> B = ( F ` 1 ) ) )
25 24 adantl 
 |-  ( ( B e. V /\ i = 1 ) -> ( B = ( F ` i ) <-> B = ( F ` 1 ) ) )
26 1 tpf1ofv1 
 |-  ( B e. V -> ( F ` 1 ) = B )
27 26 eqcomd 
 |-  ( B e. V -> B = ( F ` 1 ) )
28 22 25 27 rspcedvd 
 |-  ( B e. V -> E. i e. ( 0 ..^ 3 ) B = ( F ` i ) )
29 eqeq1 
 |-  ( t = B -> ( t = ( F ` i ) <-> B = ( F ` i ) ) )
30 29 rexbidv 
 |-  ( t = B -> ( E. i e. ( 0 ..^ 3 ) t = ( F ` i ) <-> E. i e. ( 0 ..^ 3 ) B = ( F ` i ) ) )
31 28 30 syl5ibrcom 
 |-  ( B e. V -> ( t = B -> E. i e. ( 0 ..^ 3 ) t = ( F ` i ) ) )
32 2nn0 
 |-  2 e. NN0
33 2lt3 
 |-  2 < 3
34 elfzo0 
 |-  ( 2 e. ( 0 ..^ 3 ) <-> ( 2 e. NN0 /\ 3 e. NN /\ 2 < 3 ) )
35 32 5 33 34 mpbir3an 
 |-  2 e. ( 0 ..^ 3 )
36 35 a1i 
 |-  ( C e. V -> 2 e. ( 0 ..^ 3 ) )
37 fveq2 
 |-  ( i = 2 -> ( F ` i ) = ( F ` 2 ) )
38 37 eqeq2d 
 |-  ( i = 2 -> ( C = ( F ` i ) <-> C = ( F ` 2 ) ) )
39 38 adantl 
 |-  ( ( C e. V /\ i = 2 ) -> ( C = ( F ` i ) <-> C = ( F ` 2 ) ) )
40 1 tpf1ofv2 
 |-  ( C e. V -> ( F ` 2 ) = C )
41 40 eqcomd 
 |-  ( C e. V -> C = ( F ` 2 ) )
42 36 39 41 rspcedvd 
 |-  ( C e. V -> E. i e. ( 0 ..^ 3 ) C = ( F ` i ) )
43 eqeq1 
 |-  ( t = C -> ( t = ( F ` i ) <-> C = ( F ` i ) ) )
44 43 rexbidv 
 |-  ( t = C -> ( E. i e. ( 0 ..^ 3 ) t = ( F ` i ) <-> E. i e. ( 0 ..^ 3 ) C = ( F ` i ) ) )
45 42 44 syl5ibrcom 
 |-  ( C e. V -> ( t = C -> E. i e. ( 0 ..^ 3 ) t = ( F ` i ) ) )
46 17 31 45 3jaao 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( t = A \/ t = B \/ t = C ) -> E. i e. ( 0 ..^ 3 ) t = ( F ` i ) ) )
47 4 46 syl5com 
 |-  ( t e. { A , B , C } -> ( ( A e. V /\ B e. V /\ C e. V ) -> E. i e. ( 0 ..^ 3 ) t = ( F ` i ) ) )
48 47 2 eleq2s 
 |-  ( t e. T -> ( ( A e. V /\ B e. V /\ C e. V ) -> E. i e. ( 0 ..^ 3 ) t = ( F ` i ) ) )
49 48 com12 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( t e. T -> E. i e. ( 0 ..^ 3 ) t = ( F ` i ) ) )
50 49 ralrimiv 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> A. t e. T E. i e. ( 0 ..^ 3 ) t = ( F ` i ) )
51 dffo3 
 |-  ( F : ( 0 ..^ 3 ) -onto-> T <-> ( F : ( 0 ..^ 3 ) --> T /\ A. t e. T E. i e. ( 0 ..^ 3 ) t = ( F ` i ) ) )
52 3 50 51 sylanbrc 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> F : ( 0 ..^ 3 ) -onto-> T )