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 11 funresd ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → Fun ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) )
13 funcnvres2 ⊢ ( Fun 𝐹 → ◡ ( ◡ 𝐹 ↾ 𝐶 ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) )
14 11 13 syl ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → ◡ ( ◡ 𝐹 ↾ 𝐶 ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) )
15 14 funeqd ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → ( Fun ◡ ( ◡ 𝐹 ↾ 𝐶 ) ↔ Fun ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) ) )
16 12 15 mpbird ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → Fun ◡ ( ◡ 𝐹 ↾ 𝐶 ) )
17 df-ima ⊢ ( ◡ 𝐹 “ 𝐶 ) = ran ( ◡ 𝐹 ↾ 𝐶 )
18 17 eqcomi ⊢ ran ( ◡ 𝐹 ↾ 𝐶 ) = ( ◡ 𝐹 “ 𝐶 )
19 18 a1i ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → ran ( ◡ 𝐹 ↾ 𝐶 ) = ( ◡ 𝐹 “ 𝐶 ) )
20 dff1o2 ⊢ ( ( ◡ 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( ◡ 𝐹 “ 𝐶 ) ↔ ( ( ◡ 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ Fun ◡ ( ◡ 𝐹 ↾ 𝐶 ) ∧ ran ( ◡ 𝐹 ↾ 𝐶 ) = ( ◡ 𝐹 “ 𝐶 ) ) )
21 10 16 19 20 syl3anbrc ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → ( ◡ 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( ◡ 𝐹 “ 𝐶 ) )
22 f1ocnv ⊢ ( ( ◡ 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ ( ◡ 𝐹 “ 𝐶 ) → ◡ ( ◡ 𝐹 ↾ 𝐶 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 )
23 21 22 syl ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → ◡ ( ◡ 𝐹 ↾ 𝐶 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 )
24 f1oeq1 ⊢ ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) → ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 ↔ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 ) )
25 11 13 24 3syl ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → ( ◡ ( ◡ 𝐹 ↾ 𝐶 ) : ( ◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 ↔ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 ) )
26 23 25 mpbid ⊢ ( ( Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹 ∧ Fun ( ◡ 𝐹 ↾ 𝐶 ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐶 ) ) : ( ◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐶 )