Theorem rngmgmbs4

Description: The range of an internal operation with a left and right identity element equals its base set. (Contributed by FL, 24-Jan-2010) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	rngmgmbs4	$$⊢\left(G:X\times X⟶X\wedge \exists u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)\right)\to \mathrm{ran}G=X$$

Proof

Step	Hyp	Ref	Expression
1		r19.12	$$⊢\exists u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)\to \forall x\in X\exists u\in X\left(uGx=x\wedge xGu=x\right)$$
2		simpl	$$⊢\left(uGx=x\wedge xGu=x\right)\to uGx=x$$
3	2	eqcomd	$$⊢\left(uGx=x\wedge xGu=x\right)\to x=uGx$$
4		oveq2	$$⊢y=x\to uGy=uGx$$
5	4	rspceeqv	$$⊢\left(x\in X\wedge x=uGx\right)\to \exists y\in Xx=uGy$$
6	5	ex	$$⊢x\in X\to \left(x=uGx\to \exists y\in Xx=uGy\right)$$
7	3 6	syl5	$$⊢x\in X\to \left(\left(uGx=x\wedge xGu=x\right)\to \exists y\in Xx=uGy\right)$$
8	7	reximdv	$$⊢x\in X\to \left(\exists u\in X\left(uGx=x\wedge xGu=x\right)\to \exists u\in X\exists y\in Xx=uGy\right)$$
9	8	ralimia	$$⊢\forall x\in X\exists u\in X\left(uGx=x\wedge xGu=x\right)\to \forall x\in X\exists u\in X\exists y\in Xx=uGy$$
10	1 9	syl	$$⊢\exists u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)\to \forall x\in X\exists u\in X\exists y\in Xx=uGy$$
11	10	anim2i	$$⊢\left(G:X\times X⟶X\wedge \exists u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)\right)\to \left(G:X\times X⟶X\wedge \forall x\in X\exists u\in X\exists y\in Xx=uGy\right)$$
12		foov	$$⊢G:X\times X\underset{onto}{⟶}X\leftrightarrow \left(G:X\times X⟶X\wedge \forall x\in X\exists u\in X\exists y\in Xx=uGy\right)$$
13	11 12	sylibr	$$⊢\left(G:X\times X⟶X\wedge \exists u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)\right)\to G:X\times X\underset{onto}{⟶}X$$
14		forn	$$⊢G:X\times X\underset{onto}{⟶}X\to \mathrm{ran}G=X$$
15	13 14	syl	$$⊢\left(G:X\times X⟶X\wedge \exists u\in X\forall x\in X\left(uGx=x\wedge xGu=x\right)\right)\to \mathrm{ran}G=X$$