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

Theorem upixp 32100
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 6159 . . 3  |-  ( B  e.  S  ->  (
u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s
) `  u )
) )  e.  _V )
213ad2ant2 1036 . 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 6042 . . . . . . . . . 10  |-  ( ( ( F `  a
) : B --> ( C `
 a )  /\  u  e.  B )  ->  ( ( F `  a ) `  u
)  e.  ( C `
 a ) )
43expcom 441 . . . . . . . . 9  |-  ( u  e.  B  ->  (
( F `  a
) : B --> ( C `
 a )  -> 
( ( F `  a ) `  u
)  e.  ( C `
 a ) ) )
54ralimdv 2809 . . . . . . . 8  |-  ( u  e.  B  ->  ( A. a  e.  A  ( F `  a ) : B --> ( C `
 a )  ->  A. a  e.  A  ( ( F `  a ) `  u
)  e.  ( C `
 a ) ) )
65impcom 436 . . . . . . 7  |-  ( ( A. a  e.  A  ( F `  a ) : B --> ( C `
 a )  /\  u  e.  B )  ->  A. a  e.  A  ( ( F `  a ) `  u
)  e.  ( C `
 a ) )
763ad2antl3 1178 . . . . . 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 5887 . . . . . . . . 9  |-  ( a  =  s  ->  ( F `  a )  =  ( F `  s ) )
98fveq1d 5889 . . . . . . . 8  |-  ( a  =  s  ->  (
( F `  a
) `  u )  =  ( ( F `
 s ) `  u ) )
10 fveq2 5887 . . . . . . . 8  |-  ( a  =  s  ->  ( C `  a )  =  ( C `  s ) )
119, 10eleq12d 2533 . . . . . . 7  |-  ( a  =  s  ->  (
( ( F `  a ) `  u
)  e.  ( C `
 a )  <->  ( ( F `  s ) `  u )  e.  ( C `  s ) ) )
1211cbvralv 3030 . . . . . 6  |-  ( A. a  e.  A  (
( F `  a
) `  u )  e.  ( C `  a
)  <->  A. s  e.  A  ( ( F `  s ) `  u
)  e.  ( C `
 s ) )
137, 12sylib 201 . . . . 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 1017 . . . . . 6  |-  ( ( ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )  /\  u  e.  B
)  ->  A  e.  R )
15 mptelixpg 7584 . . . . . 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 17 . . . . 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 240 . . . 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 5887 . . . . . 6  |-  ( b  =  s  ->  ( C `  b )  =  ( C `  s ) )
2019cbvixpv 7565 . . . . 5  |-  X_ b  e.  A  ( C `  b )  =  X_ s  e.  A  ( C `  s )
2118, 20eqtri 2483 . . . 4  |-  X  = 
X_ s  e.  A  ( C `  s )
2217, 21syl6eleqr 2550 . . 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 2461 . . 3  |-  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )  =  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )
2422, 23fmptd 6068 . 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 1771 . . . 4  |-  F/ a  A  e.  R
26 nfv 1771 . . . 4  |-  F/ a  B  e.  S
27 nfra1 2780 . . . 4  |-  F/ a A. a  e.  A  ( F `  a ) : B --> ( C `
 a )
2825, 26, 27nf3an 2023 . . 3  |-  F/ a ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )
29 fveq2 5887 . . . . . . . . 9  |-  ( s  =  a  ->  ( F `  s )  =  ( F `  a ) )
3029fveq1d 5889 . . . . . . . 8  |-  ( s  =  a  ->  (
( F `  s
) `  u )  =  ( ( F `
 a ) `  u ) )
31 eqid 2461 . . . . . . . 8  |-  ( s  e.  A  |->  ( ( F `  s ) `
 u ) )  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )
32 fvex 5897 . . . . . . . 8  |-  ( ( F `  s ) `
 u )  e. 
_V
3330, 31, 32fvmpt3i 5975 . . . . . . 7  |-  ( a  e.  A  ->  (
( s  e.  A  |->  ( ( F `  s ) `  u
) ) `  a
)  =  ( ( F `  a ) `
 u ) )
3433adantl 472 . . . . . 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 4503 . . . . 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 726 . . . . . 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 2462 . . . . . 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 5887 . . . . . . . . 9  |-  ( w  =  a  ->  (
x `  w )  =  ( x `  a ) )
3938mpteq2dv 4503 . . . . . . . 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 5897 . . . . . . . . . . . 12  |-  ( C `
 b )  e. 
_V
4241rgenw 2760 . . . . . . . . . . 11  |-  A. b  e.  A  ( C `  b )  e.  _V
43 ixpexg 7571 . . . . . . . . . . 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 2535 . . . . . . . . 9  |-  X  e. 
_V
4645mptex 6160 . . . . . . . 8  |-  ( x  e.  X  |->  ( x `
 w ) )  e.  _V
4739, 40, 46fvmpt3i 5975 . . . . . . 7  |-  ( a  e.  A  ->  ( P `  a )  =  ( x  e.  X  |->  ( x `  a ) ) )
4847adantl 472 . . . . . 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 5886 . . . . . 6  |-  ( x  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )  -> 
( x `  a
)  =  ( ( s  e.  A  |->  ( ( F `  s
) `  u )
) `  a )
)
5036, 37, 48, 49fmptco 6079 . . . . 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 2765 . . . . . . . 8  |-  ( A. a  e.  A  ( F `  a ) : B --> ( C `  a )  ->  (
a  e.  A  -> 
( F `  a
) : B --> ( C `
 a ) ) )
52513ad2ant3 1037 . . . . . . 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 435 . . . . . 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 5940 . . . . 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 2506 . . . 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 440 . . 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 2799 . 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 769 . . . . . 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 5940 . . . . 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 776 . . . . . . . . . . 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 5887 . . . . . . . . . . . . . 14  |-  ( a  =  s  ->  ( P `  a )  =  ( P `  s ) )
6261coeq1d 5014 . . . . . . . . . . . . 13  |-  ( a  =  s  ->  (
( P `  a
)  o.  h )  =  ( ( P `
 s )  o.  h ) )
638, 62eqeq12d 2476 . . . . . . . . . . . 12  |-  ( a  =  s  ->  (
( F `  a
)  =  ( ( P `  a )  o.  h )  <->  ( F `  s )  =  ( ( P `  s
)  o.  h ) ) )
6463rspccva 3160 . . . . . . . . . . 11  |-  ( ( A. a  e.  A  ( F `  a )  =  ( ( P `
 a )  o.  h )  /\  s  e.  A )  ->  ( F `  s )  =  ( ( P `
 s )  o.  h ) )
6560, 64sylan 478 . . . . . . . . . 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 5889 . . . . . . . . 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 5964 . . . . . . . . . . 11  |-  ( ( h : B --> X  /\  u  e.  B )  ->  ( ( ( P `
 s )  o.  h ) `  u
)  =  ( ( P `  s ) `
 ( h `  u ) ) )
6858, 67sylan 478 . . . . . . . . . 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 471 . . . . . . . . 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 5887 . . . . . . . . . . . . . 14  |-  ( w  =  s  ->  (
x `  w )  =  ( x `  s ) )
7170mpteq2dv 4503 . . . . . . . . . . . . 13  |-  ( w  =  s  ->  (
x  e.  X  |->  ( x `  w ) )  =  ( x  e.  X  |->  ( x `
 s ) ) )
7271, 40, 46fvmpt3i 5975 . . . . . . . . . . . 12  |-  ( s  e.  A  ->  ( P `  s )  =  ( x  e.  X  |->  ( x `  s ) ) )
7372adantl 472 . . . . . . . . . . 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 5889 . . . . . . . . . 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 6042 . . . . . . . . . . . . 13  |-  ( ( h : B --> X  /\  u  e.  B )  ->  ( h `  u
)  e.  X )
7658, 75sylan 478 . . . . . . . . . . . 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 5886 . . . . . . . . . . . . 13  |-  ( x  =  ( h `  u )  ->  (
x `  s )  =  ( ( h `
 u ) `  s ) )
78 eqid 2461 . . . . . . . . . . . . 13  |-  ( x  e.  X  |->  ( x `
 s ) )  =  ( x  e.  X  |->  ( x `  s ) )
79 fvex 5897 . . . . . . . . . . . . 13  |-  ( x `
 s )  e. 
_V
8077, 78, 79fvmpt3i 5975 . . . . . . . . . . . 12  |-  ( ( h `  u )  e.  X  ->  (
( x  e.  X  |->  ( x `  s
) ) `  (
h `  u )
)  =  ( ( h `  u ) `
 s ) )
8176, 80syl 17 . . . . . . . . . . 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 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 )  ->  (
( x  e.  X  |->  ( x `  s
) ) `  (
h `  u )
)  =  ( ( h `  u ) `
 s ) )
8374, 82eqtrd 2495 . . . . . . . . 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 2499 . . . . . . . 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 4502 . . . . . . 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 2549 . . . . . . . . 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 7553 . . . . . . . . 9  |-  ( ( h `  u )  e.  X_ b  e.  A  ( C `  b )  ->  ( h `  u )  Fn  A
)
8886, 87syl 17 . . . . . . . 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 5932 . . . . . . . 8  |-  ( ( h `  u )  Fn  A  <->  ( h `  u )  =  ( s  e.  A  |->  ( ( h `  u
) `  s )
) )
9088, 89sylib 201 . . . . . . 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 2498 . . . . . 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 4502 . . . . 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 2498 . . . 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 440 . . 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 1783 . 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 5731 . . . 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 5011 . . . . . 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 2471 . . . . 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 2838 . . . 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 722 . . 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 3220 . 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 1281 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 189    /\ wa 375    /\ w3a 991   A.wal 1452    = wceq 1454    e. wcel 1897   E!weu 2309   A.wral 2748   _Vcvv 3056    |-> cmpt 4474    o. ccom 4856    Fn wfn 5595   -->wf 5596   ` cfv 5600   X_cixp 7547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-ixp 7548
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator