# Metamath Proof Explorer

## 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}×{X}⟶{X}\wedge \exists {u}\in {X}\phantom{\rule{.4em}{0ex}}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left({u}{G}{x}={x}\wedge {x}{G}{u}={x}\right)\right)\to \mathrm{ran}{G}={X}$

### Proof

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