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	⊢ 𝑋 = ran 𝐺
	grpoidval.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
Assertion	grpoidval	⊢ ( 𝐺 ∈ GrpOp → 𝑈 = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		grpoidval.1	⊢ 𝑋 = ran 𝐺
2		grpoidval.2	⊢ 𝑈 = ( GId ‘ 𝐺 )
3	1	gidval	⊢ ( 𝐺 ∈ GrpOp → ( GId ‘ 𝐺 ) = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
4		simpl	⊢ ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
5	4	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
6	5	rgenw	⊢ ∀ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
7	6	a1i	⊢ ( 𝐺 ∈ GrpOp → ∀ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
8	1	grpoidinv	⊢ ( 𝐺 ∈ GrpOp → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) )
9		simpl	⊢ ( ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
10	9	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
11	10	reximi	⊢ ( ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
12	8 11	syl	⊢ ( 𝐺 ∈ GrpOp → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) )
13	1	grpoideu	⊢ ( 𝐺 ∈ GrpOp → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
14	7 12 13	3jca	⊢ ( 𝐺 ∈ GrpOp → ( ∀ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
15		reupick2	⊢ ( ( ( ∀ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∧ 𝑢 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
16	14 15	sylan	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
17	16	riotabidva	⊢ ( 𝐺 ∈ GrpOp → ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ) )
18	3 17	eqtr4d	⊢ ( 𝐺 ∈ GrpOp → ( GId ‘ 𝐺 ) = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
19	2 18	eqtrid	⊢ ( 𝐺 ∈ GrpOp → 𝑈 = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )