f1oresf1o2

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

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

Proof

Step	Hyp	Ref	Expression
1		f1oresf1o2.1	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$
2		f1oresf1o2.2	$⊢ φ \to D \subseteq A$
3		f1oresf1o2.3	$⊢ (φ \land y = F (x)) \to (x \in D \leftrightarrow χ)$
4		f1of	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A ⟶ B$
5	1 4	syl	$⊢ φ \to F : A ⟶ B$
6	5	adantr	$⊢ (φ \land x \in D) \to F : A ⟶ B$
7	2	sselda	$⊢ (φ \land x \in D) \to x \in A$
8	6 7	jca	$⊢ (φ \land x \in D) \to (F : A ⟶ B \land x \in A)$
9	8	3adant3	$⊢ (φ \land x \in D \land F (x) = y) \to (F : A ⟶ B \land x \in A)$
10		ffvelcdm	$⊢ (F : A ⟶ B \land x \in A) \to F (x) \in B$
11	9 10	syl	$⊢ (φ \land x \in D \land F (x) = y) \to F (x) \in B$
12		eleq1	$⊢ F (x) = y \to (F (x) \in B \leftrightarrow y \in B)$
13	12	3ad2ant3	$⊢ (φ \land x \in D \land F (x) = y) \to (F (x) \in B \leftrightarrow y \in B)$
14	11 13	mpbid	$⊢ (φ \land x \in D \land F (x) = y) \to y \in B$
15		eqcom	$⊢ F (x) = y \leftrightarrow y = F (x)$
16	3	biimpd	$⊢ (φ \land y = F (x)) \to (x \in D \to χ)$
17	16	ex	$⊢ φ \to (y = F (x) \to (x \in D \to χ))$
18	15 17	biimtrid	$⊢ φ \to (F (x) = y \to (x \in D \to χ))$
19	18	com23	$⊢ φ \to (x \in D \to (F (x) = y \to χ))$
20	19	3imp	$⊢ (φ \land x \in D \land F (x) = y) \to χ$
21	14 20	jca	$⊢ (φ \land x \in D \land F (x) = y) \to (y \in B \land χ)$
22	21	rexlimdv3a	$⊢ φ \to (\exists x \in D F (x) = y \to (y \in B \land χ))$
23		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
24	1 23	syl	$⊢ φ \to F : A \underset{onto}{⟶} B$
25		foelcdmi	$⊢ (F : A \underset{onto}{⟶} B \land y \in B) \to \exists x \in A F (x) = y$
26	24 25	sylan	$⊢ (φ \land y \in B) \to \exists x \in A F (x) = y$
27	26	ex	$⊢ φ \to (y \in B \to \exists x \in A F (x) = y)$
28		nfv	$⊢ Ⅎ x φ$
29		nfv	$⊢ Ⅎ x χ$
30		nfre1	$⊢ Ⅎ x \exists x \in D F (x) = y$
31	29 30	nfim	$⊢ Ⅎ x (χ \to \exists x \in D F (x) = y)$
32		rspe	$⊢ (x \in D \land F (x) = y) \to \exists x \in D F (x) = y$
33	32	expcom	$⊢ F (x) = y \to (x \in D \to \exists x \in D F (x) = y)$
34	33	eqcoms	$⊢ y = F (x) \to (x \in D \to \exists x \in D F (x) = y)$
35	34	adantl	$⊢ (φ \land y = F (x)) \to (x \in D \to \exists x \in D F (x) = y)$
36	3 35	sylbird	$⊢ (φ \land y = F (x)) \to (χ \to \exists x \in D F (x) = y)$
37	36	ex	$⊢ φ \to (y = F (x) \to (χ \to \exists x \in D F (x) = y))$
38	37	adantr	$⊢ (φ \land x \in A) \to (y = F (x) \to (χ \to \exists x \in D F (x) = y))$
39	15 38	biimtrid	$⊢ (φ \land x \in A) \to (F (x) = y \to (χ \to \exists x \in D F (x) = y))$
40	39	ex	$⊢ φ \to (x \in A \to (F (x) = y \to (χ \to \exists x \in D F (x) = y)))$
41	28 31 40	rexlimd	$⊢ φ \to (\exists x \in A F (x) = y \to (χ \to \exists x \in D F (x) = y))$
42	27 41	syld	$⊢ φ \to (y \in B \to (χ \to \exists x \in D F (x) = y))$
43	42	impd	$⊢ φ \to ((y \in B \land χ) \to \exists x \in D F (x) = y)$
44	22 43	impbid	$⊢ φ \to (\exists x \in D F (x) = y \leftrightarrow (y \in B \land χ))$
45	1 2 44	f1oresf1o	$⊢ φ \to ({F ↾}_{D}) : D \underset{1-1 onto}{⟶} \{y \in B \| χ\}$

Metamath Proof Explorer

Theorem f1oresf1o2

Proof