Metamath Proof Explorer

Theorem grpokerinj

Description: A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses grpkerinj.1 ⊢ 𝑋 = ran 𝐺
grpkerinj.2 ⊢ 𝑊 = ( GId ‘ 𝐺 )
grpkerinj.3 ⊢ 𝑌 = ran 𝐻
grpkerinj.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion grpokerinj ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 : 𝑋 –1-1→ 𝑌 ↔ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) )

Proof

Step Hyp Ref Expression
1 grpkerinj.1 ⊢ 𝑋 = ran 𝐺
2 grpkerinj.2 ⊢ 𝑊 = ( GId ‘ 𝐺 )
3 grpkerinj.3 ⊢ 𝑌 = ran 𝐻
4 grpkerinj.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
5 2 4 ghomidOLD ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 ‘ 𝑊 ) = 𝑈 )
6 5 sneqd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → { ( 𝐹 ‘ 𝑊 ) } = { 𝑈 } )
7 1 3 ghomf ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
8 7 ffnd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝐹 Fn 𝑋 )
9 1 2 grpoidcl ⊢ ( 𝐺 ∈ GrpOp → 𝑊 ∈ 𝑋 )
10 9 3ad2ant1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → 𝑊 ∈ 𝑋 )
11 fnsnfv ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑊 ∈ 𝑋 ) → { ( 𝐹 ‘ 𝑊 ) } = ( 𝐹 “ { 𝑊 } ) )
12 8 10 11 syl2anc ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → { ( 𝐹 ‘ 𝑊 ) } = ( 𝐹 “ { 𝑊 } ) )
13 6 12 eqtr3d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → { 𝑈 } = ( 𝐹 “ { 𝑊 } ) )
14 13 imaeq2d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( ◡ 𝐹 “ { 𝑈 } ) = ( ◡ 𝐹 “ ( 𝐹 “ { 𝑊 } ) ) )
15 14 adantl ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ) → ( ◡ 𝐹 “ { 𝑈 } ) = ( ◡ 𝐹 “ ( 𝐹 “ { 𝑊 } ) ) )
16 9 snssd ⊢ ( 𝐺 ∈ GrpOp → { 𝑊 } ⊆ 𝑋 )
17 16 3ad2ant1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → { 𝑊 } ⊆ 𝑋 )
18 f1imacnv ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ { 𝑊 } ⊆ 𝑋 ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑊 } ) ) = { 𝑊 } )
19 17 18 sylan2 ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑊 } ) ) = { 𝑊 } )
20 15 19 eqtrd ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ) → ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } )
21 20 expcom ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 : 𝑋 –1-1→ 𝑌 → ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) )
22 7 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) → 𝐹 : 𝑋 ⟶ 𝑌 )
23 simpl2 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐻 ∈ GrpOp )
24 7 ffvelcdmda ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 )
25 24 adantrr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 )
26 7 ffvelcdmda ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 )
27 26 adantrl ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 )
28 eqid ⊢ ( /𝑔 ‘ 𝐻 ) = ( /𝑔 ‘ 𝐻 )
29 3 4 28 grpoeqdivid ⊢ ( ( 𝐻 ∈ GrpOp ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ( /𝑔 ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) = 𝑈 ) )
30 23 25 27 29 syl3anc ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ( /𝑔 ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) = 𝑈 ) )
31 30 adantlr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ( /𝑔 ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) = 𝑈 ) )
32 eqid ⊢ ( /𝑔 ‘ 𝐺 ) = ( /𝑔 ‘ 𝐺 )
33 1 32 28 ghomdiv ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( /𝑔 ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
34 33 adantlr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( /𝑔 ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
35 34 eqeq1d ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) = 𝑈 ↔ ( ( 𝐹 ‘ 𝑥 ) ( /𝑔 ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) = 𝑈 ) )
36 4 fvexi ⊢ 𝑈 ∈ V
37 36 snid ⊢ 𝑈 ∈ { 𝑈 }
38 eleq1 ⊢ ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) = 𝑈 → ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) ∈ { 𝑈 } ↔ 𝑈 ∈ { 𝑈 } ) )
39 37 38 mpbiri ⊢ ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) = 𝑈 → ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) ∈ { 𝑈 } )
40 7 ffund ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → Fun 𝐹 )
41 40 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → Fun 𝐹 )
42 1 32 grpodivcl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
43 42 3expb ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
44 43 3ad2antl1 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
45 7 fdmd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → dom 𝐹 = 𝑋 )
46 45 adantr ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → dom 𝐹 = 𝑋 )
47 44 46 eleqtrrd ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ dom 𝐹 )
48 fvimacnv ⊢ ( ( Fun 𝐹 ∧ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ dom 𝐹 ) → ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) ∈ { 𝑈 } ↔ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑈 } ) ) )
49 41 47 48 syl2anc ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) ∈ { 𝑈 } ↔ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑈 } ) ) )
50 eleq2 ⊢ ( ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } → ( ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑈 } ) ↔ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ { 𝑊 } ) )
51 49 50 sylan9bb ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) → ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) ∈ { 𝑈 } ↔ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ { 𝑊 } ) )
52 51 an32s ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) ∈ { 𝑈 } ↔ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ { 𝑊 } ) )
53 elsni ⊢ ( ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ { 𝑊 } → ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) = 𝑊 )
54 1 2 32 grpoeqdivid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 = 𝑦 ↔ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) = 𝑊 ) )
55 54 biimprd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) = 𝑊 → 𝑥 = 𝑦 ) )
56 55 3expb ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) = 𝑊 → 𝑥 = 𝑦 ) )
57 56 3ad2antl1 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) = 𝑊 → 𝑥 = 𝑦 ) )
58 53 57 syl5 ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ { 𝑊 } → 𝑥 = 𝑦 ) )
59 58 adantlr ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ∈ { 𝑊 } → 𝑥 = 𝑦 ) )
60 52 59 sylbid ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) ∈ { 𝑈 } → 𝑥 = 𝑦 ) )
61 39 60 syl5 ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑥 ( /𝑔 ‘ 𝐺 ) 𝑦 ) ) = 𝑈 → 𝑥 = 𝑦 ) )
62 35 61 sylbird ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( /𝑔 ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) = 𝑈 → 𝑥 = 𝑦 ) )
63 31 62 sylbid ⊢ ( ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
64 63 ralrimivva ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
65 dff13 ⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
66 22 64 65 sylanbrc ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) ∧ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
67 66 ex ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } → 𝐹 : 𝑋 –1-1→ 𝑌 ) )
68 21 67 impbid ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐻 ) ) → ( 𝐹 : 𝑋 –1-1→ 𝑌 ↔ ( ◡ 𝐹 “ { 𝑈 } ) = { 𝑊 } ) )