Step |
Hyp |
Ref |
Expression |
1 |
|
rnghmf1o.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
rnghmf1o.c |
⊢ 𝐶 = ( Base ‘ 𝑆 ) |
3 |
|
isrngisom |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) ) ) |
4 |
1 2
|
rnghmf1o |
⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( 𝐹 : 𝐵 –1-1-onto→ 𝐶 ↔ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) ) |
5 |
4
|
bicomd |
⊢ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) |
6 |
5
|
a1i |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) → ( ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ↔ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) ) |
7 |
6
|
pm5.32d |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ ◡ 𝐹 ∈ ( 𝑆 RngHomo 𝑅 ) ) ↔ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) ) |
8 |
3 7
|
bitrd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝑅 RngIsom 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RngHomo 𝑆 ) ∧ 𝐹 : 𝐵 –1-1-onto→ 𝐶 ) ) ) |