Theorem fnimatp

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

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

Proof

Step	Hyp	Ref	Expression
1		fnimatp.1	|- ( ph -> F Fn D )
2		fnimatp.2	|- ( ph -> A e. D )
3		fnimatp.3	|- ( ph -> B e. D )
4		fnimatp.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 ) } )