This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) → ran 𝐺 = 𝑋 )

Proof

Step Hyp Ref Expression
1 r19.12 ⊢ ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
2 simpl ⊢ ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
3 2 eqcomd ⊢ ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → 𝑥 = ( 𝑢 𝐺 𝑥 ) )
4 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑢 𝐺 𝑦 ) = ( 𝑢 𝐺 𝑥 ) )
5 4 rspceeqv ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 = ( 𝑢 𝐺 𝑥 ) ) → ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑢 𝐺 𝑦 ) )
6 5 ex ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑥 = ( 𝑢 𝐺 𝑥 ) → ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑢 𝐺 𝑦 ) ) )
7 3 6 syl5 ⊢ ( 𝑥 ∈ 𝑋 → ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑢 𝐺 𝑦 ) ) )
8 7 reximdv ⊢ ( 𝑥 ∈ 𝑋 → ( ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∃ 𝑢 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑢 𝐺 𝑦 ) ) )
9 8 ralimia ⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑢 𝐺 𝑦 ) )
10 1 9 syl ⊢ ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑢 𝐺 𝑦 ) )
11 10 anim2i ⊢ ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) → ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑢 𝐺 𝑦 ) ) )
12 foov ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑢 𝐺 𝑦 ) ) )
13 11 12 sylibr ⊢ ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )
14 forn ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 → ran 𝐺 = 𝑋 )
15 13 14 syl ⊢ ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) → ran 𝐺 = 𝑋 )