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 \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1 onto}{⟶} C$

Proof

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun ({F^{-1} ↾}_{C}) \leftrightarrow ({F^{-1} ↾}_{C}) Fn dom ({F^{-1} ↾}_{C})$
2	1	biimpi	$⊢ Fun ({F^{-1} ↾}_{C}) \to ({F^{-1} ↾}_{C}) Fn dom ({F^{-1} ↾}_{C})$
3	2	3ad2ant3	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to ({F^{-1} ↾}_{C}) Fn dom ({F^{-1} ↾}_{C})$
4		simp2	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to C \subseteq ran F$
5		df-rn	$⊢ ran F = dom F^{-1}$
6	4 5	sseqtrdi	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to C \subseteq dom F^{-1}$
7		ssdmres	$⊢ C \subseteq dom F^{-1} \leftrightarrow dom ({F^{-1} ↾}_{C}) = C$
8	6 7	sylib	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to dom ({F^{-1} ↾}_{C}) = C$
9	8	fneq2d	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to (({F^{-1} ↾}_{C}) Fn dom ({F^{-1} ↾}_{C}) \leftrightarrow ({F^{-1} ↾}_{C}) Fn C)$
10	3 9	mpbid	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to ({F^{-1} ↾}_{C}) Fn C$
11		simp1	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to Fun F$
12	11	funresd	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to Fun ({F ↾}_{F^{-1} [C]})$
13		funcnvres2	$⊢ Fun F \to {({F^{-1} ↾}_{C})}^{-1} = {F ↾}_{F^{-1} [C]}$
14	11 13	syl	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to {({F^{-1} ↾}_{C})}^{-1} = {F ↾}_{F^{-1} [C]}$
15	14	funeqd	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to (Fun {({F^{-1} ↾}_{C})}^{-1} \leftrightarrow Fun ({F ↾}_{F^{-1} [C]}))$
16	12 15	mpbird	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to 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 \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to ran ({F^{-1} ↾}_{C}) = F^{-1} [C]$
20		dff1o2	$⊢ ({F^{-1} ↾}_{C}) : C \underset{1-1 onto}{⟶} F^{-1} [C] \leftrightarrow (({F^{-1} ↾}_{C}) Fn C \land Fun {({F^{-1} ↾}_{C})}^{-1} \land ran ({F^{-1} ↾}_{C}) = F^{-1} [C])$
21	10 16 19 20	syl3anbrc	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to ({F^{-1} ↾}_{C}) : C \underset{1-1 onto}{⟶} F^{-1} [C]$
22		f1ocnv	$⊢ ({F^{-1} ↾}_{C}) : C \underset{1-1 onto}{⟶} F^{-1} [C] \to {({F^{-1} ↾}_{C})}^{-1} : F^{-1} [C] \underset{1-1 onto}{⟶} C$
23	21 22	syl	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to {({F^{-1} ↾}_{C})}^{-1} : F^{-1} [C] \underset{1-1 onto}{⟶} C$
24		f1oeq1	$⊢ {({F^{-1} ↾}_{C})}^{-1} = {F ↾}_{F^{-1} [C]} \to ({({F^{-1} ↾}_{C})}^{-1} : F^{-1} [C] \underset{1-1 onto}{⟶} C \leftrightarrow ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1 onto}{⟶} C)$
25	11 13 24	3syl	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to ({({F^{-1} ↾}_{C})}^{-1} : F^{-1} [C] \underset{1-1 onto}{⟶} C \leftrightarrow ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1 onto}{⟶} C)$
26	23 25	mpbid	$⊢ (Fun F \land C \subseteq ran F \land Fun ({F^{-1} ↾}_{C})) \to ({F ↾}_{F^{-1} [C]}) : F^{-1} [C] \underset{1-1 onto}{⟶} C$

Metamath Proof Explorer

Theorem fresf1o

Proof