Metamath Proof Explorer
Description: An isomorphism of groups is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015) (Revised by Mario Carneiro, 6-May-2015)
|
|
Ref |
Expression |
|
Hypotheses |
isgim.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
|
|
isgim.c |
⊢ 𝐶 = ( Base ‘ 𝑆 ) |
|
Assertion |
gimf1o |
⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
isgim.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
isgim.c |
⊢ 𝐶 = ( Base ‘ 𝑆 ) |
3 |
1 2
|
isgim |
⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) |
4 |
3
|
simprbi |
⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) |