Step |
Hyp |
Ref |
Expression |
1 |
|
resima |
⊢ ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) “ ( ◡ 𝐹 “ 𝐶 ) ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝐶 ) ) |
2 |
|
fofun |
⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Fun 𝐹 ) |
3 |
2
|
adantr |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → Fun 𝐹 ) |
4 |
|
funcnvres2 |
⊢ ( Fun 𝐹 → ◡ ( ◡ 𝐹 ↾ 𝐶 ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) ) |
5 |
3 4
|
syl |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ◡ ( ◡ 𝐹 ↾ 𝐶 ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) ) |
6 |
5
|
imaeq1d |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) “ ( ◡ 𝐹 “ 𝐶 ) ) = ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) “ ( ◡ 𝐹 “ 𝐶 ) ) ) |
7 |
|
resss |
⊢ ( ◡ 𝐹 ↾ 𝐶 ) ⊆ ◡ 𝐹 |
8 |
|
cnvss |
⊢ ( ( ◡ 𝐹 ↾ 𝐶 ) ⊆ ◡ 𝐹 → ◡ ( ◡ 𝐹 ↾ 𝐶 ) ⊆ ◡ ◡ 𝐹 ) |
9 |
7 8
|
ax-mp |
⊢ ◡ ( ◡ 𝐹 ↾ 𝐶 ) ⊆ ◡ ◡ 𝐹 |
10 |
|
cnvcnvss |
⊢ ◡ ◡ 𝐹 ⊆ 𝐹 |
11 |
9 10
|
sstri |
⊢ ◡ ( ◡ 𝐹 ↾ 𝐶 ) ⊆ 𝐹 |
12 |
|
funss |
⊢ ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) ⊆ 𝐹 → ( Fun 𝐹 → Fun ◡ ( ◡ 𝐹 ↾ 𝐶 ) ) ) |
13 |
11 2 12
|
mpsyl |
⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Fun ◡ ( ◡ 𝐹 ↾ 𝐶 ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → Fun ◡ ( ◡ 𝐹 ↾ 𝐶 ) ) |
15 |
|
df-ima |
⊢ ( ◡ 𝐹 “ 𝐶 ) = ran ( ◡ 𝐹 ↾ 𝐶 ) |
16 |
|
df-rn |
⊢ ran ( ◡ 𝐹 ↾ 𝐶 ) = dom ◡ ( ◡ 𝐹 ↾ 𝐶 ) |
17 |
15 16
|
eqtr2i |
⊢ dom ◡ ( ◡ 𝐹 ↾ 𝐶 ) = ( ◡ 𝐹 “ 𝐶 ) |
18 |
|
df-fn |
⊢ ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) Fn ( ◡ 𝐹 “ 𝐶 ) ↔ ( Fun ◡ ( ◡ 𝐹 ↾ 𝐶 ) ∧ dom ◡ ( ◡ 𝐹 ↾ 𝐶 ) = ( ◡ 𝐹 “ 𝐶 ) ) ) |
19 |
14 17 18
|
sylanblrc |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ◡ ( ◡ 𝐹 ↾ 𝐶 ) Fn ( ◡ 𝐹 “ 𝐶 ) ) |
20 |
|
dfdm4 |
⊢ dom ( ◡ 𝐹 ↾ 𝐶 ) = ran ◡ ( ◡ 𝐹 ↾ 𝐶 ) |
21 |
|
forn |
⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 ) |
22 |
21
|
sseq2d |
⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐶 ⊆ ran 𝐹 ↔ 𝐶 ⊆ 𝐵 ) ) |
23 |
22
|
biimpar |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ⊆ ran 𝐹 ) |
24 |
|
df-rn |
⊢ ran 𝐹 = dom ◡ 𝐹 |
25 |
23 24
|
sseqtrdi |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → 𝐶 ⊆ dom ◡ 𝐹 ) |
26 |
|
ssdmres |
⊢ ( 𝐶 ⊆ dom ◡ 𝐹 ↔ dom ( ◡ 𝐹 ↾ 𝐶 ) = 𝐶 ) |
27 |
25 26
|
sylib |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → dom ( ◡ 𝐹 ↾ 𝐶 ) = 𝐶 ) |
28 |
20 27
|
eqtr3id |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ran ◡ ( ◡ 𝐹 ↾ 𝐶 ) = 𝐶 ) |
29 |
|
df-fo |
⊢ ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) : ( ◡ 𝐹 “ 𝐶 ) –onto→ 𝐶 ↔ ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) Fn ( ◡ 𝐹 “ 𝐶 ) ∧ ran ◡ ( ◡ 𝐹 ↾ 𝐶 ) = 𝐶 ) ) |
30 |
19 28 29
|
sylanbrc |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ◡ ( ◡ 𝐹 ↾ 𝐶 ) : ( ◡ 𝐹 “ 𝐶 ) –onto→ 𝐶 ) |
31 |
|
foima |
⊢ ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) : ( ◡ 𝐹 “ 𝐶 ) –onto→ 𝐶 → ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) “ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐶 ) |
32 |
30 31
|
syl |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) “ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐶 ) |
33 |
6 32
|
eqtr3d |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) “ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐶 ) |
34 |
1 33
|
eqtr3id |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐶 ) |