Metamath Proof Explorer

Theorem upixp

Description: Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses upixp.1 
|- X = X_ b e. A ( C ` b )
upixp.2 
|- P = ( w e. A |-> ( x e. X |-> ( x ` w ) ) )
Assertion upixp 
|- ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> E! h ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) )

Proof

Step Hyp Ref Expression
1 upixp.1 
 |-  X = X_ b e. A ( C ` b )
2 upixp.2 
 |-  P = ( w e. A |-> ( x e. X |-> ( x ` w ) ) )
3 mptexg 
 |-  ( B e. S -> ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) e. _V )
4 3 3ad2ant2 
 |-  ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) e. _V )
5 ffvelrn 
 |-  ( ( ( F ` a ) : B --> ( C ` a ) /\ u e. B ) -> ( ( F ` a ) ` u ) e. ( C ` a ) )
6 5 expcom 
 |-  ( u e. B -> ( ( F ` a ) : B --> ( C ` a ) -> ( ( F ` a ) ` u ) e. ( C ` a ) ) )
7 6 ralimdv 
 |-  ( u e. B -> ( A. a e. A ( F ` a ) : B --> ( C ` a ) -> A. a e. A ( ( F ` a ) ` u ) e. ( C ` a ) ) )
8 7 impcom 
 |-  ( ( A. a e. A ( F ` a ) : B --> ( C ` a ) /\ u e. B ) -> A. a e. A ( ( F ` a ) ` u ) e. ( C ` a ) )
9 8 3ad2antl3 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ u e. B ) -> A. a e. A ( ( F ` a ) ` u ) e. ( C ` a ) )
10 fveq2 
 |-  ( a = s -> ( F ` a ) = ( F ` s ) )
11 10 fveq1d 
 |-  ( a = s -> ( ( F ` a ) ` u ) = ( ( F ` s ) ` u ) )
12 fveq2 
 |-  ( a = s -> ( C ` a ) = ( C ` s ) )
13 11 12 eleq12d 
 |-  ( a = s -> ( ( ( F ` a ) ` u ) e. ( C ` a ) <-> ( ( F ` s ) ` u ) e. ( C ` s ) ) )
14 13 cbvralvw 
 |-  ( A. a e. A ( ( F ` a ) ` u ) e. ( C ` a ) <-> A. s e. A ( ( F ` s ) ` u ) e. ( C ` s ) )
15 9 14 sylib 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ u e. B ) -> A. s e. A ( ( F ` s ) ` u ) e. ( C ` s ) )
16 simpl1 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ u e. B ) -> A e. R )
17 mptelixpg 
 |-  ( A e. R -> ( ( s e. A |-> ( ( F ` s ) ` u ) ) e. X_ s e. A ( C ` s ) <-> A. s e. A ( ( F ` s ) ` u ) e. ( C ` s ) ) )
18 16 17 syl 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ u e. B ) -> ( ( s e. A |-> ( ( F ` s ) ` u ) ) e. X_ s e. A ( C ` s ) <-> A. s e. A ( ( F ` s ) ` u ) e. ( C ` s ) ) )
19 15 18 mpbird 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ u e. B ) -> ( s e. A |-> ( ( F ` s ) ` u ) ) e. X_ s e. A ( C ` s ) )
20 fveq2 
 |-  ( b = s -> ( C ` b ) = ( C ` s ) )
21 20 cbvixpv 
 |-  X_ b e. A ( C ` b ) = X_ s e. A ( C ` s )
22 1 21 eqtri 
 |-  X = X_ s e. A ( C ` s )
23 19 22 eleqtrrdi 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ u e. B ) -> ( s e. A |-> ( ( F ` s ) ` u ) ) e. X )
24 23 fmpttd 
 |-  ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) : B --> X )
25 nfv 
 |-  F/ a A e. R
26 nfv 
 |-  F/ a B e. S
27 nfra1 
 |-  F/ a A. a e. A ( F ` a ) : B --> ( C ` a )
28 25 26 27 nf3an 
 |-  F/ a ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) )
29 fveq2 
 |-  ( s = a -> ( F ` s ) = ( F ` a ) )
30 29 fveq1d 
 |-  ( s = a -> ( ( F ` s ) ` u ) = ( ( F ` a ) ` u ) )
31 eqid 
 |-  ( s e. A |-> ( ( F ` s ) ` u ) ) = ( s e. A |-> ( ( F ` s ) ` u ) )
32 fvex 
 |-  ( ( F ` s ) ` u ) e. _V
33 30 31 32 fvmpt3i 
 |-  ( a e. A -> ( ( s e. A |-> ( ( F ` s ) ` u ) ) ` a ) = ( ( F ` a ) ` u ) )
34 33 adantl 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) -> ( ( s e. A |-> ( ( F ` s ) ` u ) ) ` a ) = ( ( F ` a ) ` u ) )
35 34 mpteq2dv 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) -> ( u e. B |-> ( ( s e. A |-> ( ( F ` s ) ` u ) ) ` a ) ) = ( u e. B |-> ( ( F ` a ) ` u ) ) )
36 23 adantlr 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) /\ u e. B ) -> ( s e. A |-> ( ( F ` s ) ` u ) ) e. X )
37 eqidd 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) -> ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) )
38 fveq2 
 |-  ( w = a -> ( x ` w ) = ( x ` a ) )
39 38 mpteq2dv 
 |-  ( w = a -> ( x e. X |-> ( x ` w ) ) = ( x e. X |-> ( x ` a ) ) )
40 fvex 
 |-  ( C ` b ) e. _V
41 40 rgenw 
 |-  A. b e. A ( C ` b ) e. _V
42 ixpexg 
 |-  ( A. b e. A ( C ` b ) e. _V -> X_ b e. A ( C ` b ) e. _V )
43 41 42 ax-mp 
 |-  X_ b e. A ( C ` b ) e. _V
44 1 43 eqeltri 
 |-  X e. _V
45 44 mptex 
 |-  ( x e. X |-> ( x ` w ) ) e. _V
46 39 2 45 fvmpt3i 
 |-  ( a e. A -> ( P ` a ) = ( x e. X |-> ( x ` a ) ) )
47 46 adantl 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) -> ( P ` a ) = ( x e. X |-> ( x ` a ) ) )
48 fveq1 
 |-  ( x = ( s e. A |-> ( ( F ` s ) ` u ) ) -> ( x ` a ) = ( ( s e. A |-> ( ( F ` s ) ` u ) ) ` a ) )
49 36 37 47 48 fmptco 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) -> ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) = ( u e. B |-> ( ( s e. A |-> ( ( F ` s ) ` u ) ) ` a ) ) )
50 rsp 
 |-  ( A. a e. A ( F ` a ) : B --> ( C ` a ) -> ( a e. A -> ( F ` a ) : B --> ( C ` a ) ) )
51 50 3ad2ant3 
 |-  ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> ( a e. A -> ( F ` a ) : B --> ( C ` a ) ) )
52 51 imp 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) -> ( F ` a ) : B --> ( C ` a ) )
53 52 feqmptd 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) -> ( F ` a ) = ( u e. B |-> ( ( F ` a ) ` u ) ) )
54 35 49 53 3eqtr4rd 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ a e. A ) -> ( F ` a ) = ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) )
55 54 ex 
 |-  ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> ( a e. A -> ( F ` a ) = ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) ) )
56 28 55 ralrimi 
 |-  ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> A. a e. A ( F ` a ) = ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) )
57 simprl 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) -> h : B --> X )
58 57 feqmptd 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) -> h = ( u e. B |-> ( h ` u ) ) )
59 simplrr 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) )
60 fveq2 
 |-  ( a = s -> ( P ` a ) = ( P ` s ) )
61 60 coeq1d 
 |-  ( a = s -> ( ( P ` a ) o. h ) = ( ( P ` s ) o. h ) )
62 10 61 eqeq12d 
 |-  ( a = s -> ( ( F ` a ) = ( ( P ` a ) o. h ) <-> ( F ` s ) = ( ( P ` s ) o. h ) ) )
63 62 rspccva 
 |-  ( ( A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) /\ s e. A ) -> ( F ` s ) = ( ( P ` s ) o. h ) )
64 59 63 sylan 
 |-  ( ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) /\ s e. A ) -> ( F ` s ) = ( ( P ` s ) o. h ) )
65 64 fveq1d 
 |-  ( ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) /\ s e. A ) -> ( ( F ` s ) ` u ) = ( ( ( P ` s ) o. h ) ` u ) )
66 fvco3 
 |-  ( ( h : B --> X /\ u e. B ) -> ( ( ( P ` s ) o. h ) ` u ) = ( ( P ` s ) ` ( h ` u ) ) )
67 57 66 sylan 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> ( ( ( P ` s ) o. h ) ` u ) = ( ( P ` s ) ` ( h ` u ) ) )
68 67 adantr 
 |-  ( ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) /\ s e. A ) -> ( ( ( P ` s ) o. h ) ` u ) = ( ( P ` s ) ` ( h ` u ) ) )
69 fveq2 
 |-  ( w = s -> ( x ` w ) = ( x ` s ) )
70 69 mpteq2dv 
 |-  ( w = s -> ( x e. X |-> ( x ` w ) ) = ( x e. X |-> ( x ` s ) ) )
71 70 2 45 fvmpt3i 
 |-  ( s e. A -> ( P ` s ) = ( x e. X |-> ( x ` s ) ) )
72 71 adantl 
 |-  ( ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) /\ s e. A ) -> ( P ` s ) = ( x e. X |-> ( x ` s ) ) )
73 72 fveq1d 
 |-  ( ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) /\ s e. A ) -> ( ( P ` s ) ` ( h ` u ) ) = ( ( x e. X |-> ( x ` s ) ) ` ( h ` u ) ) )
74 ffvelrn 
 |-  ( ( h : B --> X /\ u e. B ) -> ( h ` u ) e. X )
75 57 74 sylan 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> ( h ` u ) e. X )
76 fveq1 
 |-  ( x = ( h ` u ) -> ( x ` s ) = ( ( h ` u ) ` s ) )
77 eqid 
 |-  ( x e. X |-> ( x ` s ) ) = ( x e. X |-> ( x ` s ) )
78 fvex 
 |-  ( x ` s ) e. _V
79 76 77 78 fvmpt3i 
 |-  ( ( h ` u ) e. X -> ( ( x e. X |-> ( x ` s ) ) ` ( h ` u ) ) = ( ( h ` u ) ` s ) )
80 75 79 syl 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> ( ( x e. X |-> ( x ` s ) ) ` ( h ` u ) ) = ( ( h ` u ) ` s ) )
81 80 adantr 
 |-  ( ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) /\ s e. A ) -> ( ( x e. X |-> ( x ` s ) ) ` ( h ` u ) ) = ( ( h ` u ) ` s ) )
82 73 81 eqtrd 
 |-  ( ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) /\ s e. A ) -> ( ( P ` s ) ` ( h ` u ) ) = ( ( h ` u ) ` s ) )
83 65 68 82 3eqtrd 
 |-  ( ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) /\ s e. A ) -> ( ( F ` s ) ` u ) = ( ( h ` u ) ` s ) )
84 83 mpteq2dva 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> ( s e. A |-> ( ( F ` s ) ` u ) ) = ( s e. A |-> ( ( h ` u ) ` s ) ) )
85 75 1 eleqtrdi 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> ( h ` u ) e. X_ b e. A ( C ` b ) )
86 ixpfn 
 |-  ( ( h ` u ) e. X_ b e. A ( C ` b ) -> ( h ` u ) Fn A )
87 85 86 syl 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> ( h ` u ) Fn A )
88 dffn5 
 |-  ( ( h ` u ) Fn A <-> ( h ` u ) = ( s e. A |-> ( ( h ` u ) ` s ) ) )
89 87 88 sylib 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> ( h ` u ) = ( s e. A |-> ( ( h ` u ) ` s ) ) )
90 84 89 eqtr4d 
 |-  ( ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) /\ u e. B ) -> ( s e. A |-> ( ( F ` s ) ` u ) ) = ( h ` u ) )
91 90 mpteq2dva 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) -> ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) = ( u e. B |-> ( h ` u ) ) )
92 58 91 eqtr4d 
 |-  ( ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) /\ ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) ) -> h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) )
93 92 ex 
 |-  ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> ( ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) -> h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) )
94 93 alrimiv 
 |-  ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> A. h ( ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) -> h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) )
95 feq1 
 |-  ( h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) -> ( h : B --> X <-> ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) : B --> X ) )
96 coeq2 
 |-  ( h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) -> ( ( P ` a ) o. h ) = ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) )
97 96 eqeq2d 
 |-  ( h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) -> ( ( F ` a ) = ( ( P ` a ) o. h ) <-> ( F ` a ) = ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) ) )
98 97 ralbidv 
 |-  ( h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) -> ( A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) <-> A. a e. A ( F ` a ) = ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) ) )
99 95 98 anbi12d 
 |-  ( h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) -> ( ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) <-> ( ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) ) ) )
100 99 eqeu 
 |-  ( ( ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) e. _V /\ ( ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) ) /\ A. h ( ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) -> h = ( u e. B |-> ( s e. A |-> ( ( F ` s ) ` u ) ) ) ) ) -> E! h ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) )
101 4 24 56 94 100 syl121anc 
 |-  ( ( A e. R /\ B e. S /\ A. a e. A ( F ` a ) : B --> ( C ` a ) ) -> E! h ( h : B --> X /\ A. a e. A ( F ` a ) = ( ( P ` a ) o. h ) ) )