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 ⊢ G : X × X ⟶ X ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ran ⁡ G = X

Proof

Step Hyp Ref Expression
1 r19.12 ⊢ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X ∃ u ∈ X u G x = x ∧ x G u = x
2 simpl ⊢ u G x = x ∧ x G u = x → u G x = x
3 2 eqcomd ⊢ u G x = x ∧ x G u = x → x = u G x
4 oveq2 ⊢ y = x → u G y = u G x
5 4 rspceeqv ⊢ x ∈ X ∧ x = u G x → ∃ y ∈ X x = u G y
6 5 ex ⊢ x ∈ X → x = u G x → ∃ y ∈ X x = u G y
7 3 6 syl5 ⊢ x ∈ X → u G x = x ∧ x G u = x → ∃ y ∈ X x = u G y
8 7 reximdv ⊢ x ∈ X → ∃ u ∈ X u G x = x ∧ x G u = x → ∃ u ∈ X ∃ y ∈ X x = u G y
9 8 ralimia ⊢ ∀ x ∈ X ∃ u ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X ∃ u ∈ X ∃ y ∈ X x = u G y
10 1 9 syl ⊢ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X ∃ u ∈ X ∃ y ∈ X x = u G y
11 10 anim2i ⊢ G : X × X ⟶ X ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → G : X × X ⟶ X ∧ ∀ x ∈ X ∃ u ∈ X ∃ y ∈ X x = u G y
12 foov ⊢ G : X × X ⟶ onto X ↔ G : X × X ⟶ X ∧ ∀ x ∈ X ∃ u ∈ X ∃ y ∈ X x = u G y
13 11 12 sylibr ⊢ G : X × X ⟶ X ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → G : X × X ⟶ onto X
14 forn ⊢ G : X × X ⟶ onto X → ran ⁡ G = X
15 13 14 syl ⊢ G : X × X ⟶ X ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ran ⁡ G = X