# 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 ${⊢}{X}=\mathrm{ran}{G}$
Assertion exidcl ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$

### Proof

Step Hyp Ref Expression
1 exidcl.1 ${⊢}{X}=\mathrm{ran}{G}$
2 rngopidOLD ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \mathrm{ran}{G}=\mathrm{dom}\mathrm{dom}{G}$
3 1 2 syl5eq ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to {X}=\mathrm{dom}\mathrm{dom}{G}$
4 3 eleq2d ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \left({A}\in {X}↔{A}\in \mathrm{dom}\mathrm{dom}{G}\right)$
5 3 eleq2d ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \left({B}\in {X}↔{B}\in \mathrm{dom}\mathrm{dom}{G}\right)$
6 4 5 anbi12d ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to \left(\left({A}\in {X}\wedge {B}\in {X}\right)↔\left({A}\in \mathrm{dom}\mathrm{dom}{G}\wedge {B}\in \mathrm{dom}\mathrm{dom}{G}\right)\right)$
7 6 pm5.32i ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)↔\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge \left({A}\in \mathrm{dom}\mathrm{dom}{G}\wedge {B}\in \mathrm{dom}\mathrm{dom}{G}\right)\right)$
8 inss1 ${⊢}\mathrm{Magma}\cap \mathrm{ExId}\subseteq \mathrm{Magma}$
9 8 sseli ${⊢}{G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\to {G}\in \mathrm{Magma}$
10 eqid ${⊢}\mathrm{dom}\mathrm{dom}{G}=\mathrm{dom}\mathrm{dom}{G}$
11 10 clmgmOLD ${⊢}\left({G}\in \mathrm{Magma}\wedge {A}\in \mathrm{dom}\mathrm{dom}{G}\wedge {B}\in \mathrm{dom}\mathrm{dom}{G}\right)\to {A}{G}{B}\in \mathrm{dom}\mathrm{dom}{G}$
12 9 11 syl3an1 ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {A}\in \mathrm{dom}\mathrm{dom}{G}\wedge {B}\in \mathrm{dom}\mathrm{dom}{G}\right)\to {A}{G}{B}\in \mathrm{dom}\mathrm{dom}{G}$
13 12 3expb ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge \left({A}\in \mathrm{dom}\mathrm{dom}{G}\wedge {B}\in \mathrm{dom}\mathrm{dom}{G}\right)\right)\to {A}{G}{B}\in \mathrm{dom}\mathrm{dom}{G}$
14 7 13 sylbi ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{G}{B}\in \mathrm{dom}\mathrm{dom}{G}$
15 14 3impb ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in \mathrm{dom}\mathrm{dom}{G}$
16 3 3ad2ant1 ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {X}=\mathrm{dom}\mathrm{dom}{G}$
17 15 16 eleqtrrd ${⊢}\left({G}\in \left(\mathrm{Magma}\cap \mathrm{ExId}\right)\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$