Metamath Proof Explorer

Theorem grporn

Description: The range of a group operation. Useful for satisfying group base set hypotheses of the form X = ran G . (Contributed by NM, 5-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses grprn.1 ${⊢}{G}\in \mathrm{GrpOp}$
grprn.2 ${⊢}\mathrm{dom}{G}={X}×{X}$
Assertion grporn ${⊢}{X}=\mathrm{ran}{G}$

Proof

Step Hyp Ref Expression
1 grprn.1 ${⊢}{G}\in \mathrm{GrpOp}$
2 grprn.2 ${⊢}\mathrm{dom}{G}={X}×{X}$
3 eqid ${⊢}\mathrm{ran}{G}=\mathrm{ran}{G}$
4 3 grpofo ${⊢}{G}\in \mathrm{GrpOp}\to {G}:\mathrm{ran}{G}×\mathrm{ran}{G}\underset{onto}{⟶}\mathrm{ran}{G}$
5 fofun ${⊢}{G}:\mathrm{ran}{G}×\mathrm{ran}{G}\underset{onto}{⟶}\mathrm{ran}{G}\to \mathrm{Fun}{G}$
6 1 4 5 mp2b ${⊢}\mathrm{Fun}{G}$
7 df-fn ${⊢}{G}Fn\left({X}×{X}\right)↔\left(\mathrm{Fun}{G}\wedge \mathrm{dom}{G}={X}×{X}\right)$
8 6 2 7 mpbir2an ${⊢}{G}Fn\left({X}×{X}\right)$
9 fofn ${⊢}{G}:\mathrm{ran}{G}×\mathrm{ran}{G}\underset{onto}{⟶}\mathrm{ran}{G}\to {G}Fn\left(\mathrm{ran}{G}×\mathrm{ran}{G}\right)$
10 1 4 9 mp2b ${⊢}{G}Fn\left(\mathrm{ran}{G}×\mathrm{ran}{G}\right)$
11 fndmu ${⊢}\left({G}Fn\left({X}×{X}\right)\wedge {G}Fn\left(\mathrm{ran}{G}×\mathrm{ran}{G}\right)\right)\to {X}×{X}=\mathrm{ran}{G}×\mathrm{ran}{G}$
12 xpid11 ${⊢}{X}×{X}=\mathrm{ran}{G}×\mathrm{ran}{G}↔{X}=\mathrm{ran}{G}$
13 11 12 sylib ${⊢}\left({G}Fn\left({X}×{X}\right)\wedge {G}Fn\left(\mathrm{ran}{G}×\mathrm{ran}{G}\right)\right)\to {X}=\mathrm{ran}{G}$
14 8 10 13 mp2an ${⊢}{X}=\mathrm{ran}{G}$