Theorem 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	|- ( ph -> A e. V )
	acunirnmpt.1	|- ( ( ph /\ j e. A ) -> B =/= (/) )
	acunirnmpt.2	|- C = ran ( j e. A |-> B )
Assertion	acunirnmpt	|- ( ph -> E. f ( f : C --> U. C /\ A. y e. C E. j e. A ( f ` y ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		acunirnmpt.0	|- ( ph -> A e. V )
2		acunirnmpt.1	|- ( ( ph /\ j e. A ) -> B =/= (/) )
3		acunirnmpt.2	|- C = ran ( j e. A |-> B )
4		simpr	|- ( ( ( ( ph /\ y e. C ) /\ j e. A ) /\ y = B ) -> y = B )
5		simplll	|- ( ( ( ( ph /\ y e. C ) /\ j e. A ) /\ y = B ) -> ph )
6		simplr	|- ( ( ( ( ph /\ y e. C ) /\ j e. A ) /\ y = B ) -> j e. A )
7	5 6 2	syl2anc	|- ( ( ( ( ph /\ y e. C ) /\ j e. A ) /\ y = B ) -> B =/= (/) )
8	4 7	eqnetrd	|- ( ( ( ( ph /\ y e. C ) /\ j e. A ) /\ y = B ) -> y =/= (/) )
9	3	eleq2i	|- ( y e. C <-> y e. ran ( j e. A |-> B ) )
10		vex	|- y e. _V
11		eqid	|- ( j e. A |-> B ) = ( j e. A |-> B )
12	11	elrnmpt	|- ( y e. _V -> ( y e. ran ( j e. A |-> B ) <-> E. j e. A y = B ) )
13	10 12	ax-mp	|- ( y e. ran ( j e. A |-> B ) <-> E. j e. A y = B )
14	9 13	bitri	|- ( y e. C <-> E. j e. A y = B )
15	14	biimpi	|- ( y e. C -> E. j e. A y = B )
16	15	adantl	|- ( ( ph /\ y e. C ) -> E. j e. A y = B )
17	8 16	r19.29a	|- ( ( ph /\ y e. C ) -> y =/= (/) )
18	17	ralrimiva	|- ( ph -> A. y e. C y =/= (/) )
19		mptexg	|- ( A e. V -> ( j e. A |-> B ) e. _V )
20		rnexg	|- ( ( j e. A |-> B ) e. _V -> ran ( j e. A |-> B ) e. _V )
21	1 19 20	3syl	|- ( ph -> ran ( j e. A |-> B ) e. _V )
22	3 21	eqeltrid	|- ( ph -> C e. _V )
23		raleq	|- ( c = C -> ( A. y e. c y =/= (/) <-> A. y e. C y =/= (/) ) )
24		id	|- ( c = C -> c = C )
25		unieq	|- ( c = C -> U. c = U. C )
26	24 25	feq23d	|- ( c = C -> ( f : c --> U. c <-> f : C --> U. C ) )
27		raleq	|- ( c = C -> ( A. y e. c ( f ` y ) e. y <-> A. y e. C ( f ` y ) e. y ) )
28	26 27	anbi12d	|- ( c = C -> ( ( f : c --> U. c /\ A. y e. c ( f ` y ) e. y ) <-> ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) ) )
29	28	exbidv	|- ( c = C -> ( E. f ( f : c --> U. c /\ A. y e. c ( f ` y ) e. y ) <-> E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) ) )
30	23 29	imbi12d	|- ( c = C -> ( ( A. y e. c y =/= (/) -> E. f ( f : c --> U. c /\ A. y e. c ( f ` y ) e. y ) ) <-> ( A. y e. C y =/= (/) -> E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) ) ) )
31		vex	|- c e. _V
32	31	ac5b	|- ( A. y e. c y =/= (/) -> E. f ( f : c --> U. c /\ A. y e. c ( f ` y ) e. y ) )
33	30 32	vtoclg	|- ( C e. _V -> ( A. y e. C y =/= (/) -> E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) ) )
34	22 33	syl	|- ( ph -> ( A. y e. C y =/= (/) -> E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) ) )
35	18 34	mpd	|- ( ph -> E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) )
36	16	adantr	|- ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) -> E. j e. A y = B )
37		simpllr	|- ( ( ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) /\ j e. A ) /\ y = B ) -> ( f ` y ) e. y )
38		simpr	|- ( ( ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) /\ j e. A ) /\ y = B ) -> y = B )
39	37 38	eleqtrd	|- ( ( ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) /\ j e. A ) /\ y = B ) -> ( f ` y ) e. B )
40	39	ex	|- ( ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) /\ j e. A ) -> ( y = B -> ( f ` y ) e. B ) )
41	40	reximdva	|- ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) -> ( E. j e. A y = B -> E. j e. A ( f ` y ) e. B ) )
42	36 41	mpd	|- ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) -> E. j e. A ( f ` y ) e. B )
43	42	ex	|- ( ( ph /\ y e. C ) -> ( ( f ` y ) e. y -> E. j e. A ( f ` y ) e. B ) )
44	43	ralimdva	|- ( ph -> ( A. y e. C ( f ` y ) e. y -> A. y e. C E. j e. A ( f ` y ) e. B ) )
45	44	anim2d	|- ( ph -> ( ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) -> ( f : C --> U. C /\ A. y e. C E. j e. A ( f ` y ) e. B ) ) )
46	45	eximdv	|- ( ph -> ( E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) -> E. f ( f : C --> U. C /\ A. y e. C E. j e. A ( f ` y ) e. B ) ) )
47	35 46	mpd	|- ( ph -> E. f ( f : C --> U. C /\ A. y e. C E. j e. A ( f ` y ) e. B ) )