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 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 )

Proof

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