acunirnmpt2

Description: Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019)

	Ref	Expression
Hypotheses	acunirnmpt.0	$⊢ φ \to A \in V$
	acunirnmpt.1	$⊢ (φ \land j \in A) \to B \neq \emptyset$
	acunirnmpt2.2	$⊢ C = ⋃ ran (j \in A ⟼ B)$
	acunirnmpt2.3	$⊢ j = f (x) \to B = D$
Assertion	acunirnmpt2	$⊢ φ \to \exists f (f : C ⟶ A \land \forall x \in C x \in D)$

Proof

Step	Hyp	Ref	Expression
1		acunirnmpt.0	$⊢ φ \to A \in V$
2		acunirnmpt.1	$⊢ (φ \land j \in A) \to B \neq \emptyset$
3		acunirnmpt2.2	$⊢ C = ⋃ ran (j \in A ⟼ B)$
4		acunirnmpt2.3	$⊢ j = f (x) \to B = D$
5		simplr	$⊢ (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \to y \in ran (j \in A ⟼ B)$
6		vex	$⊢ y \in V$
7		eqid	$⊢ (j \in A ⟼ B) = (j \in A ⟼ B)$
8	7	elrnmpt	$⊢ y \in V \to (y \in ran (j \in A ⟼ B) \leftrightarrow \exists j \in A y = B)$
9	6 8	ax-mp	$⊢ y \in ran (j \in A ⟼ B) \leftrightarrow \exists j \in A y = B$
10	5 9	sylib	$⊢ (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \to \exists j \in A y = B$
11		nfv	$⊢ Ⅎ j (φ \land x \in C)$
12		nfcv	$⊢ \underline{Ⅎ} j y$
13		nfmpt1	$⊢ \underline{Ⅎ} j (j \in A ⟼ B)$
14	13	nfrn	$⊢ \underline{Ⅎ} j ran (j \in A ⟼ B)$
15	12 14	nfel	$⊢ Ⅎ j y \in ran (j \in A ⟼ B)$
16	11 15	nfan	$⊢ Ⅎ j ((φ \land x \in C) \land y \in ran (j \in A ⟼ B))$
17		nfv	$⊢ Ⅎ j x \in y$
18	16 17	nfan	$⊢ Ⅎ j (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y)$
19		simpllr	$⊢ (((((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \land j \in A) \land y = B) \to x \in y$
20		simpr	$⊢ (((((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \land j \in A) \land y = B) \to y = B$
21	19 20	eleqtrd	$⊢ (((((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \land j \in A) \land y = B) \to x \in B$
22	21	ex	$⊢ ((((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \land j \in A) \to (y = B \to x \in B)$
23	22	ex	$⊢ (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \to (j \in A \to (y = B \to x \in B))$
24	18 23	reximdai	$⊢ (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \to (\exists j \in A y = B \to \exists j \in A x \in B)$
25	10 24	mpd	$⊢ (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \to \exists j \in A x \in B$
26	3	eleq2i	$⊢ x \in C \leftrightarrow x \in ⋃ ran (j \in A ⟼ B)$
27	26	biimpi	$⊢ x \in C \to x \in ⋃ ran (j \in A ⟼ B)$
28		eluni2	$⊢ x \in ⋃ ran (j \in A ⟼ B) \leftrightarrow \exists y \in ran (j \in A ⟼ B) x \in y$
29	27 28	sylib	$⊢ x \in C \to \exists y \in ran (j \in A ⟼ B) x \in y$
30	29	adantl	$⊢ (φ \land x \in C) \to \exists y \in ran (j \in A ⟼ B) x \in y$
31	25 30	r19.29a	$⊢ (φ \land x \in C) \to \exists j \in A x \in B$
32	31	ralrimiva	$⊢ φ \to \forall x \in C \exists j \in A x \in B$
33		mptexg	$⊢ A \in V \to (j \in A ⟼ B) \in V$
34		rnexg	$⊢ (j \in A ⟼ B) \in V \to ran (j \in A ⟼ B) \in V$
35		uniexg	$⊢ ran (j \in A ⟼ B) \in V \to ⋃ ran (j \in A ⟼ B) \in V$
36	1 33 34 35	4syl	$⊢ φ \to ⋃ ran (j \in A ⟼ B) \in V$
37	3 36	eqeltrid	$⊢ φ \to C \in V$
38		id	$⊢ c = C \to c = C$
39	38	raleqdv	$⊢ c = C \to (\forall x \in c \exists j \in A x \in B \leftrightarrow \forall x \in C \exists j \in A x \in B)$
40	38	feq2d	$⊢ c = C \to (f : c ⟶ A \leftrightarrow f : C ⟶ A)$
41	38	raleqdv	$⊢ c = C \to (\forall x \in c x \in D \leftrightarrow \forall x \in C x \in D)$
42	40 41	anbi12d	$⊢ c = C \to ((f : c ⟶ A \land \forall x \in c x \in D) \leftrightarrow (f : C ⟶ A \land \forall x \in C x \in D))$
43	42	exbidv	$⊢ c = C \to (\exists f (f : c ⟶ A \land \forall x \in c x \in D) \leftrightarrow \exists f (f : C ⟶ A \land \forall x \in C x \in D))$
44	39 43	imbi12d	$⊢ c = C \to ((\forall x \in c \exists j \in A x \in B \to \exists f (f : c ⟶ A \land \forall x \in c x \in D)) \leftrightarrow (\forall x \in C \exists j \in A x \in B \to \exists f (f : C ⟶ A \land \forall x \in C x \in D)))$
45		vex	$⊢ c \in V$
46	4	eleq2d	$⊢ j = f (x) \to (x \in B \leftrightarrow x \in D)$
47	45 46	ac6s	$⊢ \forall x \in c \exists j \in A x \in B \to \exists f (f : c ⟶ A \land \forall x \in c x \in D)$
48	44 47	vtoclg	$⊢ C \in V \to (\forall x \in C \exists j \in A x \in B \to \exists f (f : C ⟶ A \land \forall x \in C x \in D))$
49	37 48	syl	$⊢ φ \to (\forall x \in C \exists j \in A x \in B \to \exists f (f : C ⟶ A \land \forall x \in C x \in D))$
50	32 49	mpd	$⊢ φ \to \exists f (f : C ⟶ A \land \forall x \in C x \in D)$

Metamath Proof Explorer

Theorem acunirnmpt2

Proof