Metamath Proof Explorer

Theorem fresf1o

Description: Conditions for a restriction to be a one-to-one onto function. (Contributed by Thierry Arnoux, 7-Dec-2016)

Ref Expression
Assertion fresf1o ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F ↾ F -1 C : F -1 C ⟶ 1-1 onto C

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ F -1 ↾ C ↔ F -1 ↾ C Fn dom ⁡ F -1 ↾ C
2 1 biimpi ⊢ Fun ⁡ F -1 ↾ C → F -1 ↾ C Fn dom ⁡ F -1 ↾ C
3 2 3ad2ant3 ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C Fn dom ⁡ F -1 ↾ C
4 simp2 ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → C ⊆ ran ⁡ F
5 df-rn ⊢ ran ⁡ F = dom ⁡ F -1
6 4 5 sseqtrdi ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → C ⊆ dom ⁡ F -1
7 ssdmres ⊢ C ⊆ dom ⁡ F -1 ↔ dom ⁡ F -1 ↾ C = C
8 6 7 sylib ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → dom ⁡ F -1 ↾ C = C
9 8 fneq2d ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C Fn dom ⁡ F -1 ↾ C ↔ F -1 ↾ C Fn C
10 3 9 mpbid ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C Fn C
11 simp1 ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → Fun ⁡ F
12 funres ⊢ Fun ⁡ F → Fun ⁡ F ↾ F -1 C
13 11 12 syl ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → Fun ⁡ F ↾ F -1 C
14 funcnvres2 ⊢ Fun ⁡ F → F -1 ↾ C -1 = F ↾ F -1 C
15 11 14 syl ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C -1 = F ↾ F -1 C
16 15 funeqd ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → Fun ⁡ F -1 ↾ C -1 ↔ Fun ⁡ F ↾ F -1 C
17 13 16 mpbird ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → Fun ⁡ F -1 ↾ C -1
18 df-ima ⊢ F -1 C = ran ⁡ F -1 ↾ C
19 18 eqcomi ⊢ ran ⁡ F -1 ↾ C = F -1 C
20 19 a1i ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → ran ⁡ F -1 ↾ C = F -1 C
21 dff1o2 ⊢ F -1 ↾ C : C ⟶ 1-1 onto F -1 C ↔ F -1 ↾ C Fn C ∧ Fun ⁡ F -1 ↾ C -1 ∧ ran ⁡ F -1 ↾ C = F -1 C
22 10 17 20 21 syl3anbrc ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C : C ⟶ 1-1 onto F -1 C
23 f1ocnv ⊢ F -1 ↾ C : C ⟶ 1-1 onto F -1 C → F -1 ↾ C -1 : F -1 C ⟶ 1-1 onto C
24 22 23 syl ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C -1 : F -1 C ⟶ 1-1 onto C
25 f1oeq1 ⊢ F -1 ↾ C -1 = F ↾ F -1 C → F -1 ↾ C -1 : F -1 C ⟶ 1-1 onto C ↔ F ↾ F -1 C : F -1 C ⟶ 1-1 onto C
26 11 14 25 3syl ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C -1 : F -1 C ⟶ 1-1 onto C ↔ F ↾ F -1 C : F -1 C ⟶ 1-1 onto C
27 24 26 mpbid ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F ↾ F -1 C : F -1 C ⟶ 1-1 onto C