Theorem funtp

Description: A function with a domain of three elements. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	funtp.1	$$⊢A\in \mathrm{V}$$
	funtp.2	$$⊢B\in \mathrm{V}$$
	funtp.3	$$⊢C\in \mathrm{V}$$
	funtp.4	$$⊢D\in \mathrm{V}$$
	funtp.5	$$⊢E\in \mathrm{V}$$
	funtp.6	$$⊢F\in \mathrm{V}$$
Assertion	funtp	$$⊢\left(A\ne B\wedge A\ne C\wedge B\ne C\right)\to \mathrm{Fun}\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funtp.1	$$⊢A\in \mathrm{V}$$
2		funtp.2	$$⊢B\in \mathrm{V}$$
3		funtp.3	$$⊢C\in \mathrm{V}$$
4		funtp.4	$$⊢D\in \mathrm{V}$$
5		funtp.5	$$⊢E\in \mathrm{V}$$
6		funtp.6	$$⊢F\in \mathrm{V}$$
7	1 2 4 5	funpr	$$⊢A\ne B\to \mathrm{Fun}\left\{⟨A,D⟩,⟨B,E⟩\right\}$$
8	3 6	funsn	$$⊢\mathrm{Fun}\left\{⟨C,F⟩\right\}$$
9	7 8	jctir	$$⊢A\ne B\to \left(\mathrm{Fun}\left\{⟨A,D⟩,⟨B,E⟩\right\}\wedge \mathrm{Fun}\left\{⟨C,F⟩\right\}\right)$$
10	4 5	dmprop	$$⊢\mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩\right\}=\left\{A,B\right\}$$
11		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
12	10 11	eqtri	$$⊢\mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩\right\}=\left\{A\right\}\cup \left\{B\right\}$$
13	6	dmsnop	$$⊢\mathrm{dom}\left\{⟨C,F⟩\right\}=\left\{C\right\}$$
14	12 13	ineq12i	$$⊢\mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩\right\}\cap \mathrm{dom}\left\{⟨C,F⟩\right\}=\left(\left\{A\right\}\cup \left\{B\right\}\right)\cap \left\{C\right\}$$
15		disjsn2	$$⊢A\ne C\to \left\{A\right\}\cap \left\{C\right\}=\varnothing$$
16		disjsn2	$$⊢B\ne C\to \left\{B\right\}\cap \left\{C\right\}=\varnothing$$
17	15 16	anim12i	$$⊢\left(A\ne C\wedge B\ne C\right)\to \left(\left\{A\right\}\cap \left\{C\right\}=\varnothing \wedge \left\{B\right\}\cap \left\{C\right\}=\varnothing \right)$$
18		undisj1	$$⊢\left(\left\{A\right\}\cap \left\{C\right\}=\varnothing \wedge \left\{B\right\}\cap \left\{C\right\}=\varnothing \right)\leftrightarrow \left(\left\{A\right\}\cup \left\{B\right\}\right)\cap \left\{C\right\}=\varnothing$$
19	17 18	sylib	$$⊢\left(A\ne C\wedge B\ne C\right)\to \left(\left\{A\right\}\cup \left\{B\right\}\right)\cap \left\{C\right\}=\varnothing$$
20	14 19	syl5eq	$$⊢\left(A\ne C\wedge B\ne C\right)\to \mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩\right\}\cap \mathrm{dom}\left\{⟨C,F⟩\right\}=\varnothing$$
21		funun	$$⊢\left(\left(\mathrm{Fun}\left\{⟨A,D⟩,⟨B,E⟩\right\}\wedge \mathrm{Fun}\left\{⟨C,F⟩\right\}\right)\wedge \mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩\right\}\cap \mathrm{dom}\left\{⟨C,F⟩\right\}=\varnothing \right)\to \mathrm{Fun}\left(\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}\right)$$
22	9 20 21	syl2an	$$⊢\left(A\ne B\wedge \left(A\ne C\wedge B\ne C\right)\right)\to \mathrm{Fun}\left(\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}\right)$$
23	22	3impb	$$⊢\left(A\ne B\wedge A\ne C\wedge B\ne C\right)\to \mathrm{Fun}\left(\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}\right)$$
24		df-tp	$$⊢\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}=\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}$$
25	24	funeqi	$$⊢\mathrm{Fun}\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\leftrightarrow \mathrm{Fun}\left(\left\{⟨A,D⟩,⟨B,E⟩\right\}\cup \left\{⟨C,F⟩\right\}\right)$$
26	23 25	sylibr	$$⊢\left(A\ne B\wedge A\ne C\wedge B\ne C\right)\to \mathrm{Fun}\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}$$