f1oresf1o

Description: Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022)

	Ref	Expression
Hypotheses	f1oresf1o.1	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$
	f1oresf1o.2	$⊢ φ \to D \subseteq A$
	f1oresf1o.3	$⊢ φ \to (\exists x \in D F (x) = y \leftrightarrow (y \in B \land χ))$
Assertion	f1oresf1o	$⊢ φ \to ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} \{y \in B \| χ\}$

Step	Hyp	Ref	Expression
1		f1oresf1o.1	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$
2		f1oresf1o.2	$⊢ φ \to D \subseteq A$
3		f1oresf1o.3	$⊢ φ \to (\exists x \in D F (x) = y \leftrightarrow (y \in B \land χ))$
4		f1of1	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{1-1}{⟶} B$
5	1 4	syl	$⊢ φ \to F : A \underset{1-1}{⟶} B$
6		f1ores	$⊢ (F : A \underset{1-1}{⟶} B \land D \subseteq A) \to ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} F [D]$
7	5 2 6	syl2anc	$⊢ φ \to ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} F [D]$
8		f1ofun	$⊢ F : A \underset{1-1 onto}{⟶} B \to Fun F$
9	1 8	syl	$⊢ φ \to Fun F$
10		f1odm	$⊢ F : A \underset{1-1 onto}{⟶} B \to dom F = A$
11	1 10	syl	$⊢ φ \to dom F = A$
12	2 11	sseqtrrd	$⊢ φ \to D \subseteq dom F$
13		dfimafn	$⊢ (Fun F \land D \subseteq dom F) \to F [D] = \{y \| \exists x \in D F (x) = y\}$
14	9 12 13	syl2anc	$⊢ φ \to F [D] = \{y \| \exists x \in D F (x) = y\}$
15	3	abbidv	$⊢ φ \to \{y \| \exists x \in D F (x) = y\} = \{y \| (y \in B \land χ)\}$
16		df-rab	$⊢ \{y \in B \| χ\} = \{y \| (y \in B \land χ)\}$
17	15 16	syl6eqr	$⊢ φ \to \{y \| \exists x \in D F (x) = y\} = \{y \in B \| χ\}$
18	14 17	eqtr2d	$⊢ φ \to \{y \in B \| χ\} = F [D]$
19	18	f1oeq3d	$⊢ φ \to (({F ↾}_{D}) : D \underset{1-1 onto}{⟶} \{y \in B \| χ\} \leftrightarrow ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} F [D])$
20	7 19	mpbird	$⊢ φ \to ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} \{y \in B \| χ\}$

Metamath Proof Explorer