# Metamath Proof Explorer

## Theorem exidcl

Description: Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypothesis exidcl.1 𝑋 = ran 𝐺
Assertion exidcl ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )

### Proof

Step Hyp Ref Expression
1 exidcl.1 𝑋 = ran 𝐺
2 rngopidOLD ( 𝐺 ∈ ( Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺 )
3 1 2 syl5eq ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝑋 = dom dom 𝐺 )
4 3 eleq2d ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐴𝑋𝐴 ∈ dom dom 𝐺 ) )
5 3 eleq2d ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐵𝑋𝐵 ∈ dom dom 𝐺 ) )
6 4 5 anbi12d ( 𝐺 ∈ ( Magma ∩ ExId ) → ( ( 𝐴𝑋𝐵𝑋 ) ↔ ( 𝐴 ∈ dom dom 𝐺𝐵 ∈ dom dom 𝐺 ) ) )
7 6 pm5.32i ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) ↔ ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ ( 𝐴 ∈ dom dom 𝐺𝐵 ∈ dom dom 𝐺 ) ) )
8 inss1 ( Magma ∩ ExId ) ⊆ Magma
9 8 sseli ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐺 ∈ Magma )
10 eqid dom dom 𝐺 = dom dom 𝐺
11 10 clmgmOLD ( ( 𝐺 ∈ Magma ∧ 𝐴 ∈ dom dom 𝐺𝐵 ∈ dom dom 𝐺 ) → ( 𝐴 𝐺 𝐵 ) ∈ dom dom 𝐺 )
12 9 11 syl3an1 ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝐴 ∈ dom dom 𝐺𝐵 ∈ dom dom 𝐺 ) → ( 𝐴 𝐺 𝐵 ) ∈ dom dom 𝐺 )
13 12 3expb ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ ( 𝐴 ∈ dom dom 𝐺𝐵 ∈ dom dom 𝐺 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ dom dom 𝐺 )
14 7 13 sylbi ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ dom dom 𝐺 )
15 14 3impb ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ dom dom 𝐺 )
16 3 3ad2ant1 ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝐴𝑋𝐵𝑋 ) → 𝑋 = dom dom 𝐺 )
17 15 16 eleqtrrd ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )