foresf1o

Description: From a surjective function, *choose* a subset of the domain, such that the restricted function is bijective. (Contributed by Thierry Arnoux, 27-Jan-2020) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

		Ref	Expression
	Assertion	foresf1o	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to \exists x \in 𝒫 A ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		focdmex	$⊢ A \in V \to (F : A \underset{onto}{⟶} B \to B \in V)$
2	1	imp	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to B \in V$
3		simpl	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to A \in V$
4		foelrn	$⊢ (F : A \underset{onto}{⟶} B \land y \in B) \to \exists z \in A y = F (z)$
5		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
6		eqcom	$⊢ F (z) = y \leftrightarrow y = F (z)$
7		fniniseg	$⊢ F Fn A \to (z \in F^{-1} [\{y\}] \leftrightarrow (z \in A \land F (z) = y))$
8	7	biimpar	$⊢ (F Fn A \land (z \in A \land F (z) = y)) \to z \in F^{-1} [\{y\}]$
9	8	anassrs	$⊢ ((F Fn A \land z \in A) \land F (z) = y) \to z \in F^{-1} [\{y\}]$
10	6 9	sylan2br	$⊢ ((F Fn A \land z \in A) \land y = F (z)) \to z \in F^{-1} [\{y\}]$
11	5 10	sylanl1	$⊢ ((F : A \underset{onto}{⟶} B \land z \in A) \land y = F (z)) \to z \in F^{-1} [\{y\}]$
12	11	ex	$⊢ (F : A \underset{onto}{⟶} B \land z \in A) \to (y = F (z) \to z \in F^{-1} [\{y\}])$
13	12	reximdva	$⊢ F : A \underset{onto}{⟶} B \to (\exists z \in A y = F (z) \to \exists z \in A z \in F^{-1} [\{y\}])$
14	13	adantr	$⊢ (F : A \underset{onto}{⟶} B \land y \in B) \to (\exists z \in A y = F (z) \to \exists z \in A z \in F^{-1} [\{y\}])$
15	4 14	mpd	$⊢ (F : A \underset{onto}{⟶} B \land y \in B) \to \exists z \in A z \in F^{-1} [\{y\}]$
16	15	adantll	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land y \in B) \to \exists z \in A z \in F^{-1} [\{y\}]$
17	16	ralrimiva	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to \forall y \in B \exists z \in A z \in F^{-1} [\{y\}]$
18		eleq1	$⊢ z = g (y) \to (z \in F^{-1} [\{y\}] \leftrightarrow g (y) \in F^{-1} [\{y\}])$
19	18	ac6	$⊢ (B \in V \land A \in V \land \forall y \in B \exists z \in A z \in F^{-1} [\{y\}]) \to \exists g (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])$
20	2 3 17 19	syl3anc	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to \exists g (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])$
21		reseq2	$⊢ x = ran g \to {F ↾}_{x} = {F ↾}_{ran g}$
22		id	$⊢ x = ran g \to x = ran g$
23		eqidd	$⊢ x = ran g \to B = B$
24	21 22 23	f1oeq123d	$⊢ x = ran g \to (({F ↾}_{x}) : x \underset{1-1 onto}{⟶} B \leftrightarrow ({F ↾}_{ran g}) : ran g \underset{1-1 onto}{⟶} B)$
25		frn	$⊢ g : B ⟶ A \to ran g \subseteq A$
26	25	ad2antrl	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to ran g \subseteq A$
27		vex	$⊢ g \in V$
28	27	rnex	$⊢ ran g \in V$
29	28	elpw	$⊢ ran g \in 𝒫 A \leftrightarrow ran g \subseteq A$
30	26 29	sylibr	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to ran g \in 𝒫 A$
31		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
32	31	ad2antlr	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to F : A ⟶ B$
33	32 26	fssresd	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to ({F ↾}_{ran g}) : ran g ⟶ B$
34		ffn	$⊢ g : B ⟶ A \to g Fn B$
35	34	ad2antrl	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to g Fn B$
36		dffn3	$⊢ g Fn B \leftrightarrow g : B ⟶ ran g$
37	35 36	sylib	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to g : B ⟶ ran g$
38		fvres	$⊢ z \in ran g \to ({F ↾}_{ran g}) (z) = F (z)$
39	38	adantl	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \to ({F ↾}_{ran g}) (z) = F (z)$
40	39	fveq2d	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \to g (({F ↾}_{ran g}) (z)) = g (F (z))$
41		nfv	$⊢ Ⅎ y (A \in V \land F : A \underset{onto}{⟶} B)$
42		nfv	$⊢ Ⅎ y g : B ⟶ A$
43		nfra1	$⊢ Ⅎ y \forall y \in B g (y) \in F^{-1} [\{y\}]$
44	42 43	nfan	$⊢ Ⅎ y (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])$
45	41 44	nfan	$⊢ Ⅎ y ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}]))$
46		nfv	$⊢ Ⅎ y z \in ran g$
47	45 46	nfan	$⊢ Ⅎ y (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g)$
48		simpr	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to g (y) = z$
49	48	fveq2d	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to F (g (y)) = F (z)$
50	5	ad5antlr	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to F Fn A$
51		simplrr	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \to \forall y \in B g (y) \in F^{-1} [\{y\}]$
52	51	ad2antrr	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to \forall y \in B g (y) \in F^{-1} [\{y\}]$
53		simplr	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to y \in B$
54		rspa	$⊢ (\forall y \in B g (y) \in F^{-1} [\{y\}] \land y \in B) \to g (y) \in F^{-1} [\{y\}]$
55	52 53 54	syl2anc	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to g (y) \in F^{-1} [\{y\}]$
56		fniniseg	$⊢ F Fn A \to (g (y) \in F^{-1} [\{y\}] \leftrightarrow (g (y) \in A \land F (g (y)) = y))$
57	56	simplbda	$⊢ (F Fn A \land g (y) \in F^{-1} [\{y\}]) \to F (g (y)) = y$
58	50 55 57	syl2anc	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to F (g (y)) = y$
59	49 58	eqtr3d	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to F (z) = y$
60	59	fveq2d	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to g (F (z)) = g (y)$
61	60 48	eqtrd	$⊢ (((((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \land y \in B) \land g (y) = z) \to g (F (z)) = z$
62		fvelrnb	$⊢ g Fn B \to (z \in ran g \leftrightarrow \exists y \in B g (y) = z)$
63	62	biimpa	$⊢ (g Fn B \land z \in ran g) \to \exists y \in B g (y) = z$
64	35 63	sylan	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \to \exists y \in B g (y) = z$
65	47 61 64	r19.29af	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \to g (F (z)) = z$
66	40 65	eqtrd	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land z \in ran g) \to g (({F ↾}_{ran g}) (z)) = z$
67	66	ralrimiva	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to \forall z \in ran g g (({F ↾}_{ran g}) (z)) = z$
68	37	ffvelcdmda	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land y \in B) \to g (y) \in ran g$
69	68	fvresd	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land y \in B) \to ({F ↾}_{ran g}) (g (y)) = F (g (y))$
70	5	ad3antlr	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land y \in B) \to F Fn A$
71		simplrr	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land y \in B) \to \forall y \in B g (y) \in F^{-1} [\{y\}]$
72		simpr	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land y \in B) \to y \in B$
73	71 72 54	syl2anc	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land y \in B) \to g (y) \in F^{-1} [\{y\}]$
74	70 73 57	syl2anc	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land y \in B) \to F (g (y)) = y$
75	69 74	eqtrd	$⊢ (((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \land y \in B) \to ({F ↾}_{ran g}) (g (y)) = y$
76	45 75	ralrimia	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to \forall y \in B ({F ↾}_{ran g}) (g (y)) = y$
77	33 37 67 76	2fvidf1od	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to ({F ↾}_{ran g}) : ran g \underset{1-1 onto}{⟶} B$
78	24 30 77	rspcedvdw	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])) \to \exists x \in 𝒫 A ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} B$
79	20 78	exlimddv	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to \exists x \in 𝒫 A ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem foresf1o

Proof