acunirnmpt2f

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$
	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		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)$
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	sylib	$⊢ (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y) \to \exists j \in A y = B$
15		nfv	$⊢ Ⅎ j φ$
16	4	nfcri	$⊢ Ⅎ j x \in C$
17	15 16	nfan	$⊢ Ⅎ j (φ \land x \in C)$
18		nfcv	$⊢ \underline{Ⅎ} j y$
19		nfmpt1	$⊢ \underline{Ⅎ} j (j \in A ⟼ B)$
20	19	nfrn	$⊢ \underline{Ⅎ} j ran (j \in A ⟼ B)$
21	18 20	nfel	$⊢ Ⅎ j y \in ran (j \in A ⟼ B)$
22	17 21	nfan	$⊢ Ⅎ j ((φ \land x \in C) \land y \in ran (j \in A ⟼ B))$
23		nfv	$⊢ Ⅎ j x \in y$
24	22 23	nfan	$⊢ Ⅎ j (((φ \land x \in C) \land y \in ran (j \in A ⟼ B)) \land x \in y)$
25		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$
26		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$
27	25 26	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$
28	27	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)$
29	28	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))$
30	24 29	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)$
31	14 30	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$
32	8	ralrimiva	$⊢ φ \to \forall j \in A B \in W$
33		dfiun3g	$⊢ \forall j \in A B \in W \to ⋃_{j \in A} B = ⋃ ran (j \in A ⟼ B)$
34	32 33	syl	$⊢ φ \to ⋃_{j \in A} B = ⋃ ran (j \in A ⟼ B)$
35	6 34	syl5eq	$⊢ φ \to C = ⋃ ran (j \in A ⟼ B)$
36	35	eleq2d	$⊢ φ \to (x \in C \leftrightarrow x \in ⋃ ran (j \in A ⟼ B))$
37	36	biimpa	$⊢ (φ \land x \in C) \to x \in ⋃ ran (j \in A ⟼ B)$
38		eluni2	$⊢ x \in ⋃ ran (j \in A ⟼ B) \leftrightarrow \exists y \in ran (j \in A ⟼ B) x \in y$
39	37 38	sylib	$⊢ (φ \land x \in C) \to \exists y \in ran (j \in A ⟼ B) x \in y$
40	31 39	r19.29a	$⊢ (φ \land x \in C) \to \exists j \in A x \in B$
41	40	ralrimiva	$⊢ φ \to \forall x \in C \exists j \in A x \in B$
42		nfcv	$⊢ \underline{Ⅎ} k A$
43		nfcv	$⊢ \underline{Ⅎ} k B$
44		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ k / j ⦌ B$
45		csbeq1a	$⊢ j = k \to B = ⦋ k / j ⦌ B$
46	3 42 43 44 45	cbvmptf	$⊢ (j \in A ⟼ B) = (k \in A ⟼ ⦋ k / j ⦌ B)$
47		mptexg	$⊢ A \in V \to (k \in A ⟼ ⦋ k / j ⦌ B) \in V$
48	46 47	eqeltrid	$⊢ A \in V \to (j \in A ⟼ B) \in V$
49		rnexg	$⊢ (j \in A ⟼ B) \in V \to ran (j \in A ⟼ B) \in V$
50		uniexg	$⊢ ran (j \in A ⟼ B) \in V \to ⋃ ran (j \in A ⟼ B) \in V$
51	1 48 49 50	4syl	$⊢ φ \to ⋃ ran (j \in A ⟼ B) \in V$
52	35 51	eqeltrd	$⊢ φ \to C \in V$
53		id	$⊢ c = C \to c = C$
54	53	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)$
55	53	feq2d	$⊢ c = C \to (f : c ⟶ A \leftrightarrow f : C ⟶ A)$
56	53	raleqdv	$⊢ c = C \to (\forall x \in c x \in D \leftrightarrow \forall x \in C x \in D)$
57	55 56	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))$
58	57	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))$
59	54 58	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)))$
60	5	nfcri	$⊢ Ⅎ j x \in D$
61		vex	$⊢ c \in V$
62	7	eleq2d	$⊢ j = f (x) \to (x \in B \leftrightarrow x \in D)$
63	3 60 61 62	ac6sf2	$⊢ \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)$
64	59 63	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))$
65	52 64	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))$
66	41 65	mpd	$⊢ φ \to \exists f (f : C ⟶ A \land \forall x \in C x \in D)$

Metamath Proof Explorer

Theorem acunirnmpt2f

Proof