Theorem imasaddflem

Description: The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	imasaddf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
	imasaddf.e	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
	imasaddflem.a	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
	imasaddflem.c	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to p\underset{\dot{}}{·}q\in V$$
Assertion	imasaddflem	$$⊢\phi \to \underset{\dot{}}{\bullet }:B\times B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		imasaddf.f	$$⊢\phi \to F:V\underset{onto}{⟶}B$$
2		imasaddf.e	$$⊢\left(\phi \wedge \left(a\in V\wedge b\in V\right)\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(\left(F\left(a\right)=F\left(p\right)\wedge F\left(b\right)=F\left(q\right)\right)\to F\left(a\underset{\dot{}}{·}b\right)=F\left(p\underset{\dot{}}{·}q\right)\right)$$
3		imasaddflem.a	$$⊢\phi \to \underset{\dot{}}{\bullet }=\bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}$$
4		imasaddflem.c	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to p\underset{\dot{}}{·}q\in V$$
5	1 2 3	imasaddfnlem	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(B\times B\right)$$
6		fof	$$⊢F:V\underset{onto}{⟶}B\to F:V⟶B$$
7	1 6	syl	$$⊢\phi \to F:V⟶B$$
8		ffvelrn	$$⊢\left(F:V⟶B\wedge p\in V\right)\to F\left(p\right)\in B$$
9		ffvelrn	$$⊢\left(F:V⟶B\wedge q\in V\right)\to F\left(q\right)\in B$$
10	8 9	anim12dan	$$⊢\left(F:V⟶B\wedge \left(p\in V\wedge q\in V\right)\right)\to \left(F\left(p\right)\in B\wedge F\left(q\right)\in B\right)$$
11		opelxpi	$$⊢\left(F\left(p\right)\in B\wedge F\left(q\right)\in B\right)\to ⟨F\left(p\right),F\left(q\right)⟩\in \left(B\times B\right)$$
12	10 11	syl	$$⊢\left(F:V⟶B\wedge \left(p\in V\wedge q\in V\right)\right)\to ⟨F\left(p\right),F\left(q\right)⟩\in \left(B\times B\right)$$
13	7 12	sylan	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to ⟨F\left(p\right),F\left(q\right)⟩\in \left(B\times B\right)$$
14		ffvelrn	$$⊢\left(F:V⟶B\wedge p\underset{\dot{}}{·}q\in V\right)\to F\left(p\underset{\dot{}}{·}q\right)\in B$$
15	7 4 14	syl2an2r	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to F\left(p\underset{\dot{}}{·}q\right)\in B$$
16	13 15	opelxpd	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to ⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\in \left(\left(B\times B\right)\times B\right)$$
17	16	snssd	$$⊢\left(\phi \wedge \left(p\in V\wedge q\in V\right)\right)\to \left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}\subseteq \left(B\times B\right)\times B$$
18	17	anassrs	$$⊢\left(\left(\phi \wedge p\in V\right)\wedge q\in V\right)\to \left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}\subseteq \left(B\times B\right)\times B$$
19	18	iunssd	$$⊢\left(\phi \wedge p\in V\right)\to \bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}\subseteq \left(B\times B\right)\times B$$
20	19	iunssd	$$⊢\phi \to \bigcup _{p\in V}\bigcup _{q\in V}\left\{⟨⟨F\left(p\right),F\left(q\right)⟩,F\left(p\underset{\dot{}}{·}q\right)⟩\right\}\subseteq \left(B\times B\right)\times B$$
21	3 20	eqsstrd	$$⊢\phi \to \underset{\dot{}}{\bullet }\subseteq \left(B\times B\right)\times B$$
22		dff2	$$⊢\underset{\dot{}}{\bullet }:B\times B⟶B\leftrightarrow \left(\underset{\dot{}}{\bullet }Fn\left(B\times B\right)\wedge \underset{\dot{}}{\bullet }\subseteq \left(B\times B\right)\times B\right)$$
23	5 21 22	sylanbrc	$$⊢\phi \to \underset{\dot{}}{\bullet }:B\times B⟶B$$