Metamath Proof Explorer

Theorem aciunf1lem

Description: Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019)

Ref Expression
Hypotheses acunirnmpt.0 
|- ( ph -> A e. V )
acunirnmpt.1 
|- ( ( ph /\ j e. A ) -> B =/= (/) )
aciunf1lem.a 
|- F/_ j A
aciunf1lem.1 
|- ( ( ph /\ j e. A ) -> B e. W )
Assertion aciunf1lem 
|- ( ph -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( f ` x ) ) = x ) )

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 aciunf1lem.1 
 |-  ( ( ph /\ j e. A ) -> B e. W )
5 nfiu1 
 |-  F/_ j U_ j e. A B
6 nfcsb1v 
 |-  F/_ j [_ ( g ` x ) / j ]_ B
7 eqid 
 |-  U_ j e. A B = U_ j e. A B
8 csbeq1a 
 |-  ( j = ( g ` x ) -> B = [_ ( g ` x ) / j ]_ B )
9 1 2 3 5 6 7 8 4 acunirnmpt2f 
 |-  ( ph -> E. g ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) )
10 nfv 
 |-  F/ x ph
11 nfv 
 |-  F/ x g : U_ j e. A B --> A
12 nfra1 
 |-  F/ x A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B
13 11 12 nfan 
 |-  F/ x ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B )
14 10 13 nfan 
 |-  F/ x ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) )
15 nfv 
 |-  F/ j ph
16 nfcv 
 |-  F/_ j g
17 16 5 3 nff 
 |-  F/ j g : U_ j e. A B --> A
18 nfcv 
 |-  F/_ j x
19 18 6 nfel 
 |-  F/ j x e. [_ ( g ` x ) / j ]_ B
20 5 19 nfralw 
 |-  F/ j A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B
21 17 20 nfan 
 |-  F/ j ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B )
22 15 21 nfan 
 |-  F/ j ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) )
23 18 5 nfel 
 |-  F/ j x e. U_ j e. A B
24 22 23 nfan 
 |-  F/ j ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B )
25 nfcv 
 |-  F/_ j <. ( g ` x ) , x >.
26 nfiu1 
 |-  F/_ j U_ j e. A ( { j } X. B )
27 25 26 nfel 
 |-  F/ j <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B )
28 simplr 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) )
29 28 simpld 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> g : U_ j e. A B --> A )
30 29 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> g : U_ j e. A B --> A )
31 simpllr 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> x e. U_ j e. A B )
32 30 31 ffvelrnd 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> ( g ` x ) e. A )
33 fvex 
 |-  ( g ` x ) e. _V
34 33 snid 
 |-  ( g ` x ) e. { ( g ` x ) }
35 34 a1i 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> ( g ` x ) e. { ( g ` x ) } )
36 28 simprd 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B )
37 simpr 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> x e. U_ j e. A B )
38 rsp 
 |-  ( A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B -> ( x e. U_ j e. A B -> x e. [_ ( g ` x ) / j ]_ B ) )
39 36 37 38 sylc 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> x e. [_ ( g ` x ) / j ]_ B )
40 39 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> x e. [_ ( g ` x ) / j ]_ B )
41 35 40 jca 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> ( ( g ` x ) e. { ( g ` x ) } /\ x e. [_ ( g ` x ) / j ]_ B ) )
42 opelxp 
 |-  ( <. ( g ` x ) , x >. e. ( { ( g ` x ) } X. [_ ( g ` x ) / j ]_ B ) <-> ( ( g ` x ) e. { ( g ` x ) } /\ x e. [_ ( g ` x ) / j ]_ B ) )
43 41 42 sylibr 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> <. ( g ` x ) , x >. e. ( { ( g ` x ) } X. [_ ( g ` x ) / j ]_ B ) )
44 sneq 
 |-  ( k = ( g ` x ) -> { k } = { ( g ` x ) } )
45 csbeq1 
 |-  ( k = ( g ` x ) -> [_ k / j ]_ B = [_ ( g ` x ) / j ]_ B )
46 44 45 xpeq12d 
 |-  ( k = ( g ` x ) -> ( { k } X. [_ k / j ]_ B ) = ( { ( g ` x ) } X. [_ ( g ` x ) / j ]_ B ) )
47 46 eleq2d 
 |-  ( k = ( g ` x ) -> ( <. ( g ` x ) , x >. e. ( { k } X. [_ k / j ]_ B ) <-> <. ( g ` x ) , x >. e. ( { ( g ` x ) } X. [_ ( g ` x ) / j ]_ B ) ) )
48 47 rspcev 
 |-  ( ( ( g ` x ) e. A /\ <. ( g ` x ) , x >. e. ( { ( g ` x ) } X. [_ ( g ` x ) / j ]_ B ) ) -> E. k e. A <. ( g ` x ) , x >. e. ( { k } X. [_ k / j ]_ B ) )
49 32 43 48 syl2anc 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> E. k e. A <. ( g ` x ) , x >. e. ( { k } X. [_ k / j ]_ B ) )
50 eliun 
 |-  ( <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B ) <-> E. j e. A <. ( g ` x ) , x >. e. ( { j } X. B ) )
51 nfcv 
 |-  F/_ k A
52 nfv 
 |-  F/ k <. ( g ` x ) , x >. e. ( { j } X. B )
53 nfcv 
 |-  F/_ j { k }
54 nfcsb1v 
 |-  F/_ j [_ k / j ]_ B
55 53 54 nfxp 
 |-  F/_ j ( { k } X. [_ k / j ]_ B )
56 25 55 nfel 
 |-  F/ j <. ( g ` x ) , x >. e. ( { k } X. [_ k / j ]_ B )
57 sneq 
 |-  ( j = k -> { j } = { k } )
58 csbeq1a 
 |-  ( j = k -> B = [_ k / j ]_ B )
59 57 58 xpeq12d 
 |-  ( j = k -> ( { j } X. B ) = ( { k } X. [_ k / j ]_ B ) )
60 59 eleq2d 
 |-  ( j = k -> ( <. ( g ` x ) , x >. e. ( { j } X. B ) <-> <. ( g ` x ) , x >. e. ( { k } X. [_ k / j ]_ B ) ) )
61 3 51 52 56 60 cbvrexfw 
 |-  ( E. j e. A <. ( g ` x ) , x >. e. ( { j } X. B ) <-> E. k e. A <. ( g ` x ) , x >. e. ( { k } X. [_ k / j ]_ B ) )
62 50 61 bitri 
 |-  ( <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B ) <-> E. k e. A <. ( g ` x ) , x >. e. ( { k } X. [_ k / j ]_ B ) )
63 49 62 sylibr 
 |-  ( ( ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) /\ j e. A ) /\ x e. B ) -> <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B ) )
64 eliun 
 |-  ( x e. U_ j e. A B <-> E. j e. A x e. B )
65 64 biimpi 
 |-  ( x e. U_ j e. A B -> E. j e. A x e. B )
66 65 adantl 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> E. j e. A x e. B )
67 24 27 63 66 r19.29af2 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B ) )
68 67 ex 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> ( x e. U_ j e. A B -> <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B ) ) )
69 14 68 ralrimi 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> A. x e. U_ j e. A B <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B ) )
70 vex 
 |-  x e. _V
71 33 70 opth 
 |-  ( <. ( g ` x ) , x >. = <. ( g ` y ) , y >. <-> ( ( g ` x ) = ( g ` y ) /\ x = y ) )
72 71 simprbi 
 |-  ( <. ( g ` x ) , x >. = <. ( g ` y ) , y >. -> x = y )
73 72 rgen2w 
 |-  A. x e. U_ j e. A B A. y e. U_ j e. A B ( <. ( g ` x ) , x >. = <. ( g ` y ) , y >. -> x = y )
74 73 a1i 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> A. x e. U_ j e. A B A. y e. U_ j e. A B ( <. ( g ` x ) , x >. = <. ( g ` y ) , y >. -> x = y ) )
75 69 74 jca 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> ( A. x e. U_ j e. A B <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B A. y e. U_ j e. A B ( <. ( g ` x ) , x >. = <. ( g ` y ) , y >. -> x = y ) ) )
76 eqid 
 |-  ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. )
77 fveq2 
 |-  ( x = y -> ( g ` x ) = ( g ` y ) )
78 id 
 |-  ( x = y -> x = y )
79 77 78 opeq12d 
 |-  ( x = y -> <. ( g ` x ) , x >. = <. ( g ` y ) , y >. )
80 76 79 f1mpt 
 |-  ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) <-> ( A. x e. U_ j e. A B <. ( g ` x ) , x >. e. U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B A. y e. U_ j e. A B ( <. ( g ` x ) , x >. = <. ( g ` y ) , y >. -> x = y ) ) )
81 75 80 sylibr 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) )
82 opex 
 |-  <. ( g ` x ) , x >. e. _V
83 76 fvmpt2 
 |-  ( ( x e. U_ j e. A B /\ <. ( g ` x ) , x >. e. _V ) -> ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) = <. ( g ` x ) , x >. )
84 82 83 mpan2 
 |-  ( x e. U_ j e. A B -> ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) = <. ( g ` x ) , x >. )
85 37 84 syl 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) = <. ( g ` x ) , x >. )
86 85 fveq2d 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = ( 2nd ` <. ( g ` x ) , x >. ) )
87 33 70 op2nd 
 |-  ( 2nd ` <. ( g ` x ) , x >. ) = x
88 86 87 eqtrdi 
 |-  ( ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) /\ x e. U_ j e. A B ) -> ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x )
89 88 ex 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> ( x e. U_ j e. A B -> ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x ) )
90 14 89 ralrimi 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> A. x e. U_ j e. A B ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x )
91 81 90 jca 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x ) )
92 nfcv 
 |-  F/_ j k
93 92 3 nfel 
 |-  F/ j k e. A
94 15 93 nfan 
 |-  F/ j ( ph /\ k e. A )
95 nfcv 
 |-  F/_ j W
96 54 95 nfel 
 |-  F/ j [_ k / j ]_ B e. W
97 94 96 nfim 
 |-  F/ j ( ( ph /\ k e. A ) -> [_ k / j ]_ B e. W )
98 eleq1w 
 |-  ( j = k -> ( j e. A <-> k e. A ) )
99 98 anbi2d 
 |-  ( j = k -> ( ( ph /\ j e. A ) <-> ( ph /\ k e. A ) ) )
100 58 eleq1d 
 |-  ( j = k -> ( B e. W <-> [_ k / j ]_ B e. W ) )
101 99 100 imbi12d 
 |-  ( j = k -> ( ( ( ph /\ j e. A ) -> B e. W ) <-> ( ( ph /\ k e. A ) -> [_ k / j ]_ B e. W ) ) )
102 97 101 4 chvarfv 
 |-  ( ( ph /\ k e. A ) -> [_ k / j ]_ B e. W )
103 102 ralrimiva 
 |-  ( ph -> A. k e. A [_ k / j ]_ B e. W )
104 nfcv 
 |-  F/_ k B
105 3 51 104 54 58 cbviunf 
 |-  U_ j e. A B = U_ k e. A [_ k / j ]_ B
106 iunexg 
 |-  ( ( A e. V /\ A. k e. A [_ k / j ]_ B e. W ) -> U_ k e. A [_ k / j ]_ B e. _V )
107 105 106 eqeltrid 
 |-  ( ( A e. V /\ A. k e. A [_ k / j ]_ B e. W ) -> U_ j e. A B e. _V )
108 1 103 107 syl2anc 
 |-  ( ph -> U_ j e. A B e. _V )
109 mptexg 
 |-  ( U_ j e. A B e. _V -> ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) e. _V )
110 f1eq1 
 |-  ( f = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) -> ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) <-> ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) ) )
111 nfcv 
 |-  F/_ x f
112 nfmpt1 
 |-  F/_ x ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. )
113 111 112 nfeq 
 |-  F/ x f = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. )
114 fveq1 
 |-  ( f = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) -> ( f ` x ) = ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) )
115 114 fveqeq2d 
 |-  ( f = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) -> ( ( 2nd ` ( f ` x ) ) = x <-> ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x ) )
116 113 115 ralbid 
 |-  ( f = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) -> ( A. x e. U_ j e. A B ( 2nd ` ( f ` x ) ) = x <-> A. x e. U_ j e. A B ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x ) )
117 110 116 anbi12d 
 |-  ( f = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) -> ( ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( f ` x ) ) = x ) <-> ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x ) ) )
118 117 spcegv 
 |-  ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) e. _V -> ( ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x ) -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( f ` x ) ) = x ) ) )
119 108 109 118 3syl 
 |-  ( ph -> ( ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x ) -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( f ` x ) ) = x ) ) )
120 119 adantr 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> ( ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) ) = x ) -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( f ` x ) ) = x ) ) )
121 91 120 mpd 
 |-  ( ( ph /\ ( g : U_ j e. A B --> A /\ A. x e. U_ j e. A B x e. [_ ( g ` x ) / j ]_ B ) ) -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( f ` x ) ) = x ) )
122 9 121 exlimddv 
 |-  ( ph -> E. f ( f : U_ j e. A B -1-1-> U_ j e. A ( { j } X. B ) /\ A. x e. U_ j e. A B ( 2nd ` ( f ` x ) ) = x ) )