Metamath Proof Explorer

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 bilani 
 |-  ( ( ph /\ y e. C ) -> E. j e. A y = B )
16 8 15 r19.29a 
 |-  ( ( ph /\ y e. C ) -> y =/= (/) )
17 16 ralrimiva 
 |-  ( ph -> A. y e. C y =/= (/) )
18 mptexg 
 |-  ( A e. V -> ( j e. A |-> B ) e. _V )
19 rnexg 
 |-  ( ( j e. A |-> B ) e. _V -> ran ( j e. A |-> B ) e. _V )
20 1 18 19 3syl 
 |-  ( ph -> ran ( j e. A |-> B ) e. _V )
21 3 20 eqeltrid 
 |-  ( ph -> C e. _V )
22 raleq 
 |-  ( c = C -> ( A. y e. c y =/= (/) <-> A. y e. C y =/= (/) ) )
23 id 
 |-  ( c = C -> c = C )
24 unieq 
 |-  ( c = C -> U. c = U. C )
25 23 24 feq23d 
 |-  ( c = C -> ( f : c --> U. c <-> f : C --> U. C ) )
26 raleq 
 |-  ( c = C -> ( A. y e. c ( f ` y ) e. y <-> A. y e. C ( f ` y ) e. y ) )
27 25 26 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 ) ) )
28 27 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 ) ) )
29 22 28 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 ) ) ) )
30 vex 
 |-  c e. _V
31 30 ac5b 
 |-  ( A. y e. c y =/= (/) -> E. f ( f : c --> U. c /\ A. y e. c ( f ` y ) e. y ) )
32 29 31 vtoclg 
 |-  ( C e. _V -> ( A. y e. C y =/= (/) -> E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) ) )
33 21 32 syl 
 |-  ( ph -> ( A. y e. C y =/= (/) -> E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) ) )
34 17 33 mpd 
 |-  ( ph -> E. f ( f : C --> U. C /\ A. y e. C ( f ` y ) e. y ) )
35 15 adantr 
 |-  ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) -> E. j e. A y = B )
36 simpllr 
 |-  ( ( ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) /\ j e. A ) /\ y = B ) -> ( f ` y ) e. y )
37 simpr 
 |-  ( ( ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) /\ j e. A ) /\ y = B ) -> y = B )
38 36 37 eleqtrd 
 |-  ( ( ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) /\ j e. A ) /\ y = B ) -> ( f ` y ) e. B )
39 38 ex 
 |-  ( ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) /\ j e. A ) -> ( y = B -> ( f ` y ) e. B ) )
40 39 reximdva 
 |-  ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) -> ( E. j e. A y = B -> E. j e. A ( f ` y ) e. B ) )
41 35 40 mpd 
 |-  ( ( ( ph /\ y e. C ) /\ ( f ` y ) e. y ) -> E. j e. A ( f ` y ) e. B )
42 41 ex 
 |-  ( ( ph /\ y e. C ) -> ( ( f ` y ) e. y -> E. j e. A ( f ` y ) e. B ) )
43 42 ralimdva 
 |-  ( ph -> ( A. y e. C ( f ` y ) e. y -> A. y e. C E. j e. A ( f ` y ) e. B ) )
44 43 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 ) ) )
45 44 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 ) ) )
46 34 45 mpd 
 |-  ( ph -> E. f ( f : C --> U. C /\ A. y e. C E. j e. A ( f ` y ) e. B ) )