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 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )