Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  upixp Structured version   Unicode version

Theorem upixp 29851
Description: Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
Hypotheses
Ref Expression
upixp.1  |-  X  = 
X_ b  e.  A  ( C `  b )
upixp.2  |-  P  =  ( w  e.  A  |->  ( x  e.  X  |->  ( x `  w
) ) )
Assertion
Ref Expression
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 ) ) )
Distinct variable groups:    A, a,
b, h, w, x    R, a, b, h, w, x    S, a, b, h, w, x    F, a, b, h, w, x    B, a, b, h, w, x    C, a, b, h, w, x    X, a, h, w, x    P, a, h
Allowed substitution hints:    P( x, w, b)    X( b)

Proof of Theorem upixp
Dummy variables  s  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mptexg 6130 . . 3  |-  ( B  e.  S  ->  (
u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s
) `  u )
) )  e.  _V )
213ad2ant2 1018 . 2  |-  ( ( 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 )
3 ffvelrn 6019 . . . . . . . . . 10  |-  ( ( ( F `  a
) : B --> ( C `
 a )  /\  u  e.  B )  ->  ( ( F `  a ) `  u
)  e.  ( C `
 a ) )
43expcom 435 . . . . . . . . 9  |-  ( u  e.  B  ->  (
( F `  a
) : B --> ( C `
 a )  -> 
( ( F `  a ) `  u
)  e.  ( C `
 a ) ) )
54ralimdv 2874 . . . . . . . 8  |-  ( u  e.  B  ->  ( A. a  e.  A  ( F `  a ) : B --> ( C `
 a )  ->  A. a  e.  A  ( ( F `  a ) `  u
)  e.  ( C `
 a ) ) )
65impcom 430 . . . . . . 7  |-  ( ( A. a  e.  A  ( F `  a ) : B --> ( C `
 a )  /\  u  e.  B )  ->  A. a  e.  A  ( ( F `  a ) `  u
)  e.  ( C `
 a ) )
763ad2antl3 1160 . . . . . 6  |-  ( ( ( 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 ) )
8 fveq2 5866 . . . . . . . . 9  |-  ( a  =  s  ->  ( F `  a )  =  ( F `  s ) )
98fveq1d 5868 . . . . . . . 8  |-  ( a  =  s  ->  (
( F `  a
) `  u )  =  ( ( F `
 s ) `  u ) )
10 fveq2 5866 . . . . . . . 8  |-  ( a  =  s  ->  ( C `  a )  =  ( C `  s ) )
119, 10eleq12d 2549 . . . . . . 7  |-  ( a  =  s  ->  (
( ( F `  a ) `  u
)  e.  ( C `
 a )  <->  ( ( F `  s ) `  u )  e.  ( C `  s ) ) )
1211cbvralv 3088 . . . . . 6  |-  ( A. a  e.  A  (
( F `  a
) `  u )  e.  ( C `  a
)  <->  A. s  e.  A  ( ( F `  s ) `  u
)  e.  ( C `
 s ) )
137, 12sylib 196 . . . . 5  |-  ( ( ( 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 ) )
14 simpl1 999 . . . . . 6  |-  ( ( ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )  /\  u  e.  B
)  ->  A  e.  R )
15 mptelixpg 7506 . . . . . 6  |-  ( 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
) ) )
1614, 15syl 16 . . . . 5  |-  ( ( ( 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 ) ) )
1713, 16mpbird 232 . . . 4  |-  ( ( ( 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 ) )
18 upixp.1 . . . . 5  |-  X  = 
X_ b  e.  A  ( C `  b )
19 fveq2 5866 . . . . . 6  |-  ( b  =  s  ->  ( C `  b )  =  ( C `  s ) )
2019cbvixpv 7487 . . . . 5  |-  X_ b  e.  A  ( C `  b )  =  X_ s  e.  A  ( C `  s )
2118, 20eqtri 2496 . . . 4  |-  X  = 
X_ s  e.  A  ( C `  s )
2217, 21syl6eleqr 2566 . . 3  |-  ( ( ( 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 )
23 eqid 2467 . . 3  |-  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )  =  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )
2422, 23fmptd 6045 . 2  |-  ( ( 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 1683 . . . 4  |-  F/ a  A  e.  R
26 nfv 1683 . . . 4  |-  F/ a  B  e.  S
27 nfra1 2845 . . . 4  |-  F/ a A. a  e.  A  ( F `  a ) : B --> ( C `
 a )
2825, 26, 27nf3an 1877 . . 3  |-  F/ a ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )
29 fveq2 5866 . . . . . . . . 9  |-  ( s  =  a  ->  ( F `  s )  =  ( F `  a ) )
3029fveq1d 5868 . . . . . . . 8  |-  ( s  =  a  ->  (
( F `  s
) `  u )  =  ( ( F `
 a ) `  u ) )
31 eqid 2467 . . . . . . . 8  |-  ( s  e.  A  |->  ( ( F `  s ) `
 u ) )  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )
32 fvex 5876 . . . . . . . 8  |-  ( ( F `  s ) `
 u )  e. 
_V
3330, 31, 32fvmpt3i 5954 . . . . . . 7  |-  ( a  e.  A  ->  (
( s  e.  A  |->  ( ( F `  s ) `  u
) ) `  a
)  =  ( ( F `  a ) `
 u ) )
3433adantl 466 . . . . . 6  |-  ( ( ( 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 ) )
3534mpteq2dv 4534 . . . . 5  |-  ( ( ( 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 ) ) )
3622adantlr 714 . . . . . 6  |-  ( ( ( ( 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 2468 . . . . . 6  |-  ( ( ( 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 5866 . . . . . . . . 9  |-  ( w  =  a  ->  (
x `  w )  =  ( x `  a ) )
3938mpteq2dv 4534 . . . . . . . 8  |-  ( w  =  a  ->  (
x  e.  X  |->  ( x `  w ) )  =  ( x  e.  X  |->  ( x `
 a ) ) )
40 upixp.2 . . . . . . . 8  |-  P  =  ( w  e.  A  |->  ( x  e.  X  |->  ( x `  w
) ) )
41 fvex 5876 . . . . . . . . . . . 12  |-  ( C `
 b )  e. 
_V
4241rgenw 2825 . . . . . . . . . . 11  |-  A. b  e.  A  ( C `  b )  e.  _V
43 ixpexg 7493 . . . . . . . . . . 11  |-  ( A. b  e.  A  ( C `  b )  e.  _V  ->  X_ b  e.  A  ( C `  b )  e.  _V )
4442, 43ax-mp 5 . . . . . . . . . 10  |-  X_ b  e.  A  ( C `  b )  e.  _V
4518, 44eqeltri 2551 . . . . . . . . 9  |-  X  e. 
_V
4645mptex 6131 . . . . . . . 8  |-  ( x  e.  X  |->  ( x `
 w ) )  e.  _V
4739, 40, 46fvmpt3i 5954 . . . . . . 7  |-  ( a  e.  A  ->  ( P `  a )  =  ( x  e.  X  |->  ( x `  a ) ) )
4847adantl 466 . . . . . 6  |-  ( ( ( 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 ) ) )
49 fveq1 5865 . . . . . 6  |-  ( x  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )  -> 
( x `  a
)  =  ( ( s  e.  A  |->  ( ( F `  s
) `  u )
) `  a )
)
5036, 37, 48, 49fmptco 6054 . . . . 5  |-  ( ( ( 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 ) ) )
51 rsp 2830 . . . . . . . 8  |-  ( A. a  e.  A  ( F `  a ) : B --> ( C `  a )  ->  (
a  e.  A  -> 
( F `  a
) : B --> ( C `
 a ) ) )
52513ad2ant3 1019 . . . . . . 7  |-  ( ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )  ->  ( a  e.  A  ->  ( F `  a ) : B --> ( C `  a ) ) )
5352imp 429 . . . . . 6  |-  ( ( ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )  /\  a  e.  A
)  ->  ( F `  a ) : B --> ( C `  a ) )
5453feqmptd 5920 . . . . 5  |-  ( ( ( 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 )
) )
5535, 50, 543eqtr4rd 2519 . . . 4  |-  ( ( ( 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 ) ) ) ) )
5655ex 434 . . 3  |-  ( ( 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 ) ) ) ) ) )
5728, 56ralrimi 2864 . 2  |-  ( ( 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
) ) ) ) )
58 simprl 755 . . . . . 6  |-  ( ( ( 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 )
5958feqmptd 5920 . . . . 5  |-  ( ( ( 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 ) ) )
60 simplrr 760 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
61 fveq2 5866 . . . . . . . . . . . . . 14  |-  ( a  =  s  ->  ( P `  a )  =  ( P `  s ) )
6261coeq1d 5164 . . . . . . . . . . . . 13  |-  ( a  =  s  ->  (
( P `  a
)  o.  h )  =  ( ( P `
 s )  o.  h ) )
638, 62eqeq12d 2489 . . . . . . . . . . . 12  |-  ( a  =  s  ->  (
( F `  a
)  =  ( ( P `  a )  o.  h )  <->  ( F `  s )  =  ( ( P `  s
)  o.  h ) ) )
6463rspccva 3213 . . . . . . . . . . 11  |-  ( ( A. a  e.  A  ( F `  a )  =  ( ( P `
 a )  o.  h )  /\  s  e.  A )  ->  ( F `  s )  =  ( ( P `
 s )  o.  h ) )
6560, 64sylan 471 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) )
6665fveq1d 5868 . . . . . . . . 9  |-  ( ( ( ( ( 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 ) )
67 fvco3 5944 . . . . . . . . . . 11  |-  ( ( h : B --> X  /\  u  e.  B )  ->  ( ( ( P `
 s )  o.  h ) `  u
)  =  ( ( P `  s ) `
 ( h `  u ) ) )
6858, 67sylan 471 . . . . . . . . . 10  |-  ( ( ( ( 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 )
) )
6968adantr 465 . . . . . . . . 9  |-  ( ( ( ( ( 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
) ) )
70 fveq2 5866 . . . . . . . . . . . . . 14  |-  ( w  =  s  ->  (
x `  w )  =  ( x `  s ) )
7170mpteq2dv 4534 . . . . . . . . . . . . 13  |-  ( w  =  s  ->  (
x  e.  X  |->  ( x `  w ) )  =  ( x  e.  X  |->  ( x `
 s ) ) )
7271, 40, 46fvmpt3i 5954 . . . . . . . . . . . 12  |-  ( s  e.  A  ->  ( P `  s )  =  ( x  e.  X  |->  ( x `  s ) ) )
7372adantl 466 . . . . . . . . . . 11  |-  ( ( ( ( ( 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 ) ) )
7473fveq1d 5868 . . . . . . . . . 10  |-  ( ( ( ( ( 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
) ) )
75 ffvelrn 6019 . . . . . . . . . . . . 13  |-  ( ( h : B --> X  /\  u  e.  B )  ->  ( h `  u
)  e.  X )
7658, 75sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ( 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
)
77 fveq1 5865 . . . . . . . . . . . . 13  |-  ( x  =  ( h `  u )  ->  (
x `  s )  =  ( ( h `
 u ) `  s ) )
78 eqid 2467 . . . . . . . . . . . . 13  |-  ( x  e.  X  |->  ( x `
 s ) )  =  ( x  e.  X  |->  ( x `  s ) )
79 fvex 5876 . . . . . . . . . . . . 13  |-  ( x `
 s )  e. 
_V
8077, 78, 79fvmpt3i 5954 . . . . . . . . . . . 12  |-  ( ( h `  u )  e.  X  ->  (
( x  e.  X  |->  ( x `  s
) ) `  (
h `  u )
)  =  ( ( h `  u ) `
 s ) )
8176, 80syl 16 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
8281adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( 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 ) )
8374, 82eqtrd 2508 . . . . . . . . 9  |-  ( ( ( ( ( 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
) )
8466, 69, 833eqtrd 2512 . . . . . . . 8  |-  ( ( ( ( ( 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 ) )
8584mpteq2dva 4533 . . . . . . 7  |-  ( ( ( ( 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 ) ) )
8676, 18syl6eleq 2565 . . . . . . . . 9  |-  ( ( ( ( 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 )
)
87 ixpfn 7475 . . . . . . . . 9  |-  ( ( h `  u )  e.  X_ b  e.  A  ( C `  b )  ->  ( h `  u )  Fn  A
)
8886, 87syl 16 . . . . . . . 8  |-  ( ( ( ( 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
)
89 dffn5 5913 . . . . . . . 8  |-  ( ( h `  u )  Fn  A  <->  ( h `  u )  =  ( s  e.  A  |->  ( ( h `  u
) `  s )
) )
9088, 89sylib 196 . . . . . . 7  |-  ( ( ( ( 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 )
) )
9185, 90eqtr4d 2511 . . . . . 6  |-  ( ( ( ( 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 ) )
9291mpteq2dva 4533 . . . . 5  |-  ( ( ( 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 ) ) )
9359, 92eqtr4d 2511 . . . 4  |-  ( ( ( 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 )
) ) )
9493ex 434 . . 3  |-  ( ( 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 ) ) ) ) )
9594alrimiv 1695 . 2  |-  ( ( 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 ) ) ) ) )
96 feq1 5713 . . . 4  |-  ( h  =  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `
 s ) `  u ) ) )  ->  ( h : B --> X  <->  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) ) : B --> X ) )
97 coeq2 5161 . . . . . 6  |-  ( 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 ) ) ) ) )
9897eqeq2d 2481 . . . . 5  |-  ( 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 ) ) ) ) ) )
9998ralbidv 2903 . . . 4  |-  ( 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
) ) ) ) ) )
10096, 99anbi12d 710 . . 3  |-  ( 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 ) ) ) ) ) ) )
101100eqeu 3274 . 2  |-  ( ( ( 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 ) ) )
1022, 24, 57, 95, 101syl121anc 1233 1  |-  ( ( 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 ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973   A.wal 1377    = wceq 1379    e. wcel 1767   E!weu 2275   A.wral 2814   _Vcvv 3113    |-> cmpt 4505    o. ccom 5003    Fn wfn 5583   -->wf 5584   ` cfv 5588   X_cixp 7469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ixp 7470
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator