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 = ran G
Assertion exidcl 
|- ( ( G e. ( Magma i^i ExId ) /\ A e. X /\ B e. X ) -> ( A G B ) e. X )

Proof

Step Hyp Ref Expression
1 exidcl.1 
 |-  X = ran G
2 rngopidOLD 
 |-  ( G e. ( Magma i^i ExId ) -> ran G = dom dom G )
3 1 2 syl5eq 
 |-  ( G e. ( Magma i^i ExId ) -> X = dom dom G )
4 3 eleq2d 
 |-  ( G e. ( Magma i^i ExId ) -> ( A e. X <-> A e. dom dom G ) )
5 3 eleq2d 
 |-  ( G e. ( Magma i^i ExId ) -> ( B e. X <-> B e. dom dom G ) )
6 4 5 anbi12d 
 |-  ( G e. ( Magma i^i ExId ) -> ( ( A e. X /\ B e. X ) <-> ( A e. dom dom G /\ B e. dom dom G ) ) )
7 6 pm5.32i 
 |-  ( ( G e. ( Magma i^i ExId ) /\ ( A e. X /\ B e. X ) ) <-> ( G e. ( Magma i^i ExId ) /\ ( A e. dom dom G /\ B e. dom dom G ) ) )
8 inss1 
 |-  ( Magma i^i ExId ) C_ Magma
9 8 sseli 
 |-  ( G e. ( Magma i^i ExId ) -> G e. Magma )
10 eqid 
 |-  dom dom G = dom dom G
11 10 clmgmOLD 
 |-  ( ( G e. Magma /\ A e. dom dom G /\ B e. dom dom G ) -> ( A G B ) e. dom dom G )
12 9 11 syl3an1 
 |-  ( ( G e. ( Magma i^i ExId ) /\ A e. dom dom G /\ B e. dom dom G ) -> ( A G B ) e. dom dom G )
13 12 3expb 
 |-  ( ( G e. ( Magma i^i ExId ) /\ ( A e. dom dom G /\ B e. dom dom G ) ) -> ( A G B ) e. dom dom G )
14 7 13 sylbi 
 |-  ( ( G e. ( Magma i^i ExId ) /\ ( A e. X /\ B e. X ) ) -> ( A G B ) e. dom dom G )
15 14 3impb 
 |-  ( ( G e. ( Magma i^i ExId ) /\ A e. X /\ B e. X ) -> ( A G B ) e. dom dom G )
16 3 3ad2ant1 
 |-  ( ( G e. ( Magma i^i ExId ) /\ A e. X /\ B e. X ) -> X = dom dom G )
17 15 16 eleqtrrd 
 |-  ( ( G e. ( Magma i^i ExId ) /\ A e. X /\ B e. X ) -> ( A G B ) e. X )