This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )