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 𝐺 = 𝑋 )