Theorem grpoinvf

Description: Mapping of the inverse function of a group. (Contributed by NM, 29-Mar-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpasscan1.1	⊢ 𝑋 = ran 𝐺
	grpasscan1.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion	grpoinvf	⊢ ( 𝐺 ∈ GrpOp → 𝑁 : 𝑋 –1-1-onto→ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		grpasscan1.1	⊢ 𝑋 = ran 𝐺
2		grpasscan1.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
3		riotaex	⊢ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ∈ V
4		eqid	⊢ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) )
5	3 4	fnmpti	⊢ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ) Fn 𝑋
6		eqid	⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
7	1 6 2	grpoinvfval	⊢ ( 𝐺 ∈ GrpOp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ) )
8	7	fneq1d	⊢ ( 𝐺 ∈ GrpOp → ( 𝑁 Fn 𝑋 ↔ ( 𝑥 ∈ 𝑋 ↦ ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = ( GId ‘ 𝐺 ) ) ) Fn 𝑋 ) )
9	5 8	mpbiri	⊢ ( 𝐺 ∈ GrpOp → 𝑁 Fn 𝑋 )
10		fnrnfv	⊢ ( 𝑁 Fn 𝑋 → ran 𝑁 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) } )
11	9 10	syl	⊢ ( 𝐺 ∈ GrpOp → ran 𝑁 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) } )
12	1 2	grpoinvcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑦 ) ∈ 𝑋 )
13	1 2	grpo2inv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) = 𝑦 )
14	13	eqcomd	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → 𝑦 = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) )
15		fveq2	⊢ ( 𝑥 = ( 𝑁 ‘ 𝑦 ) → ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) )
16	15	rspceeqv	⊢ ( ( ( 𝑁 ‘ 𝑦 ) ∈ 𝑋 ∧ 𝑦 = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) )
17	12 14 16	syl2anc	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) )
18	17	ex	⊢ ( 𝐺 ∈ GrpOp → ( 𝑦 ∈ 𝑋 → ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) ) )
19		simpr	⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 = ( 𝑁 ‘ 𝑥 ) ) → 𝑦 = ( 𝑁 ‘ 𝑥 ) )
20	1 2	grpoinvcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ 𝑥 ) ∈ 𝑋 )
21	20	adantr	⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 = ( 𝑁 ‘ 𝑥 ) ) → ( 𝑁 ‘ 𝑥 ) ∈ 𝑋 )
22	19 21	eqeltrd	⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 = ( 𝑁 ‘ 𝑥 ) ) → 𝑦 ∈ 𝑋 )
23	22	rexlimdva2	⊢ ( 𝐺 ∈ GrpOp → ( ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) → 𝑦 ∈ 𝑋 ) )
24	18 23	impbid	⊢ ( 𝐺 ∈ GrpOp → ( 𝑦 ∈ 𝑋 ↔ ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) ) )
25	24	eqabdv	⊢ ( 𝐺 ∈ GrpOp → 𝑋 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑋 𝑦 = ( 𝑁 ‘ 𝑥 ) } )
26	11 25	eqtr4d	⊢ ( 𝐺 ∈ GrpOp → ran 𝑁 = 𝑋 )
27		fveq2	⊢ ( ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑦 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) )
28	1 2	grpo2inv	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑥 ) ) = 𝑥 )
29	28 13	eqeqan12d	⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
30	29	anandis	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ ( 𝑁 ‘ 𝑥 ) ) = ( 𝑁 ‘ ( 𝑁 ‘ 𝑦 ) ) ↔ 𝑥 = 𝑦 ) )
31	27 30	imbitrid	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
32	31	ralrimivva	⊢ ( 𝐺 ∈ GrpOp → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
33		dff1o6	⊢ ( 𝑁 : 𝑋 –1-1-onto→ 𝑋 ↔ ( 𝑁 Fn 𝑋 ∧ ran 𝑁 = 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) = ( 𝑁 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
34	9 26 32 33	syl3anbrc	⊢ ( 𝐺 ∈ GrpOp → 𝑁 : 𝑋 –1-1-onto→ 𝑋 )