acunirnmpt2

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$
	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		mptexg	$⊢ A \in V \to (j \in A ⟼ B) \in V$
6		rnexg	$⊢ (j \in A ⟼ B) \in V \to ran (j \in A ⟼ B) \in V$
7		uniexg	$⊢ ran (j \in A ⟼ B) \in V \to ⋃ ran (j \in A ⟼ B) \in V$
8	1 5 6 7	4syl	$⊢ φ \to ⋃ ran (j \in A ⟼ B) \in V$
9	3 8	eqeltrid	$⊢ φ \to C \in V$
10		eqid	$⊢ (j \in A ⟼ B) = (j \in A ⟼ B)$
11		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)$
12	10 11	elrnmpt2d	$⊢ (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \to \exists j \in A y = B$
13		nfv	$⊢ Ⅎ j (φ \land x \in C)$
14		nfmpt1	$⊢ \underline{Ⅎ} j (j \in A ⟼ B)$
15	14	nfrn	$⊢ \underline{Ⅎ} j ran (j \in A ⟼ B)$
16	15	nfcri	$⊢ Ⅎ j y \in ran (j \in A ⟼ B)$
17	13 16	nfan	$⊢ Ⅎ j ((φ \land x \in C) \land y \in ran (j \in A ⟼ B))$
18		nfv	$⊢ Ⅎ j x \in y$
19	17 18	nfan	$⊢ Ⅎ j (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y)$
20		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$
21		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$
22	20 21	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$
23	22	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))$
24	19 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	12 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		eluni2	$⊢ x \in ⋃ ran (j \in A ⟼ B) \leftrightarrow \exists y \in ran (j \in A ⟼ B) x \in y$
28	26 27	sylbb	$⊢ x \in C \to \exists y \in ran (j \in A ⟼ B) x \in y$
29	28	adantl	$⊢ (φ \land x \in C) \to \exists y \in ran (j \in A ⟼ B) x \in y$
30	25 29	r19.29a	$⊢ (φ \land x \in C) \to \exists j \in A x \in B$
31	30	ralrimiva	$⊢ φ \to \forall x \in C \exists j \in A x \in B$
32	4	eleq2d	$⊢ j = f (x) \to (x \in B \leftrightarrow x \in D)$
33	32	ac6	$⊢ (C \in V \land A \in V \land \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)$
34	9 1 31 33	syl3anc	$⊢ φ \to \exists f (f : C ⟶ A \land \forall x \in C x \in D)$

Metamath Proof Explorer

Theorem acunirnmpt2

Proof