Metamath Proof Explorer

Theorem exidres

Description: Obsolete theorem, use idressidex instead. 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) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses exidres.1 ⊢ X = ran ⁡ G
exidres.2 ⊢ U = GId ⁡ G
exidres.3 ⊢ H = G ↾ Y × Y
Assertion exidres ⊢ G ∈ Magma ∩ ExId ∧ Y ⊆ X ∧ U ∈ Y → H ∈ ExId

Proof

Step Hyp Ref Expression
1 exidres.1 ⊢ X = ran ⁡ G
2 exidres.2 ⊢ U = GId ⁡ G
3 exidres.3 ⊢ H = G ↾ Y × Y
4 1 2 3 exidreslem ⊢ G ∈ Magma ∩ ExId ∧ Y ⊆ X ∧ U ∈ Y → U ∈ dom ⁡ dom ⁡ H ∧ ∀ x ∈ dom ⁡ dom ⁡ H U H x = x ∧ x H U = x
5 oveq1 ⊢ u = U → u H x = U H x
6 5 eqeq1d ⊢ u = U → u H x = x ↔ U H x = x
7 6 ovanraleqv ⊢ u = U → ∀ x ∈ dom ⁡ dom ⁡ H u H x = x ∧ x H u = x ↔ ∀ x ∈ dom ⁡ dom ⁡ H U H x = x ∧ x H U = x
8 7 rspcev ⊢ U ∈ dom ⁡ dom ⁡ H ∧ ∀ x ∈ dom ⁡ dom ⁡ H U H x = x ∧ x H U = x → ∃ u ∈ dom ⁡ dom ⁡ H ∀ x ∈ dom ⁡ dom ⁡ H u H x = x ∧ x H u = x
9 4 8 syl ⊢ G ∈ Magma ∩ ExId ∧ Y ⊆ X ∧ U ∈ Y → ∃ u ∈ dom ⁡ dom ⁡ H ∀ x ∈ dom ⁡ dom ⁡ H u H x = x ∧ x H u = x
10 resexg ⊢ G ∈ Magma ∩ ExId → G ↾ Y × Y ∈ V
11 3 10 eqeltrid ⊢ G ∈ Magma ∩ ExId → H ∈ V
12 eqid ⊢ dom ⁡ dom ⁡ H = dom ⁡ dom ⁡ H
13 12 isexid ⊢ H ∈ V → H ∈ ExId ↔ ∃ u ∈ dom ⁡ dom ⁡ H ∀ x ∈ dom ⁡ dom ⁡ H u H x = x ∧ x H u = x
14 11 13 syl ⊢ G ∈ Magma ∩ ExId → H ∈ ExId ↔ ∃ u ∈ dom ⁡ dom ⁡ H ∀ x ∈ dom ⁡ dom ⁡ H u H x = x ∧ x H u = x
15 14 3ad2ant1 ⊢ G ∈ Magma ∩ ExId ∧ Y ⊆ X ∧ U ∈ Y → H ∈ ExId ↔ ∃ u ∈ dom ⁡ dom ⁡ H ∀ x ∈ dom ⁡ dom ⁡ H u H x = x ∧ x H u = x
16 9 15 mpbird ⊢ G ∈ Magma ∩ ExId ∧ Y ⊆ X ∧ U ∈ Y → H ∈ ExId