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 11 funresd ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → Fun ⁡ F ↾ F -1 C
13 funcnvres2 ⊢ Fun ⁡ F → F -1 ↾ C -1 = F ↾ F -1 C
14 11 13 syl ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C -1 = F ↾ F -1 C
15 14 funeqd ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → Fun ⁡ F -1 ↾ C -1 ↔ Fun ⁡ F ↾ F -1 C
16 12 15 mpbird ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → Fun ⁡ F -1 ↾ C -1
17 df-ima ⊢ F -1 C = ran ⁡ F -1 ↾ C
18 17 eqcomi ⊢ ran ⁡ F -1 ↾ C = F -1 C
19 18 a1i ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → ran ⁡ F -1 ↾ C = F -1 C
20 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
21 10 16 19 20 syl3anbrc ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C : C ⟶ 1-1 onto F -1 C
22 f1ocnv ⊢ F -1 ↾ C : C ⟶ 1-1 onto F -1 C → F -1 ↾ C -1 : F -1 C ⟶ 1-1 onto C
23 21 22 syl ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F -1 ↾ C -1 : F -1 C ⟶ 1-1 onto C
24 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
25 11 13 24 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
26 23 25 mpbid ⊢ Fun ⁡ F ∧ C ⊆ ran ⁡ F ∧ Fun ⁡ F -1 ↾ C → F ↾ F -1 C : F -1 C ⟶ 1-1 onto C