Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
2 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
3 |
1 2
|
isgim |
⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ) ) |
4 |
1 2
|
ghmf1o |
⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ↔ ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ) ) |
5 |
4
|
pm5.32i |
⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ) ) |
6 |
3 5
|
bitri |
⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 GrpHom 𝑅 ) ) ) |