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 ffvelcdmd 
 |-  ( ( ( ( ( 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 bilani 
 |-  ( ( ( 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 )
66 24 27 63 65 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 ) )
67 66 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 ) ) )
68 14 67 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 ) )
69 vex 
 |-  x e. _V
70 33 69 opth 
 |-  ( <. ( g ` x ) , x >. = <. ( g ` y ) , y >. <-> ( ( g ` x ) = ( g ` y ) /\ x = y ) )
71 70 simprbi 
 |-  ( <. ( g ` x ) , x >. = <. ( g ` y ) , y >. -> x = y )
72 71 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 )
73 72 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 ) )
74 68 73 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 ) ) )
75 eqid 
 |-  ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. )
76 fveq2 
 |-  ( x = y -> ( g ` x ) = ( g ` y ) )
77 id 
 |-  ( x = y -> x = y )
78 76 77 opeq12d 
 |-  ( x = y -> <. ( g ` x ) , x >. = <. ( g ` y ) , y >. )
79 75 78 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 ) ) )
80 74 79 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 ) )
81 opex 
 |-  <. ( g ` x ) , x >. e. _V
82 75 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 >. )
83 81 82 mpan2 
 |-  ( x e. U_ j e. A B -> ( ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) ` x ) = <. ( g ` x ) , x >. )
84 37 83 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 >. )
85 84 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 >. ) )
86 33 69 op2nd 
 |-  ( 2nd ` <. ( g ` x ) , x >. ) = x
87 85 86 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 )
88 87 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 ) )
89 14 88 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 )
90 80 89 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 ) )
91 nfcv 
 |-  F/_ j k
92 91 3 nfel 
 |-  F/ j k e. A
93 15 92 nfan 
 |-  F/ j ( ph /\ k e. A )
94 nfcv 
 |-  F/_ j W
95 54 94 nfel 
 |-  F/ j [_ k / j ]_ B e. W
96 93 95 nfim 
 |-  F/ j ( ( ph /\ k e. A ) -> [_ k / j ]_ B e. W )
97 eleq1w 
 |-  ( j = k -> ( j e. A <-> k e. A ) )
98 97 anbi2d 
 |-  ( j = k -> ( ( ph /\ j e. A ) <-> ( ph /\ k e. A ) ) )
99 58 eleq1d 
 |-  ( j = k -> ( B e. W <-> [_ k / j ]_ B e. W ) )
100 98 99 imbi12d 
 |-  ( j = k -> ( ( ( ph /\ j e. A ) -> B e. W ) <-> ( ( ph /\ k e. A ) -> [_ k / j ]_ B e. W ) ) )
101 96 100 4 chvarfv 
 |-  ( ( ph /\ k e. A ) -> [_ k / j ]_ B e. W )
102 101 ralrimiva 
 |-  ( ph -> A. k e. A [_ k / j ]_ B e. W )
103 nfcv 
 |-  F/_ k B
104 3 51 103 54 58 cbviunf 
 |-  U_ j e. A B = U_ k e. A [_ k / j ]_ B
105 iunexg 
 |-  ( ( A e. V /\ A. k e. A [_ k / j ]_ B e. W ) -> U_ k e. A [_ k / j ]_ B e. _V )
106 104 105 eqeltrid 
 |-  ( ( A e. V /\ A. k e. A [_ k / j ]_ B e. W ) -> U_ j e. A B e. _V )
107 1 102 106 syl2anc 
 |-  ( ph -> U_ j e. A B e. _V )
108 mptexg 
 |-  ( U_ j e. A B e. _V -> ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. ) e. _V )
109 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 ) ) )
110 nfcv 
 |-  F/_ x f
111 nfmpt1 
 |-  F/_ x ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. )
112 110 111 nfeq 
 |-  F/ x f = ( x e. U_ j e. A B |-> <. ( g ` x ) , x >. )
113 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 ) )
114 113 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 ) )
115 112 114 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 ) )
116 109 115 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 ) ) )
117 116 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 ) ) )
118 107 108 117 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 ) ) )
119 118 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 ) ) )
120 90 119 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 ) )
121 9 120 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 ) )