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	biimpi	$⊢ y \in C \to \exists j \in A y = B$
16	15	adantl	$⊢ (φ \land y \in C) \to \exists j \in A y = B$
17	8 16	r19.29a	$⊢ (φ \land y \in C) \to y \neq \emptyset$
18	17	ralrimiva	$⊢ φ \to \forall y \in C y \neq \emptyset$
19		mptexg	$⊢ A \in V \to (j \in A ⟼ B) \in V$
20		rnexg	$⊢ (j \in A ⟼ B) \in V \to ran (j \in A ⟼ B) \in V$
21	1 19 20	3syl	$⊢ φ \to ran (j \in A ⟼ B) \in V$
22	3 21	eqeltrid	$⊢ φ \to C \in V$
23		raleq	$⊢ c = C \to (\forall y \in c y \neq \emptyset \leftrightarrow \forall y \in C y \neq \emptyset)$
24		id	$⊢ c = C \to c = C$
25		unieq	$⊢ c = C \to ⋃ c = ⋃ C$
26	24 25	feq23d	$⊢ c = C \to (f : c ⟶ ⋃ c \leftrightarrow f : C ⟶ ⋃ C)$
27		raleq	$⊢ c = C \to (\forall y \in c f (y) \in y \leftrightarrow \forall y \in C f (y) \in y)$
28	26 27	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))$
29	28	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))$
30	23 29	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)))$
31		vex	$⊢ c \in V$
32	31	ac5b	$⊢ \forall y \in c y \neq \emptyset \to \exists f (f : c ⟶ ⋃ c \land \forall y \in c f (y) \in y)$
33	30 32	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))$
34	22 33	syl	$⊢ φ \to (\forall y \in C y \neq \emptyset \to \exists f (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y))$
35	18 34	mpd	$⊢ φ \to \exists f (f : C ⟶ ⋃ C \land \forall y \in C f (y) \in y)$
36	16	adantr	$⊢ ((φ \land y \in C) \land f (y) \in y) \to \exists j \in A y = B$
37		simpllr	$⊢ ((((φ \land y \in C) \land f (y) \in y) \land j \in A) \land y = B) \to f (y) \in y$
38		simpr	$⊢ ((((φ \land y \in C) \land f (y) \in y) \land j \in A) \land y = B) \to y = B$
39	37 38	eleqtrd	$⊢ ((((φ \land y \in C) \land f (y) \in y) \land j \in A) \land y = B) \to f (y) \in B$
40	39	ex	$⊢ (((φ \land y \in C) \land f (y) \in y) \land j \in A) \to (y = B \to f (y) \in B)$
41	40	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)$
42	36 41	mpd	$⊢ ((φ \land y \in C) \land f (y) \in y) \to \exists j \in A f (y) \in B$
43	42	ex	$⊢ (φ \land y \in C) \to (f (y) \in y \to \exists j \in A f (y) \in B)$
44	43	ralimdva	$⊢ φ \to (\forall y \in C f (y) \in y \to \forall y \in C \exists j \in A f (y) \in B)$
45	44	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))$
46	45	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))$
47	35 46	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