Metamath Proof Explorer

Theorem grtrimap

Description: Conditions for mapping triangles onto triangles. Lemma for grimgrtri and grlimgrtri . (Contributed by AV, 23-Aug-2025)

Ref Expression
Assertion grtrimap 
|- ( F : V -1-1-> W -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> ( ( ( F ` a ) e. W /\ ( F ` b ) e. W /\ ( F ` c ) e. W ) /\ ( F " T ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } /\ ( # ` ( F " T ) ) = 3 ) ) )

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : V -1-1-> W -> F : V --> W )
2 1 ffvelcdmda 
 |-  ( ( F : V -1-1-> W /\ a e. V ) -> ( F ` a ) e. W )
3 2 ex 
 |-  ( F : V -1-1-> W -> ( a e. V -> ( F ` a ) e. W ) )
4 1 ffvelcdmda 
 |-  ( ( F : V -1-1-> W /\ b e. V ) -> ( F ` b ) e. W )
5 4 ex 
 |-  ( F : V -1-1-> W -> ( b e. V -> ( F ` b ) e. W ) )
6 1 ffvelcdmda 
 |-  ( ( F : V -1-1-> W /\ c e. V ) -> ( F ` c ) e. W )
7 6 ex 
 |-  ( F : V -1-1-> W -> ( c e. V -> ( F ` c ) e. W ) )
8 3 5 7 3anim123d 
 |-  ( F : V -1-1-> W -> ( ( a e. V /\ b e. V /\ c e. V ) -> ( ( F ` a ) e. W /\ ( F ` b ) e. W /\ ( F ` c ) e. W ) ) )
9 8 adantrd 
 |-  ( F : V -1-1-> W -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> ( ( F ` a ) e. W /\ ( F ` b ) e. W /\ ( F ` c ) e. W ) ) )
10 9 imp 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( ( F ` a ) e. W /\ ( F ` b ) e. W /\ ( F ` c ) e. W ) )
11 imaeq2 
 |-  ( T = { a , b , c } -> ( F " T ) = ( F " { a , b , c } ) )
12 11 ad2antrl 
 |-  ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> ( F " T ) = ( F " { a , b , c } ) )
13 12 adantl 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( F " T ) = ( F " { a , b , c } ) )
14 f1fn 
 |-  ( F : V -1-1-> W -> F Fn V )
15 14 adantr 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> F Fn V )
16 simprl1 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> a e. V )
17 simprl2 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> b e. V )
18 simprl3 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> c e. V )
19 15 16 17 18 fnimatpd 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( F " { a , b , c } ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } )
20 13 19 eqtrd 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( F " T ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } )
21 simpl 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> F : V -1-1-> W )
22 tpssi 
 |-  ( ( a e. V /\ b e. V /\ c e. V ) -> { a , b , c } C_ V )
23 22 adantr 
 |-  ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> { a , b , c } C_ V )
24 sseq1 
 |-  ( T = { a , b , c } -> ( T C_ V <-> { a , b , c } C_ V ) )
25 24 ad2antrl 
 |-  ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> ( T C_ V <-> { a , b , c } C_ V ) )
26 23 25 mpbird 
 |-  ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> T C_ V )
27 26 adantl 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> T C_ V )
28 tpex 
 |-  { a , b , c } e. _V
29 eleq1 
 |-  ( T = { a , b , c } -> ( T e. _V <-> { a , b , c } e. _V ) )
30 28 29 mpbiri 
 |-  ( T = { a , b , c } -> T e. _V )
31 30 ad2antrl 
 |-  ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> T e. _V )
32 31 adantl 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> T e. _V )
33 f1imaeng 
 |-  ( ( F : V -1-1-> W /\ T C_ V /\ T e. _V ) -> ( F " T ) ~~ T )
34 hasheni 
 |-  ( ( F " T ) ~~ T -> ( # ` ( F " T ) ) = ( # ` T ) )
35 33 34 syl 
 |-  ( ( F : V -1-1-> W /\ T C_ V /\ T e. _V ) -> ( # ` ( F " T ) ) = ( # ` T ) )
36 35 eqcomd 
 |-  ( ( F : V -1-1-> W /\ T C_ V /\ T e. _V ) -> ( # ` T ) = ( # ` ( F " T ) ) )
37 21 27 32 36 syl3anc 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( # ` T ) = ( # ` ( F " T ) ) )
38 simprrr 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( # ` T ) = 3 )
39 37 38 eqtr3d 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( # ` ( F " T ) ) = 3 )
40 10 20 39 3jca 
 |-  ( ( F : V -1-1-> W /\ ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( ( ( F ` a ) e. W /\ ( F ` b ) e. W /\ ( F ` c ) e. W ) /\ ( F " T ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } /\ ( # ` ( F " T ) ) = 3 ) )
41 40 ex 
 |-  ( F : V -1-1-> W -> ( ( ( a e. V /\ b e. V /\ c e. V ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> ( ( ( F ` a ) e. W /\ ( F ` b ) e. W /\ ( F ` c ) e. W ) /\ ( F " T ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } /\ ( # ` ( F " T ) ) = 3 ) ) )