Theorem exidres

Description: The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypotheses	exidres.1	⊢ 𝑋 = ran 𝐺
	exidres.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
	exidres.3	⊢ 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) )
Assertion	exidres	⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → 𝐻 ∈ ExId )

Proof

Step	Hyp	Ref	Expression
1		exidres.1	⊢ 𝑋 = ran 𝐺
2		exidres.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
3		exidres.3	⊢ 𝐻 = ( 𝐺 ↾ ( 𝑌 × 𝑌 ) )
4	1 2 3	exidreslem	⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )
5		oveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐻 𝑥 ) = ( 𝑈 𝐻 𝑥 ) )
6	5	eqeq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐻 𝑥 ) = 𝑥 ) )
7	6	ovanraleqv	⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) )
8	7	rspcev	⊢ ( ( 𝑈 ∈ dom dom 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑈 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑈 ) = 𝑥 ) ) → ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
9	4 8	syl	⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) )
10		resexg	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐺 ↾ ( 𝑌 × 𝑌 ) ) ∈ V )
11	3 10	eqeltrid	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → 𝐻 ∈ V )
12		eqid	⊢ dom dom 𝐻 = dom dom 𝐻
13	12	isexid	⊢ ( 𝐻 ∈ V → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
14	11 13	syl	⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
15	14	3ad2ant1	⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → ( 𝐻 ∈ ExId ↔ ∃ 𝑢 ∈ dom dom 𝐻 ∀ 𝑥 ∈ dom dom 𝐻 ( ( 𝑢 𝐻 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐻 𝑢 ) = 𝑥 ) ) )
16	9 15	mpbird	⊢ ( ( 𝐺 ∈ ( Magma ∩ ExId ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑈 ∈ 𝑌 ) → 𝐻 ∈ ExId )