acunirnmpt2f

Description: Axiom of choice for the union of the range of a mapping to function. (Contributed by Thierry Arnoux, 7-Nov-2019) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

	Ref	Expression
Hypotheses	acunirnmpt.0	$⊢ φ \to A \in V$
	acunirnmpt.1	$⊢ (φ \land j \in A) \to B \neq \emptyset$
	aciunf1lem.a	$⊢ \underline{Ⅎ} j A$
	acunirnmpt2f.c	$⊢ \underline{Ⅎ} j C$
	acunirnmpt2f.d	$⊢ \underline{Ⅎ} j D$
	acunirnmpt2f.2	$⊢ C = ⋃_{j \in A} B$
	acunirnmpt2f.3	$⊢ j = f (x) \to B = D$
	acunirnmpt2f.4	$⊢ (φ \land j \in A) \to B \in W$
Assertion	acunirnmpt2f	$⊢ φ \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		aciunf1lem.a	$⊢ \underline{Ⅎ} j A$
4		acunirnmpt2f.c	$⊢ \underline{Ⅎ} j C$
5		acunirnmpt2f.d	$⊢ \underline{Ⅎ} j D$
6		acunirnmpt2f.2	$⊢ C = ⋃_{j \in A} B$
7		acunirnmpt2f.3	$⊢ j = f (x) \to B = D$
8		acunirnmpt2f.4	$⊢ (φ \land j \in A) \to B \in W$
9	8	ralrimiva	$⊢ φ \to \forall j \in A B \in W$
10		dfiun3g	$⊢ \forall j \in A B \in W \to ⋃_{j \in A} B = ⋃ ran (j \in A ⟼ B)$
11	9 10	syl	$⊢ φ \to ⋃_{j \in A} B = ⋃ ran (j \in A ⟼ B)$
12	6 11	eqtrid	$⊢ φ \to C = ⋃ ran (j \in A ⟼ B)$
13	3	mptexgf	$⊢ A \in V \to (j \in A ⟼ B) \in V$
14		rnexg	$⊢ (j \in A ⟼ B) \in V \to ran (j \in A ⟼ B) \in V$
15		uniexg	$⊢ ran (j \in A ⟼ B) \in V \to ⋃ ran (j \in A ⟼ B) \in V$
16	1 13 14 15	4syl	$⊢ φ \to ⋃ ran (j \in A ⟼ B) \in V$
17	12 16	eqeltrd	$⊢ φ \to C \in V$
18	17 1	jca	$⊢ φ \to (C \in V \land A \in V)$
19		eqid	$⊢ (j \in A ⟼ B) = (j \in A ⟼ B)$
20		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)$
21	19 20	elrnmpt2d	$⊢ (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \to \exists j \in A y = B$
22		nfv	$⊢ Ⅎ j φ$
23	4	nfcri	$⊢ Ⅎ j x \in C$
24	22 23	nfan	$⊢ Ⅎ j (φ \land x \in C)$
25		nfmpt1	$⊢ \underline{Ⅎ} j (j \in A ⟼ B)$
26	25	nfrn	$⊢ \underline{Ⅎ} j ran (j \in A ⟼ B)$
27	26	nfcri	$⊢ Ⅎ j y \in ran (j \in A ⟼ B)$
28	24 27	nfan	$⊢ Ⅎ j ((φ \land x \in C) \land y \in ran (j \in A ⟼ B))$
29		nfv	$⊢ Ⅎ j x \in y$
30	28 29	nfan	$⊢ Ⅎ j (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y)$
31		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$
32		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$
33	31 32	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$
34	33	exp31	$⊢ (((φ \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))$
35	30 34	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)$
36	21 35	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$
37	12	eleq2d	$⊢ φ \to (x \in C \leftrightarrow x \in ⋃ ran (j \in A ⟼ B))$
38	37	biimpa	$⊢ (φ \land x \in C) \to x \in ⋃ ran (j \in A ⟼ B)$
39		eluni2	$⊢ x \in ⋃ ran (j \in A ⟼ B) \leftrightarrow \exists y \in ran (j \in A ⟼ B) x \in y$
40	38 39	sylib	$⊢ (φ \land x \in C) \to \exists y \in ran (j \in A ⟼ B) x \in y$
41	36 40	r19.29a	$⊢ (φ \land x \in C) \to \exists j \in A x \in B$
42	41	ralrimiva	$⊢ φ \to \forall x \in C \exists j \in A x \in B$
43		nfcv	$⊢ \underline{Ⅎ} c A$
44		nfv	$⊢ Ⅎ c x \in B$
45		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ c / j ⦌ B$
46	45	nfcri	$⊢ Ⅎ j x \in ⦋ c / j ⦌ B$
47		csbeq1a	$⊢ j = c \to B = ⦋ c / j ⦌ B$
48	47	eleq2d	$⊢ j = c \to (x \in B \leftrightarrow x \in ⦋ c / j ⦌ B)$
49	3 43 44 46 48	cbvrexfw	$⊢ \exists j \in A x \in B \leftrightarrow \exists c \in A x \in ⦋ c / j ⦌ B$
50	49	ralbii	$⊢ \forall x \in C \exists j \in A x \in B \leftrightarrow \forall x \in C \exists c \in A x \in ⦋ c / j ⦌ B$
51		csbeq1	$⊢ c = f (x) \to ⦋ c / j ⦌ B = ⦋ f (x) / j ⦌ B$
52		fvex	$⊢ f (x) \in V$
53	52 5 7	csbief	$⊢ ⦋ f (x) / j ⦌ B = D$
54	51 53	eqtrdi	$⊢ c = f (x) \to ⦋ c / j ⦌ B = D$
55	54	eleq2d	$⊢ c = f (x) \to (x \in ⦋ c / j ⦌ B \leftrightarrow x \in D)$
56	55	ac6	$⊢ (C \in V \land A \in V \land \forall x \in C \exists c \in A x \in ⦋ c / j ⦌ B) \to \exists f (f : C ⟶ A \land \forall x \in C x \in D)$
57	56	3expia	$⊢ (C \in V \land A \in V) \to (\forall x \in C \exists c \in A x \in ⦋ c / j ⦌ B \to \exists f (f : C ⟶ A \land \forall x \in C x \in D))$
58	50 57	biimtrid	$⊢ (C \in V \land A \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))$
59	18 42 58	sylc	$⊢ φ \to \exists f (f : C ⟶ A \land \forall x \in C x \in D)$

Metamath Proof Explorer

Theorem acunirnmpt2f

Proof