# Metamath Proof Explorer

## Theorem isexid2

Description: If G e. ( Magma i^i ExId ) , then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis isexid2.1 𝑋 = ran 𝐺
Assertion isexid2 ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )

### Proof

Step Hyp Ref Expression
1 isexid2.1 𝑋 = ran 𝐺
2 rngopidOLD ( 𝐺 ∈ ( Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺 )
3 elin ( 𝐺 ∈ ( Magma ∩ ExId ) ↔ ( 𝐺 ∈ Magma ∧ 𝐺 ∈ ExId ) )
4 eqid dom dom 𝐺 = dom dom 𝐺
5 4 isexid ( 𝐺 ∈ ExId → ( 𝐺 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐺𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
6 5 ibi ( 𝐺 ∈ ExId → ∃ 𝑢 ∈ dom dom 𝐺𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
7 6 a1d ( 𝐺 ∈ ExId → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
8 7 adantl ( ( 𝐺 ∈ Magma ∧ 𝐺 ∈ ExId ) → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
9 3 8 sylbi ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
10 eqeq2 ( ran 𝐺 = dom dom 𝐺 → ( 𝑋 = ran 𝐺𝑋 = dom dom 𝐺 ) )
11 raleq ( ran 𝐺 = dom dom 𝐺 → ( ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
12 11 rexeqbi1dv ( ran 𝐺 = dom dom 𝐺 → ( ∃ 𝑢 ∈ ran 𝐺𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ dom dom 𝐺𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
13 10 12 imbi12d ( ran 𝐺 = dom dom 𝐺 → ( ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ↔ ( 𝑋 = dom dom 𝐺 → ∃ 𝑢 ∈ dom dom 𝐺𝑥 ∈ dom dom 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) )
14 9 13 syl5ibr ( ran 𝐺 = dom dom 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) ) )
15 2 14 mpcom ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝑋 = ran 𝐺 → ∃ 𝑢 ∈ ran 𝐺𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
16 15 com12 ( 𝑋 = ran 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢 ∈ ran 𝐺𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
17 raleq ( 𝑋 = ran 𝐺 → ( ∀ 𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
18 17 rexeqbi1dv ( 𝑋 = ran 𝐺 → ( ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ ran 𝐺𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
19 16 18 sylibrd ( 𝑋 = ran 𝐺 → ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
20 1 19 ax-mp ( 𝐺 ∈ ( Magma ∩ ExId ) → ∃ 𝑢𝑋𝑥𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )