acunirnmpt2

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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	acunirnmpt.1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
	acunirnmpt2.2	⊢ 𝐶 = ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
	acunirnmpt2.3	⊢ ( 𝑗 = ( 𝑓 ‘ 𝑥 ) → 𝐵 = 𝐷 )
Assertion	acunirnmpt2	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		acunirnmpt.0	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		acunirnmpt.1	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
3		acunirnmpt2.2	⊢ 𝐶 = ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
4		acunirnmpt2.3	⊢ ( 𝑗 = ( 𝑓 ‘ 𝑥 ) → 𝐵 = 𝐷 )
5		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
6		vex	⊢ 𝑦 ∈ V
7		eqid	⊢ ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
8	7	elrnmpt	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 ) )
9	6 8	ax-mp	⊢ ( 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
10	5 9	sylib	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 )
11		nfv	⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ 𝐶 )
12		nfcv	⊢ Ⅎ 𝑗 𝑦
13		nfmpt1	⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
14	13	nfrn	⊢ Ⅎ 𝑗 ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
15	12 14	nfel	⊢ Ⅎ 𝑗 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 )
16	11 15	nfan	⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
17		nfv	⊢ Ⅎ 𝑗 𝑥 ∈ 𝑦
18	16 17	nfan	⊢ Ⅎ 𝑗 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 )
19		simpllr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝑦 )
20		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
21	19 20	eleqtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝐵 )
22	21	ex	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑦 = 𝐵 → 𝑥 ∈ 𝐵 ) )
23	22	ex	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ( 𝑗 ∈ 𝐴 → ( 𝑦 = 𝐵 → 𝑥 ∈ 𝐵 ) ) )
24	18 23	reximdai	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ( ∃ 𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
25	10 24	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
26	3	eleq2i	⊢ ( 𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
27	26	biimpi	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) )
28		eluni2	⊢ ( 𝑥 ∈ ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) 𝑥 ∈ 𝑦 )
29	27 28	sylib	⊢ ( 𝑥 ∈ 𝐶 → ∃ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) 𝑥 ∈ 𝑦 )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑦 ∈ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) 𝑥 ∈ 𝑦 )
31	25 30	r19.29a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
32	31	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
33		mptexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
34		rnexg	⊢ ( ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
35		uniexg	⊢ ( ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
36	1 33 34 35	4syl	⊢ ( 𝜑 → ∪ ran ( 𝑗 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
37	3 36	eqeltrid	⊢ ( 𝜑 → 𝐶 ∈ V )
38		id	⊢ ( 𝑐 = 𝐶 → 𝑐 = 𝐶 )
39	38	raleqdv	⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑥 ∈ 𝑐 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
40	38	feq2d	⊢ ( 𝑐 = 𝐶 → ( 𝑓 : 𝑐 ⟶ 𝐴 ↔ 𝑓 : 𝐶 ⟶ 𝐴 ) )
41	38	raleqdv	⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ↔ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )
42	40 41	anbi12d	⊢ ( 𝑐 = 𝐶 → ( ( 𝑓 : 𝑐 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ) ↔ ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
43	42	exbidv	⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ) ↔ ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
44	39 43	imbi12d	⊢ ( 𝑐 = 𝐶 → ( ( ∀ 𝑥 ∈ 𝑐 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ) ) ↔ ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) ) )
45		vex	⊢ 𝑐 ∈ V
46	4	eleq2d	⊢ ( 𝑗 = ( 𝑓 ‘ 𝑥 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐷 ) )
47	45 46	ac6s	⊢ ( ∀ 𝑥 ∈ 𝑐 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝑐 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ) )
48	44 47	vtoclg	⊢ ( 𝐶 ∈ V → ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
49	37 48	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐶 ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) ) )
50	32 49	mpd	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐶 𝑥 ∈ 𝐷 ) )

Metamath Proof Explorer

Theorem acunirnmpt2

Proof