Metamath Proof Explorer

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 
|- ( ph -> A e. V )
acunirnmpt.1 
|- ( ( ph /\ j e. A ) -> B =/= (/) )
aciunf1lem.a 
|- F/_ j A
acunirnmpt2f.c 
|- F/_ j C
acunirnmpt2f.d 
|- F/_ j D
acunirnmpt2f.2 
|- C = U_ j e. A B
acunirnmpt2f.3 
|- ( j = ( f ` x ) -> B = D )
acunirnmpt2f.4 
|- ( ( ph /\ j e. A ) -> B e. W )
Assertion acunirnmpt2f 
|- ( ph -> E. f ( f : C --> A /\ A. x e. C x e. D ) )

Proof

Step Hyp Ref Expression
1 acunirnmpt.0 
 |-  ( ph -> A e. V )
2 acunirnmpt.1 
 |-  ( ( ph /\ j e. A ) -> B =/= (/) )
3 aciunf1lem.a 
 |-  F/_ j A
4 acunirnmpt2f.c 
 |-  F/_ j C
5 acunirnmpt2f.d 
 |-  F/_ j D
6 acunirnmpt2f.2 
 |-  C = U_ j e. A B
7 acunirnmpt2f.3 
 |-  ( j = ( f ` x ) -> B = D )
8 acunirnmpt2f.4 
 |-  ( ( ph /\ j e. A ) -> B e. W )
9 8 ralrimiva 
 |-  ( ph -> A. j e. A B e. W )
10 dfiun3g 
 |-  ( A. j e. A B e. W -> U_ j e. A B = U. ran ( j e. A |-> B ) )
11 9 10 syl 
 |-  ( ph -> U_ j e. A B = U. ran ( j e. A |-> B ) )
12 6 11 eqtrid 
 |-  ( ph -> C = U. ran ( j e. A |-> B ) )
13 3 mptexgf 
 |-  ( A e. V -> ( j e. A |-> B ) e. _V )
14 rnexg 
 |-  ( ( j e. A |-> B ) e. _V -> ran ( j e. A |-> B ) e. _V )
15 uniexg 
 |-  ( ran ( j e. A |-> B ) e. _V -> U. ran ( j e. A |-> B ) e. _V )
16 1 13 14 15 4syl 
 |-  ( ph -> U. ran ( j e. A |-> B ) e. _V )
17 12 16 eqeltrd 
 |-  ( ph -> C e. _V )
18 17 1 jca 
 |-  ( ph -> ( C e. _V /\ A e. V ) )
19 eqid 
 |-  ( j e. A |-> B ) = ( j e. A |-> B )
20 simplr 
 |-  ( ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y ) -> y e. ran ( j e. A |-> B ) )
21 19 20 elrnmpt2d 
 |-  ( ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y ) -> E. j e. A y = B )
22 nfv 
 |-  F/ j ph
23 4 nfcri 
 |-  F/ j x e. C
24 22 23 nfan 
 |-  F/ j ( ph /\ x e. C )
25 nfmpt1 
 |-  F/_ j ( j e. A |-> B )
26 25 nfrn 
 |-  F/_ j ran ( j e. A |-> B )
27 26 nfcri 
 |-  F/ j y e. ran ( j e. A |-> B )
28 24 27 nfan 
 |-  F/ j ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) )
29 nfv 
 |-  F/ j x e. y
30 28 29 nfan 
 |-  F/ j ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y )
31 simpllr 
 |-  ( ( ( ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y ) /\ j e. A ) /\ y = B ) -> x e. y )
32 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y ) /\ j e. A ) /\ y = B ) -> y = B )
33 31 32 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y ) /\ j e. A ) /\ y = B ) -> x e. B )
34 33 exp31 
 |-  ( ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y ) -> ( j e. A -> ( y = B -> x e. B ) ) )
35 30 34 reximdai 
 |-  ( ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y ) -> ( E. j e. A y = B -> E. j e. A x e. B ) )
36 21 35 mpd 
 |-  ( ( ( ( ph /\ x e. C ) /\ y e. ran ( j e. A |-> B ) ) /\ x e. y ) -> E. j e. A x e. B )
37 12 eleq2d 
 |-  ( ph -> ( x e. C <-> x e. U. ran ( j e. A |-> B ) ) )
38 37 biimpa 
 |-  ( ( ph /\ x e. C ) -> x e. U. ran ( j e. A |-> B ) )
39 eluni2 
 |-  ( x e. U. ran ( j e. A |-> B ) <-> E. y e. ran ( j e. A |-> B ) x e. y )
40 38 39 sylib 
 |-  ( ( ph /\ x e. C ) -> E. y e. ran ( j e. A |-> B ) x e. y )
41 36 40 r19.29a 
 |-  ( ( ph /\ x e. C ) -> E. j e. A x e. B )
42 41 ralrimiva 
 |-  ( ph -> A. x e. C E. j e. A x e. B )
43 nfcv 
 |-  F/_ c A
44 nfv 
 |-  F/ c x e. B
45 nfcsb1v 
 |-  F/_ j [_ c / j ]_ B
46 45 nfcri 
 |-  F/ j x e. [_ c / j ]_ B
47 csbeq1a 
 |-  ( j = c -> B = [_ c / j ]_ B )
48 47 eleq2d 
 |-  ( j = c -> ( x e. B <-> x e. [_ c / j ]_ B ) )
49 3 43 44 46 48 cbvrexfw 
 |-  ( E. j e. A x e. B <-> E. c e. A x e. [_ c / j ]_ B )
50 49 ralbii 
 |-  ( A. x e. C E. j e. A x e. B <-> A. x e. C E. c e. A x e. [_ c / j ]_ B )
51 csbeq1 
 |-  ( c = ( f ` x ) -> [_ c / j ]_ B = [_ ( f ` x ) / j ]_ B )
52 fvex 
 |-  ( f ` x ) e. _V
53 52 5 7 csbief 
 |-  [_ ( f ` x ) / j ]_ B = D
54 51 53 eqtrdi 
 |-  ( c = ( f ` x ) -> [_ c / j ]_ B = D )
55 54 eleq2d 
 |-  ( c = ( f ` x ) -> ( x e. [_ c / j ]_ B <-> x e. D ) )
56 55 ac6 
 |-  ( ( C e. _V /\ A e. V /\ A. x e. C E. c e. A x e. [_ c / j ]_ B ) -> E. f ( f : C --> A /\ A. x e. C x e. D ) )
57 56 3expia 
 |-  ( ( C e. _V /\ A e. V ) -> ( A. x e. C E. c e. A x e. [_ c / j ]_ B -> E. f ( f : C --> A /\ A. x e. C x e. D ) ) )
58 50 57 biimtrid 
 |-  ( ( C e. _V /\ A e. V ) -> ( A. x e. C E. j e. A x e. B -> E. f ( f : C --> A /\ A. x e. C x e. D ) ) )
59 18 42 58 sylc 
 |-  ( ph -> E. f ( f : C --> A /\ A. x e. C x e. D ) )