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)

		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		foelrn	$⊢ (F : A \underset{onto}{⟶} B \land y \in B) \to \exists z \in A y = F (z)$
4		fofn	$⊢ F : A \underset{onto}{⟶} B \to F Fn A$
5		eqcom	$⊢ F (z) = y \leftrightarrow y = F (z)$
6		fniniseg	$⊢ F Fn A \to (z \in F^{-1} [\{y\}] \leftrightarrow (z \in A \land F (z) = y))$
7	6	biimpar	$⊢ (F Fn A \land (z \in A \land F (z) = y)) \to z \in F^{-1} [\{y\}]$
8	7	anassrs	$⊢ ((F Fn A \land z \in A) \land F (z) = y) \to z \in F^{-1} [\{y\}]$
9	5 8	sylan2br	$⊢ ((F Fn A \land z \in A) \land y = F (z)) \to z \in F^{-1} [\{y\}]$
10	4 9	sylanl1	$⊢ ((F : A \underset{onto}{⟶} B \land z \in A) \land y = F (z)) \to z \in F^{-1} [\{y\}]$
11	10	ex	$⊢ (F : A \underset{onto}{⟶} B \land z \in A) \to (y = F (z) \to z \in F^{-1} [\{y\}])$
12	11	reximdva	$⊢ F : A \underset{onto}{⟶} B \to (\exists z \in A y = F (z) \to \exists z \in A z \in F^{-1} [\{y\}])$
13	12	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\}])$
14	3 13	mpd	$⊢ (F : A \underset{onto}{⟶} B \land y \in B) \to \exists z \in A z \in F^{-1} [\{y\}]$
15	14	adantll	$⊢ ((A \in V \land F : A \underset{onto}{⟶} B) \land y \in B) \to \exists z \in A z \in F^{-1} [\{y\}]$
16	15	ralrimiva	$⊢ (A \in V \land F : A \underset{onto}{⟶} B) \to \forall y \in B \exists z \in A z \in F^{-1} [\{y\}]$
17		eleq1	$⊢ z = g (y) \to (z \in F^{-1} [\{y\}] \leftrightarrow g (y) \in F^{-1} [\{y\}])$
18	17	ac6sg	$⊢ B \in V \to (\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\}]))$
19	2 16 18	sylc	$⊢ (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\}])$
20		frn	$⊢ g : B ⟶ A \to ran g \subseteq A$
21	20	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$
22		vex	$⊢ g \in V$
23	22	rnex	$⊢ ran g \in V$
24	23	elpw	$⊢ ran g \in 𝒫 A \leftrightarrow ran g \subseteq A$
25	21 24	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$
26		fof	$⊢ F : A \underset{onto}{⟶} B \to F : A ⟶ B$
27	26	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$
28	27 21	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$
29		ffn	$⊢ g : B ⟶ A \to g Fn B$
30	29	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$
31		dffn3	$⊢ g Fn B \leftrightarrow g : B ⟶ ran g$
32	30 31	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$
33		fvres	$⊢ z \in ran g \to ({F ↾}_{ran g}) (z) = F (z)$
34	33	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)$
35	34	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))$
36		nfv	$⊢ Ⅎ y (A \in V \land F : A \underset{onto}{⟶} B)$
37		nfv	$⊢ Ⅎ y g : B ⟶ A$
38		nfra1	$⊢ Ⅎ y \forall y \in B g (y) \in F^{-1} [\{y\}]$
39	37 38	nfan	$⊢ Ⅎ y (g : B ⟶ A \land \forall y \in B g (y) \in F^{-1} [\{y\}])$
40	36 39	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\}]))$
41		nfv	$⊢ Ⅎ y z \in ran g$
42	40 41	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)$
43		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$
44	43	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)$
45	4	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$
46		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\}]$
47	46	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\}]$
48		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$
49		rspa	$⊢ (\forall y \in B g (y) \in F^{-1} [\{y\}] \land y \in B) \to g (y) \in F^{-1} [\{y\}]$
50	47 48 49	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\}]$
51		fniniseg	$⊢ F Fn A \to (g (y) \in F^{-1} [\{y\}] \leftrightarrow (g (y) \in A \land F (g (y)) = y))$
52	51	simplbda	$⊢ (F Fn A \land g (y) \in F^{-1} [\{y\}]) \to F (g (y)) = y$
53	45 50 52	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$
54	44 53	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$
55	54	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)$
56	55 43	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$
57		fvelrnb	$⊢ g Fn B \to (z \in ran g \leftrightarrow \exists y \in B g (y) = z)$
58	57	biimpa	$⊢ (g Fn B \land z \in ran g) \to \exists y \in B g (y) = z$
59	30 58	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$
60	42 56 59	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$
61	35 60	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$
62	61	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$
63	32	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$
64		fvres	$⊢ g (y) \in ran g \to ({F ↾}_{ran g}) (g (y)) = F (g (y))$
65	63 64	syl	$⊢ (((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))$
66	4	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$
67		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\}]$
68		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$
69	67 68 49	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\}]$
70	66 69 52	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$
71	65 70	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$
72	71	ex	$⊢ ((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 (y \in B \to ({F ↾}_{ran g}) (g (y)) = y)$
73	40 72	ralrimi	$⊢ ((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$
74	28 32 62 73	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$
75		reseq2	$⊢ x = ran g \to {F ↾}_{x} = {F ↾}_{ran g}$
76		id	$⊢ x = ran g \to x = ran g$
77		eqidd	$⊢ x = ran g \to B = B$
78	75 76 77	f1oeq123d	$⊢ x = ran g \to (({F ↾}_{x}) : x \underset{1-1 onto}{⟶} B \leftrightarrow ({F ↾}_{ran g}) : ran g \underset{1-1 onto}{⟶} B)$
79	78	rspcev	$⊢ (ran g \in 𝒫 A \land ({F ↾}_{ran g}) : ran g \underset{1-1 onto}{⟶} B) \to \exists x \in 𝒫 A ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} B$
80	25 74 79	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\}])) \to \exists x \in 𝒫 A ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} B$
81	19 80	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