acunirnmpt

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

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

Proof

Step	Hyp	Ref	Expression
1		acunirnmpt.0	$⊢ φ \to A \in V$
2		acunirnmpt.1	$⊢ (φ \land j \in A) \to B \neq \emptyset$
3		acunirnmpt.2	$⊢ C = ran (j \in A ⟼ B)$
4		simpr	$⊢ (((φ \land y \in C) \land j \in A) \land y = B) \to y = B$
5		simplll	$⊢ (((φ \land y \in C) \land j \in A) \land y = B) \to φ$
6		simplr	$⊢ (((φ \land y \in C) \land j \in A) \land y = B) \to j \in A$
7	5 6 2	syl2anc	$⊢ (((φ \land y \in C) \land j \in A) \land y = B) \to B \neq \emptyset$
8	4 7	eqnetrd	$⊢ (((φ \land y \in C) \land j \in A) \land y = B) \to y \neq \emptyset$
9	3	eleq2i	$⊢ y \in C \leftrightarrow y \in ran (j \in A ⟼ B)$
10		vex	$⊢ y \in V$
11		eqid	$⊢ (j \in A ⟼ B) = (j \in A ⟼ B)$
12	11	elrnmpt	$⊢ y \in V \to (y \in ran (j \in A ⟼ B) \leftrightarrow \exists j \in A y = B)$
13	10 12	ax-mp	$⊢ y \in ran (j \in A ⟼ B) \leftrightarrow \exists j \in A y = B$
14	9 13	bitri	$⊢ y \in C \leftrightarrow \exists j \in A y = B$
15	14	bilani	$⊢ (φ \land y \in C) \to \exists j \in A y = B$
16	8 15	r19.29a	$⊢ (φ \land y \in C) \to y \neq \emptyset$
17	16	ralrimiva	$⊢ φ \to \forall y \in C y \neq \emptyset$
18		mptexg	$⊢ A \in V \to (j \in A ⟼ B) \in V$
19		rnexg	$⊢ (j \in A ⟼ B) \in V \to ran (j \in A ⟼ B) \in V$
20	1 18 19	3syl	$⊢ φ \to ran (j \in A ⟼ B) \in V$
21	3 20	eqeltrid	$⊢ φ \to C \in V$
22		raleq	$⊢ c = C \to (\forall y \in c y \neq \emptyset \leftrightarrow \forall y \in C y \neq \emptyset)$
23		id	$⊢ c = C \to c = C$
24		unieq	$⊢ c = C \to ⋃ c = ⋃ C$
25	23 24	feq23d	$⊢ c = C \to (f : c ⟶ ⋃ c \leftrightarrow f : C ⟶ ⋃ C)$
26		raleq	$⊢ c = C \to (\forall y \in c f (y) \in y \leftrightarrow \forall y \in C f (y) \in y)$
27	25 26	anbi12d	$⊢ c = C \to ((f : c ⟶ ⋃ c \land \forall y \in c f (y) \in y) \leftrightarrow (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y))$
28	27	exbidv	$⊢ c = C \to (\exists f (f : c ⟶ ⋃ c \land \forall y \in c f (y) \in y) \leftrightarrow \exists f (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y))$
29	22 28	imbi12d	$⊢ c = C \to ((\forall y \in c y \neq \emptyset \to \exists f (f : c ⟶ ⋃ c \land \forall y \in c f (y) \in y)) \leftrightarrow (\forall y \in C y \neq \emptyset \to \exists f (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y)))$
30		vex	$⊢ c \in V$
31	30	ac5b	$⊢ \forall y \in c y \neq \emptyset \to \exists f (f : c ⟶ ⋃ c \land \forall y \in c f (y) \in y)$
32	29 31	vtoclg	$⊢ C \in V \to (\forall y \in C y \neq \emptyset \to \exists f (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y))$
33	21 32	syl	$⊢ φ \to (\forall y \in C y \neq \emptyset \to \exists f (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y))$
34	17 33	mpd	$⊢ φ \to \exists f (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y)$
35	15	adantr	$⊢ ((φ \land y \in C) \land f (y) \in y) \to \exists j \in A y = B$
36		simpllr	$⊢ ((((φ \land y \in C) \land f (y) \in y) \land j \in A) \land y = B) \to f (y) \in y$
37		simpr	$⊢ ((((φ \land y \in C) \land f (y) \in y) \land j \in A) \land y = B) \to y = B$
38	36 37	eleqtrd	$⊢ ((((φ \land y \in C) \land f (y) \in y) \land j \in A) \land y = B) \to f (y) \in B$
39	38	ex	$⊢ (((φ \land y \in C) \land f (y) \in y) \land j \in A) \to (y = B \to f (y) \in B)$
40	39	reximdva	$⊢ ((φ \land y \in C) \land f (y) \in y) \to (\exists j \in A y = B \to \exists j \in A f (y) \in B)$
41	35 40	mpd	$⊢ ((φ \land y \in C) \land f (y) \in y) \to \exists j \in A f (y) \in B$
42	41	ex	$⊢ (φ \land y \in C) \to (f (y) \in y \to \exists j \in A f (y) \in B)$
43	42	ralimdva	$⊢ φ \to (\forall y \in C f (y) \in y \to \forall y \in C \exists j \in A f (y) \in B)$
44	43	anim2d	$⊢ φ \to ((f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y) \to (f : C ⟶ ⋃ C \land \forall y \in C \exists j \in A f (y) \in B))$
45	44	eximdv	$⊢ φ \to (\exists f (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y) \to \exists f (f : C ⟶ ⋃ C \land \forall y \in C \exists j \in A f (y) \in B))$
46	34 45	mpd	$⊢ φ \to \exists f (f : C ⟶ ⋃ C \land \forall y \in C \exists j \in A f (y) \in B)$

Metamath Proof Explorer

Theorem acunirnmpt

Proof