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

Metamath Proof Explorer

Theorem fnimatpd

Description: The image of an unordered triple under a function. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses fnimatpd.1 
|- ( ph -> F Fn D )
fnimatpd.2 
|- ( ph -> A e. D )
fnimatpd.3 
|- ( ph -> B e. D )
fnimatpd.4 
|- ( ph -> C e. D )
Assertion fnimatpd 
|- ( ph -> ( F " { A , B , C } ) = { ( F ` A ) , ( F ` B ) , ( F ` C ) } )

Proof

Step Hyp Ref Expression
1 fnimatpd.1 
 |-  ( ph -> F Fn D )
2 fnimatpd.2 
 |-  ( ph -> A e. D )
3 fnimatpd.3 
 |-  ( ph -> B e. D )
4 fnimatpd.4 
 |-  ( ph -> C e. D )
5 fnimapr 
 |-  ( ( F Fn D /\ A e. D /\ B e. D ) -> ( F " { A , B } ) = { ( F ` A ) , ( F ` B ) } )
6 1 2 3 5 syl3anc 
 |-  ( ph -> ( F " { A , B } ) = { ( F ` A ) , ( F ` B ) } )
7 fnsnfv 
 |-  ( ( F Fn D /\ C e. D ) -> { ( F ` C ) } = ( F " { C } ) )
8 1 4 7 syl2anc 
 |-  ( ph -> { ( F ` C ) } = ( F " { C } ) )
9 8 eqcomd 
 |-  ( ph -> ( F " { C } ) = { ( F ` C ) } )
10 6 9 uneq12d 
 |-  ( ph -> ( ( F " { A , B } ) u. ( F " { C } ) ) = ( { ( F ` A ) , ( F ` B ) } u. { ( F ` C ) } ) )
11 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
12 11 imaeq2i 
 |-  ( F " { A , B , C } ) = ( F " ( { A , B } u. { C } ) )
13 imaundi 
 |-  ( F " ( { A , B } u. { C } ) ) = ( ( F " { A , B } ) u. ( F " { C } ) )
14 12 13 eqtri 
 |-  ( F " { A , B , C } ) = ( ( F " { A , B } ) u. ( F " { C } ) )
15 df-tp 
 |-  { ( F ` A ) , ( F ` B ) , ( F ` C ) } = ( { ( F ` A ) , ( F ` B ) } u. { ( F ` C ) } )
16 10 14 15 3eqtr4g 
 |-  ( ph -> ( F " { A , B , C } ) = { ( F ` A ) , ( F ` B ) , ( F ` C ) } )