Theorem imasaddfn

Description: The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 10-Jul-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)$$
	imasaddf.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
	imasaddf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
	imasaddf.r	$$⊢\phi \to R\in Z$$
	imasaddf.p	$$⊢\underset{\dot{}}{·}={+}_R$$
	imasaddf.a	$$⊢\underset{\dot{}}{\bullet }={+}_U$$
Assertion	imasaddfn	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(B\times B\right)$$

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		imasaddf.u	$$⊢\phi \to U=F{“}_{𝑠}R$$
4		imasaddf.v	$$⊢\phi \to V={\mathrm{Base}}_R$$
5		imasaddf.r	$$⊢\phi \to R\in Z$$
6		imasaddf.p	$$⊢\underset{\dot{}}{·}={+}_R$$
7		imasaddf.a	$$⊢\underset{\dot{}}{\bullet }={+}_U$$
8	3 4 1 5 6 7	imasplusg	$$⊢\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\}$$
9	1 2 8	imasaddfnlem	$$⊢\phi \to \underset{\dot{}}{\bullet }Fn\left(B\times B\right)$$