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

Theorem upixp 28532
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 5944 . . 3  |-  ( B  e.  S  ->  (
u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s
) `  u )
) )  e.  _V )
213ad2ant2 1005 . 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 5838 . . . . . . . . . 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 2793 . . . . . . . 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 1147 . . . . . 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 5688 . . . . . . . . 9  |-  ( a  =  s  ->  ( F `  a )  =  ( F `  s ) )
98fveq1d 5690 . . . . . . . 8  |-  ( a  =  s  ->  (
( F `  a
) `  u )  =  ( ( F `
 s ) `  u ) )
10 fveq2 5688 . . . . . . . 8  |-  ( a  =  s  ->  ( C `  a )  =  ( C `  s ) )
119, 10eleq12d 2509 . . . . . . 7  |-  ( a  =  s  ->  (
( ( F `  a ) `  u
)  e.  ( C `
 a )  <->  ( ( F `  s ) `  u )  e.  ( C `  s ) ) )
1211cbvralv 2945 . . . . . 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 986 . . . . . 6  |-  ( ( ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )  /\  u  e.  B
)  ->  A  e.  R )
15 mptelixpg 7296 . . . . . 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 5688 . . . . . 6  |-  ( b  =  s  ->  ( C `  b )  =  ( C `  s ) )
2019cbvixpv 7277 . . . . 5  |-  X_ b  e.  A  ( C `  b )  =  X_ s  e.  A  ( C `  s )
2118, 20eqtri 2461 . . . 4  |-  X  = 
X_ s  e.  A  ( C `  s )
2217, 21syl6eleqr 2532 . . 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 2441 . . 3  |-  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )  =  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )
2422, 23fmptd 5864 . 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 1678 . . . 4  |-  F/ a  A  e.  R
26 nfv 1678 . . . 4  |-  F/ a  B  e.  S
27 nfra1 2764 . . . 4  |-  F/ a A. a  e.  A  ( F `  a ) : B --> ( C `
 a )
2825, 26, 27nf3an 1867 . . 3  |-  F/ a ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )
29 fveq2 5688 . . . . . . . . 9  |-  ( s  =  a  ->  ( F `  s )  =  ( F `  a ) )
3029fveq1d 5690 . . . . . . . 8  |-  ( s  =  a  ->  (
( F `  s
) `  u )  =  ( ( F `
 a ) `  u ) )
31 eqid 2441 . . . . . . . 8  |-  ( s  e.  A  |->  ( ( F `  s ) `
 u ) )  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )
32 fvex 5698 . . . . . . . 8  |-  ( ( F `  s ) `
 u )  e. 
_V
3330, 31, 32fvmpt3i 5775 . . . . . . 7  |-  ( a  e.  A  ->  (
( s  e.  A  |->  ( ( F `  s ) `  u
) ) `  a
)  =  ( ( F `  a ) `
 u ) )
3433adantl 463 . . . . . 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 4376 . . . . 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 709 . . . . . 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 2442 . . . . . 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 5688 . . . . . . . . 9  |-  ( w  =  a  ->  (
x `  w )  =  ( x `  a ) )
3938mpteq2dv 4376 . . . . . . . 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 5698 . . . . . . . . . . . 12  |-  ( C `
 b )  e. 
_V
4241rgenw 2781 . . . . . . . . . . 11  |-  A. b  e.  A  ( C `  b )  e.  _V
43 ixpexg 7283 . . . . . . . . . . 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 2511 . . . . . . . . 9  |-  X  e. 
_V
4645mptex 5945 . . . . . . . 8  |-  ( x  e.  X  |->  ( x `
 w ) )  e.  _V
4739, 40, 46fvmpt3i 5775 . . . . . . 7  |-  ( a  e.  A  ->  ( P `  a )  =  ( x  e.  X  |->  ( x `  a ) ) )
4847adantl 463 . . . . . 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 5687 . . . . . 6  |-  ( x  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )  -> 
( x `  a
)  =  ( ( s  e.  A  |->  ( ( F `  s
) `  u )
) `  a )
)
5036, 37, 48, 49fmptco 5873 . . . . 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 2774 . . . . . . . 8  |-  ( A. a  e.  A  ( F `  a ) : B --> ( C `  a )  ->  (
a  e.  A  -> 
( F `  a
) : B --> ( C `
 a ) ) )
52513ad2ant3 1006 . . . . . . 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 5741 . . . . 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 2484 . . . 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 2795 . 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 750 . . . . . 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 5741 . . . . 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 755 . . . . . . . . . . 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 5688 . . . . . . . . . . . . . 14  |-  ( a  =  s  ->  ( P `  a )  =  ( P `  s ) )
6261coeq1d 4997 . . . . . . . . . . . . 13  |-  ( a  =  s  ->  (
( P `  a
)  o.  h )  =  ( ( P `
 s )  o.  h ) )
638, 62eqeq12d 2455 . . . . . . . . . . . 12  |-  ( a  =  s  ->  (
( F `  a
)  =  ( ( P `  a )  o.  h )  <->  ( F `  s )  =  ( ( P `  s
)  o.  h ) ) )
6463rspccva 3069 . . . . . . . . . . 11  |-  ( ( A. a  e.  A  ( F `  a )  =  ( ( P `
 a )  o.  h )  /\  s  e.  A )  ->  ( F `  s )  =  ( ( P `
 s )  o.  h ) )
6560, 64sylan 468 . . . . . . . . . 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 5690 . . . . . . . . 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 5765 . . . . . . . . . . 11  |-  ( ( h : B --> X  /\  u  e.  B )  ->  ( ( ( P `
 s )  o.  h ) `  u
)  =  ( ( P `  s ) `
 ( h `  u ) ) )
6858, 67sylan 468 . . . . . . . . . 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 462 . . . . . . . . 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 5688 . . . . . . . . . . . . . 14  |-  ( w  =  s  ->  (
x `  w )  =  ( x `  s ) )
7170mpteq2dv 4376 . . . . . . . . . . . . 13  |-  ( w  =  s  ->  (
x  e.  X  |->  ( x `  w ) )  =  ( x  e.  X  |->  ( x `
 s ) ) )
7271, 40, 46fvmpt3i 5775 . . . . . . . . . . . 12  |-  ( s  e.  A  ->  ( P `  s )  =  ( x  e.  X  |->  ( x `  s ) ) )
7372adantl 463 . . . . . . . . . . 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 5690 . . . . . . . . . 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 5838 . . . . . . . . . . . . 13  |-  ( ( h : B --> X  /\  u  e.  B )  ->  ( h `  u
)  e.  X )
7658, 75sylan 468 . . . . . . . . . . . 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 5687 . . . . . . . . . . . . 13  |-  ( x  =  ( h `  u )  ->  (
x `  s )  =  ( ( h `
 u ) `  s ) )
78 eqid 2441 . . . . . . . . . . . . 13  |-  ( x  e.  X  |->  ( x `
 s ) )  =  ( x  e.  X  |->  ( x `  s ) )
79 fvex 5698 . . . . . . . . . . . . 13  |-  ( x `
 s )  e. 
_V
8077, 78, 79fvmpt3i 5775 . . . . . . . . . . . 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 462 . . . . . . . . . 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 2473 . . . . . . . . 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 2477 . . . . . . . 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 4375 . . . . . . 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 2531 . . . . . . . . 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 7265 . . . . . . . . 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 5734 . . . . . . . 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 2476 . . . . . 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 4375 . . . . 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 2476 . . . 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 1690 . 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 5539 . . . 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 4994 . . . . . 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 2452 . . . . 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 2733 . . . 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 705 . . 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 3127 . 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 1218 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 960   A.wal 1362    = wceq 1364    e. wcel 1761   E!weu 2259   A.wral 2713   _Vcvv 2970    e. cmpt 4347    o. ccom 4840    Fn wfn 5410   -->wf 5411   ` cfv 5415   X_cixp 7259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ixp 7260
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator