Metamath Proof Explorer

Theorem grpoidval

Description: Lemma for grpoidcl and others. (Contributed by NM, 5-Feb-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpoidval.1 ⊢ X = ran ⁡ G
grpoidval.2 ⊢ U = GId ⁡ G
Assertion grpoidval ⊢ G ∈ GrpOp → U = ι u ∈ X | ∀ x ∈ X u G x = x

Proof

Step Hyp Ref Expression
1 grpoidval.1 ⊢ X = ran ⁡ G
2 grpoidval.2 ⊢ U = GId ⁡ G
3 1 gidval ⊢ G ∈ GrpOp → GId ⁡ G = ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x
4 simpl ⊢ u G x = x ∧ x G u = x → u G x = x
5 4 ralimi ⊢ ∀ x ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X u G x = x
6 5 rgenw ⊢ ∀ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X u G x = x
7 6 a1i ⊢ G ∈ GrpOp → ∀ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X u G x = x
8 1 grpoidinv ⊢ G ∈ GrpOp → ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x ∧ ∃ y ∈ X y G x = u ∧ x G y = u
9 simpl ⊢ u G x = x ∧ x G u = x ∧ ∃ y ∈ X y G x = u ∧ x G y = u → u G x = x ∧ x G u = x
10 9 ralimi ⊢ ∀ x ∈ X u G x = x ∧ x G u = x ∧ ∃ y ∈ X y G x = u ∧ x G y = u → ∀ x ∈ X u G x = x ∧ x G u = x
11 10 reximi ⊢ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x ∧ ∃ y ∈ X y G x = u ∧ x G y = u → ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x
12 8 11 syl ⊢ G ∈ GrpOp → ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x
13 1 grpoideu ⊢ G ∈ GrpOp → ∃! u ∈ X ∀ x ∈ X u G x = x
14 7 12 13 3jca ⊢ G ∈ GrpOp → ∀ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X u G x = x ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x ∧ ∃! u ∈ X ∀ x ∈ X u G x = x
15 reupick2 ⊢ ∀ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x → ∀ x ∈ X u G x = x ∧ ∃ u ∈ X ∀ x ∈ X u G x = x ∧ x G u = x ∧ ∃! u ∈ X ∀ x ∈ X u G x = x ∧ u ∈ X → ∀ x ∈ X u G x = x ↔ ∀ x ∈ X u G x = x ∧ x G u = x
16 14 15 sylan ⊢ G ∈ GrpOp ∧ u ∈ X → ∀ x ∈ X u G x = x ↔ ∀ x ∈ X u G x = x ∧ x G u = x
17 16 riotabidva ⊢ G ∈ GrpOp → ι u ∈ X | ∀ x ∈ X u G x = x = ι u ∈ X | ∀ x ∈ X u G x = x ∧ x G u = x
18 3 17 eqtr4d ⊢ G ∈ GrpOp → GId ⁡ G = ι u ∈ X | ∀ x ∈ X u G x = x
19 2 18 syl5eq ⊢ G ∈ GrpOp → U = ι u ∈ X | ∀ x ∈ X u G x = x