Step |
Hyp |
Ref |
Expression |
1 |
|
f1ocnv |
⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 → ◡ ( 𝐹 ↾ 𝑅 ) : 𝑃 –1-1-onto→ 𝑅 ) |
2 |
1
|
adantl |
⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ◡ ( 𝐹 ↾ 𝑅 ) : 𝑃 –1-1-onto→ 𝑅 ) |
3 |
|
funcnvres |
⊢ ( Fun ◡ 𝐹 → ◡ ( 𝐹 ↾ 𝑅 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝑅 ) ) ) |
4 |
|
df-ima |
⊢ ( 𝐹 “ 𝑅 ) = ran ( 𝐹 ↾ 𝑅 ) |
5 |
|
dff1o5 |
⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ↔ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1→ 𝑃 ∧ ran ( 𝐹 ↾ 𝑅 ) = 𝑃 ) ) |
6 |
5
|
simprbi |
⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 → ran ( 𝐹 ↾ 𝑅 ) = 𝑃 ) |
7 |
4 6
|
eqtrid |
⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 → ( 𝐹 “ 𝑅 ) = 𝑃 ) |
8 |
7
|
reseq2d |
⊢ ( ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 → ( ◡ 𝐹 ↾ ( 𝐹 “ 𝑅 ) ) = ( ◡ 𝐹 ↾ 𝑃 ) ) |
9 |
3 8
|
sylan9eq |
⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ◡ ( 𝐹 ↾ 𝑅 ) = ( ◡ 𝐹 ↾ 𝑃 ) ) |
10 |
9
|
f1oeq1d |
⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ( ◡ ( 𝐹 ↾ 𝑅 ) : 𝑃 –1-1-onto→ 𝑅 ↔ ( ◡ 𝐹 ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑅 ) ) |
11 |
2 10
|
mpbid |
⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝑅 ) : 𝑅 –1-1-onto→ 𝑃 ) → ( ◡ 𝐹 ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑅 ) |