Theorem fnimatp

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

	Ref	Expression
Hypotheses	fnimatp.1	⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
	fnimatp.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	fnimatp.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	fnimatp.4	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
Assertion	fnimatp	⊢ ( 𝜑 → ( 𝐹 “ { 𝐴 , 𝐵 , 𝐶 } ) = { ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐶 ) } )

Proof

Step	Hyp	Ref	Expression
1		fnimatp.1	⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
2		fnimatp.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
3		fnimatp.3	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
4		fnimatp.4	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
5		fnimapr	⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐹 “ { 𝐴 , 𝐵 } ) = { ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) } )
6	1 2 3 5	syl3anc	⊢ ( 𝜑 → ( 𝐹 “ { 𝐴 , 𝐵 } ) = { ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) } )
7		fnsnfv	⊢ ( ( 𝐹 Fn 𝐷 ∧ 𝐶 ∈ 𝐷 ) → { ( 𝐹 ‘ 𝐶 ) } = ( 𝐹 “ { 𝐶 } ) )
8	1 4 7	syl2anc	⊢ ( 𝜑 → { ( 𝐹 ‘ 𝐶 ) } = ( 𝐹 “ { 𝐶 } ) )
9	8	eqcomd	⊢ ( 𝜑 → ( 𝐹 “ { 𝐶 } ) = { ( 𝐹 ‘ 𝐶 ) } )
10	6 9	uneq12d	⊢ ( 𝜑 → ( ( 𝐹 “ { 𝐴 , 𝐵 } ) ∪ ( 𝐹 “ { 𝐶 } ) ) = ( { ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) } ∪ { ( 𝐹 ‘ 𝐶 ) } ) )
11		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
12	11	imaeq2i	⊢ ( 𝐹 “ { 𝐴 , 𝐵 , 𝐶 } ) = ( 𝐹 “ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) )
13		imaundi	⊢ ( 𝐹 “ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) ) = ( ( 𝐹 “ { 𝐴 , 𝐵 } ) ∪ ( 𝐹 “ { 𝐶 } ) )
14	12 13	eqtri	⊢ ( 𝐹 “ { 𝐴 , 𝐵 , 𝐶 } ) = ( ( 𝐹 “ { 𝐴 , 𝐵 } ) ∪ ( 𝐹 “ { 𝐶 } ) )
15		df-tp	⊢ { ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐶 ) } = ( { ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) } ∪ { ( 𝐹 ‘ 𝐶 ) } )
16	10 14 15	3eqtr4g	⊢ ( 𝜑 → ( 𝐹 “ { 𝐴 , 𝐵 , 𝐶 } ) = { ( 𝐹 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐶 ) } )