Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	acunirnmpt.1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
	aciunf1lem.a	⊢ Ⅎ 𝑗 𝐴
	acunirnmpt2f.c	⊢ Ⅎ 𝑗 𝐶
	acunirnmpt2f.d	⊢ Ⅎ 𝑗 𝐷
	acunirnmpt2f.2	⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵
	acunirnmpt2f.3	⊢ ( 𝑗 = ( 𝑓 ‘ 𝑥 ) → 𝐵 = 𝐷 )
	acunirnmpt2f.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
Assertion	acunirnmpt2f	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		acunirnmpt.0	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		acunirnmpt.1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
3		aciunf1lem.a	⊢ Ⅎ 𝑗 𝐴
4		acunirnmpt2f.c	⊢ Ⅎ 𝑗 𝐶
5		acunirnmpt2f.d	⊢ Ⅎ 𝑗 𝐷
6		acunirnmpt2f.2	⊢ 𝐶 = ∪ 𝑗 ∈ 𝐴 𝐵
7		acunirnmpt2f.3	⊢ ( 𝑗 = ( 𝑓 ‘ 𝑥 ) → 𝐵 = 𝐷 )
8		acunirnmpt2f.4	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
9	8	ralrimiva	⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ 𝑊 )
10		dfiun3g	⊢ ( ∀ 𝑗 ∈ 𝐴 𝐵 ∈ 𝑊 → ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
11	9 10	syl	⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
12	6 11	eqtrid	⊢ ( 𝜑 → 𝐶 = ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
13	3	mptexgf	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
14		rnexg	⊢ ( ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
15		uniexg	⊢ ( ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
16	1 13 14 15	4syl	⊢ ( 𝜑 → ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
17	12 16	eqeltrd	⊢ ( 𝜑 → 𝐶 ∈ V )
18	17 1	jca	⊢ ( 𝜑 → ( 𝐶 ∈ V ∧ 𝐴 ∈ 𝑉 ) )
19		eqid	⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
20		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
21	19 20	elrnmpt2d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
22		nfv	⊢ Ⅎ 𝑗 𝜑
23	4	nfcri	⊢ Ⅎ 𝑗 𝑥 ∈ 𝐶
24	22 23	nfan	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ 𝐶 )
25		nfmpt1	⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
26	25	nfrn	⊢ Ⅎ 𝑗 ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
27	26	nfcri	⊢ Ⅎ 𝑗 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
28	24 27	nfan	⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
29		nfv	⊢ Ⅎ 𝑗 𝑥 ∈ 𝑦
30	28 29	nfan	⊢ Ⅎ 𝑗 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 )
31		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 )
32		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
33	31 32	eleqtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝐵 )
34	33	exp31	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑗 ∈ 𝐴 → ( 𝑦 = 𝐵 → 𝑥 ∈ 𝐵 ) ) )
35	30 34	reximdai	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
36	21 35	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
37	12	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) )
38	37	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
39		eluni2	⊢ ( 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) 𝑥 ∈ 𝑦 )
40	38 39	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) 𝑥 ∈ 𝑦 )
41	36 40	r19.29a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
42	41	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
43		nfcv	⊢ Ⅎ 𝑐 𝐴
44		nfv	⊢ Ⅎ 𝑐 𝑥 ∈ 𝐵
45		nfcsb1v	⊢ Ⅎ 𝑗 ⦋ 𝑐 / 𝑗 ⦌ 𝐵
46	45	nfcri	⊢ Ⅎ 𝑗 𝑥 ∈ ⦋ 𝑐 / 𝑗 ⦌ 𝐵
47		csbeq1a	⊢ ( 𝑗 = 𝑐 → 𝐵 = ⦋ 𝑐 / 𝑗 ⦌ 𝐵 )
48	47	eleq2d	⊢ ( 𝑗 = 𝑐 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ⦋ 𝑐 / 𝑗 ⦌ 𝐵 ) )
49	3 43 44 46 48	cbvrexfw	⊢ ( ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ⦋ 𝑐 / 𝑗 ⦌ 𝐵 )
50	49	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐶 ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ⦋ 𝑐 / 𝑗 ⦌ 𝐵 )
51		csbeq1	⊢ ( 𝑐 = ( 𝑓 ‘ 𝑥 ) → ⦋ 𝑐 / 𝑗 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 )
52		fvex	⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
53	52 5 7	csbief	⊢ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 = 𝐷
54	51 53	eqtrdi	⊢ ( 𝑐 = ( 𝑓 ‘ 𝑥 ) → ⦋ 𝑐 / 𝑗 ⦌ 𝐵 = 𝐷 )
55	54	eleq2d	⊢ ( 𝑐 = ( 𝑓 ‘ 𝑥 ) → ( 𝑥 ∈ ⦋ 𝑐 / 𝑗 ⦌ 𝐵 ↔ 𝑥 ∈ 𝐷 ) )
56	55	ac6	⊢ ( ( 𝐶 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ⦋ 𝑐 / 𝑗 ⦌ 𝐵 ) → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )
57	56	3expia	⊢ ( ( 𝐶 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑐 ∈ 𝐴 𝑥 ∈ ⦋ 𝑐 / 𝑗 ⦌ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
58	50 57	biimtrid	⊢ ( ( 𝐶 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
59	18 42 58	sylc	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )