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

Theorem upixp 28623
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 5947 . . 3  |-  ( B  e.  S  ->  (
u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s
) `  u )
) )  e.  _V )
213ad2ant2 1010 . 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 5841 . . . . . . . . . 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 2795 . . . . . . . 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 1152 . . . . . 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 5691 . . . . . . . . 9  |-  ( a  =  s  ->  ( F `  a )  =  ( F `  s ) )
98fveq1d 5693 . . . . . . . 8  |-  ( a  =  s  ->  (
( F `  a
) `  u )  =  ( ( F `
 s ) `  u ) )
10 fveq2 5691 . . . . . . . 8  |-  ( a  =  s  ->  ( C `  a )  =  ( C `  s ) )
119, 10eleq12d 2511 . . . . . . 7  |-  ( a  =  s  ->  (
( ( F `  a ) `  u
)  e.  ( C `
 a )  <->  ( ( F `  s ) `  u )  e.  ( C `  s ) ) )
1211cbvralv 2947 . . . . . 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 991 . . . . . 6  |-  ( ( ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )  /\  u  e.  B
)  ->  A  e.  R )
15 mptelixpg 7300 . . . . . 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 5691 . . . . . 6  |-  ( b  =  s  ->  ( C `  b )  =  ( C `  s ) )
2019cbvixpv 7281 . . . . 5  |-  X_ b  e.  A  ( C `  b )  =  X_ s  e.  A  ( C `  s )
2118, 20eqtri 2463 . . . 4  |-  X  = 
X_ s  e.  A  ( C `  s )
2217, 21syl6eleqr 2534 . . 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 2443 . . 3  |-  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )  =  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )
2422, 23fmptd 5867 . 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 1673 . . . 4  |-  F/ a  A  e.  R
26 nfv 1673 . . . 4  |-  F/ a  B  e.  S
27 nfra1 2766 . . . 4  |-  F/ a A. a  e.  A  ( F `  a ) : B --> ( C `
 a )
2825, 26, 27nf3an 1863 . . 3  |-  F/ a ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )
29 fveq2 5691 . . . . . . . . 9  |-  ( s  =  a  ->  ( F `  s )  =  ( F `  a ) )
3029fveq1d 5693 . . . . . . . 8  |-  ( s  =  a  ->  (
( F `  s
) `  u )  =  ( ( F `
 a ) `  u ) )
31 eqid 2443 . . . . . . . 8  |-  ( s  e.  A  |->  ( ( F `  s ) `
 u ) )  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )
32 fvex 5701 . . . . . . . 8  |-  ( ( F `  s ) `
 u )  e. 
_V
3330, 31, 32fvmpt3i 5778 . . . . . . 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 4379 . . . . 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 2444 . . . . . 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 5691 . . . . . . . . 9  |-  ( w  =  a  ->  (
x `  w )  =  ( x `  a ) )
3938mpteq2dv 4379 . . . . . . . 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 5701 . . . . . . . . . . . 12  |-  ( C `
 b )  e. 
_V
4241rgenw 2783 . . . . . . . . . . 11  |-  A. b  e.  A  ( C `  b )  e.  _V
43 ixpexg 7287 . . . . . . . . . . 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 2513 . . . . . . . . 9  |-  X  e. 
_V
4645mptex 5948 . . . . . . . 8  |-  ( x  e.  X  |->  ( x `
 w ) )  e.  _V
4739, 40, 46fvmpt3i 5778 . . . . . . 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 5690 . . . . . 6  |-  ( x  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )  -> 
( x `  a
)  =  ( ( s  e.  A  |->  ( ( F `  s
) `  u )
) `  a )
)
5036, 37, 48, 49fmptco 5876 . . . . 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 2776 . . . . . . . 8  |-  ( A. a  e.  A  ( F `  a ) : B --> ( C `  a )  ->  (
a  e.  A  -> 
( F `  a
) : B --> ( C `
 a ) ) )
52513ad2ant3 1011 . . . . . . 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 5744 . . . . 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 2486 . . . 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 2797 . 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 5744 . . . . 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 5691 . . . . . . . . . . . . . 14  |-  ( a  =  s  ->  ( P `  a )  =  ( P `  s ) )
6261coeq1d 5001 . . . . . . . . . . . . 13  |-  ( a  =  s  ->  (
( P `  a
)  o.  h )  =  ( ( P `
 s )  o.  h ) )
638, 62eqeq12d 2457 . . . . . . . . . . . 12  |-  ( a  =  s  ->  (
( F `  a
)  =  ( ( P `  a )  o.  h )  <->  ( F `  s )  =  ( ( P `  s
)  o.  h ) ) )
6463rspccva 3072 . . . . . . . . . . 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 5693 . . . . . . . . 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 5768 . . . . . . . . . . 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 5691 . . . . . . . . . . . . . 14  |-  ( w  =  s  ->  (
x `  w )  =  ( x `  s ) )
7170mpteq2dv 4379 . . . . . . . . . . . . 13  |-  ( w  =  s  ->  (
x  e.  X  |->  ( x `  w ) )  =  ( x  e.  X  |->  ( x `
 s ) ) )
7271, 40, 46fvmpt3i 5778 . . . . . . . . . . . 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 5693 . . . . . . . . . 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 5841 . . . . . . . . . . . . 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 5690 . . . . . . . . . . . . 13  |-  ( x  =  ( h `  u )  ->  (
x `  s )  =  ( ( h `
 u ) `  s ) )
78 eqid 2443 . . . . . . . . . . . . 13  |-  ( x  e.  X  |->  ( x `
 s ) )  =  ( x  e.  X  |->  ( x `  s ) )
79 fvex 5701 . . . . . . . . . . . . 13  |-  ( x `
 s )  e. 
_V
8077, 78, 79fvmpt3i 5778 . . . . . . . . . . . 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 2475 . . . . . . . . 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 2479 . . . . . . . 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 4378 . . . . . . 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 2533 . . . . . . . . 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 7269 . . . . . . . . 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 5737 . . . . . . . 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 2478 . . . . . 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 4378 . . . . 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 2478 . . . 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 1685 . 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 5542 . . . 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 4998 . . . . . 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 2454 . . . . 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 2735 . . . 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 3130 . 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 1223 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 965   A.wal 1367    = wceq 1369    e. wcel 1756   E!weu 2253   A.wral 2715   _Vcvv 2972    e. cmpt 4350    o. ccom 4844    Fn wfn 5413   -->wf 5414   ` cfv 5418   X_cixp 7263
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ixp 7264
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator