Step |
Hyp |
Ref |
Expression |
1 |
|
inpreima |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) ) |
2 |
|
funforn |
⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 –onto→ ran 𝐹 ) |
3 |
|
fof |
⊢ ( 𝐹 : dom 𝐹 –onto→ ran 𝐹 → 𝐹 : dom 𝐹 ⟶ ran 𝐹 ) |
4 |
2 3
|
sylbi |
⊢ ( Fun 𝐹 → 𝐹 : dom 𝐹 ⟶ ran 𝐹 ) |
5 |
|
fimacnv |
⊢ ( 𝐹 : dom 𝐹 ⟶ ran 𝐹 → ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹 ) |
6 |
4 5
|
syl |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹 ) |
7 |
6
|
ineq2d |
⊢ ( Fun 𝐹 → ( ( ◡ 𝐹 “ 𝐴 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∩ dom 𝐹 ) ) |
8 |
|
cnvresima |
⊢ ( ◡ ( 𝐹 ↾ dom 𝐹 ) “ 𝐴 ) = ( ( ◡ 𝐹 “ 𝐴 ) ∩ dom 𝐹 ) |
9 |
|
resdm2 |
⊢ ( 𝐹 ↾ dom 𝐹 ) = ◡ ◡ 𝐹 |
10 |
|
funrel |
⊢ ( Fun 𝐹 → Rel 𝐹 ) |
11 |
|
dfrel2 |
⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 ) |
12 |
10 11
|
sylib |
⊢ ( Fun 𝐹 → ◡ ◡ 𝐹 = 𝐹 ) |
13 |
9 12
|
eqtrid |
⊢ ( Fun 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 ) |
14 |
13
|
cnveqd |
⊢ ( Fun 𝐹 → ◡ ( 𝐹 ↾ dom 𝐹 ) = ◡ 𝐹 ) |
15 |
14
|
imaeq1d |
⊢ ( Fun 𝐹 → ( ◡ ( 𝐹 ↾ dom 𝐹 ) “ 𝐴 ) = ( ◡ 𝐹 “ 𝐴 ) ) |
16 |
8 15
|
eqtr3id |
⊢ ( Fun 𝐹 → ( ( ◡ 𝐹 “ 𝐴 ) ∩ dom 𝐹 ) = ( ◡ 𝐹 “ 𝐴 ) ) |
17 |
1 7 16
|
3eqtrrd |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ 𝐴 ) = ( ◡ 𝐹 “ ( 𝐴 ∩ ran 𝐹 ) ) ) |