Metamath Proof Explorer

Theorem foimacnv

Description: A reverse version of f1imacnv . (Contributed by Jeff Hankins, 16-Jul-2009)

Ref Expression
Assertion foimacnv ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐶 )

Proof

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 syl5eqr ⊢ ( ( 𝐹 : 𝐴 –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 syl5eqr ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝐶 ⊆ 𝐵 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝐶 ) ) = 𝐶 )