Theorem fnimatpd

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

	Ref	Expression
Hypotheses	fnimatpd.1	$$⊢\phi \to FFnD$$
	fnimatpd.2	$$⊢\phi \to A\in D$$
	fnimatpd.3	$$⊢\phi \to B\in D$$
	fnimatpd.4	$$⊢\phi \to C\in D$$
Assertion	fnimatpd	$$⊢\phi \to F\left[\left\{A,B,C\right\}\right]=\left\{F\left(A\right),F\left(B\right),F\left(C\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnimatpd.1	$$⊢\phi \to FFnD$$
2		fnimatpd.2	$$⊢\phi \to A\in D$$
3		fnimatpd.3	$$⊢\phi \to B\in D$$
4		fnimatpd.4	$$⊢\phi \to C\in D$$
5		fnimapr	$$⊢\left(FFnD\wedge A\in D\wedge B\in D\right)\to F\left[\left\{A,B\right\}\right]=\left\{F\left(A\right),F\left(B\right)\right\}$$
6	1 2 3 5	syl3anc	$$⊢\phi \to F\left[\left\{A,B\right\}\right]=\left\{F\left(A\right),F\left(B\right)\right\}$$
7		fnsnfv	$$⊢\left(FFnD\wedge C\in D\right)\to \left\{F\left(C\right)\right\}=F\left[\left\{C\right\}\right]$$
8	1 4 7	syl2anc	$$⊢\phi \to \left\{F\left(C\right)\right\}=F\left[\left\{C\right\}\right]$$
9	8	eqcomd	$$⊢\phi \to F\left[\left\{C\right\}\right]=\left\{F\left(C\right)\right\}$$
10	6 9	uneq12d	$$⊢\phi \to F\left[\left\{A,B\right\}\right]\cup F\left[\left\{C\right\}\right]=\left\{F\left(A\right),F\left(B\right)\right\}\cup \left\{F\left(C\right)\right\}$$
11		df-tp	$$⊢\left\{A,B,C\right\}=\left\{A,B\right\}\cup \left\{C\right\}$$
12	11	imaeq2i	$$⊢F\left[\left\{A,B,C\right\}\right]=F\left[\left\{A,B\right\}\cup \left\{C\right\}\right]$$
13		imaundi	$$⊢F\left[\left\{A,B\right\}\cup \left\{C\right\}\right]=F\left[\left\{A,B\right\}\right]\cup F\left[\left\{C\right\}\right]$$
14	12 13	eqtri	$$⊢F\left[\left\{A,B,C\right\}\right]=F\left[\left\{A,B\right\}\right]\cup F\left[\left\{C\right\}\right]$$
15		df-tp	$$⊢\left\{F\left(A\right),F\left(B\right),F\left(C\right)\right\}=\left\{F\left(A\right),F\left(B\right)\right\}\cup \left\{F\left(C\right)\right\}$$
16	10 14 15	3eqtr4g	$$⊢\phi \to F\left[\left\{A,B,C\right\}\right]=\left\{F\left(A\right),F\left(B\right),F\left(C\right)\right\}$$