Metamath Proof Explorer

Theorem foimacnv

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

Ref Expression
Assertion foimacnv ⊢ F : A ⟶ onto B ∧ C ⊆ B → F F -1 C = C

Proof

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