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

Theorem upixp 30425
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 6143 . . 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 6030 . . . . . . . . . 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 2867 . . . . . . . 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 5872 . . . . . . . . 9  |-  ( a  =  s  ->  ( F `  a )  =  ( F `  s ) )
98fveq1d 5874 . . . . . . . 8  |-  ( a  =  s  ->  (
( F `  a
) `  u )  =  ( ( F `
 s ) `  u ) )
10 fveq2 5872 . . . . . . . 8  |-  ( a  =  s  ->  ( C `  a )  =  ( C `  s ) )
119, 10eleq12d 2539 . . . . . . 7  |-  ( a  =  s  ->  (
( ( F `  a ) `  u
)  e.  ( C `
 a )  <->  ( ( F `  s ) `  u )  e.  ( C `  s ) ) )
1211cbvralv 3084 . . . . . 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 7525 . . . . . 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 5872 . . . . . 6  |-  ( b  =  s  ->  ( C `  b )  =  ( C `  s ) )
2019cbvixpv 7506 . . . . 5  |-  X_ b  e.  A  ( C `  b )  =  X_ s  e.  A  ( C `  s )
2118, 20eqtri 2486 . . . 4  |-  X  = 
X_ s  e.  A  ( C `  s )
2217, 21syl6eleqr 2556 . . 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 2457 . . 3  |-  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )  =  ( u  e.  B  |->  ( s  e.  A  |->  ( ( F `  s ) `
 u ) ) )
2422, 23fmptd 6056 . 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 1708 . . . 4  |-  F/ a  A  e.  R
26 nfv 1708 . . . 4  |-  F/ a  B  e.  S
27 nfra1 2838 . . . 4  |-  F/ a A. a  e.  A  ( F `  a ) : B --> ( C `
 a )
2825, 26, 27nf3an 1931 . . 3  |-  F/ a ( A  e.  R  /\  B  e.  S  /\  A. a  e.  A  ( F `  a ) : B --> ( C `
 a ) )
29 fveq2 5872 . . . . . . . . 9  |-  ( s  =  a  ->  ( F `  s )  =  ( F `  a ) )
3029fveq1d 5874 . . . . . . . 8  |-  ( s  =  a  ->  (
( F `  s
) `  u )  =  ( ( F `
 a ) `  u ) )
31 eqid 2457 . . . . . . . 8  |-  ( s  e.  A  |->  ( ( F `  s ) `
 u ) )  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )
32 fvex 5882 . . . . . . . 8  |-  ( ( F `  s ) `
 u )  e. 
_V
3330, 31, 32fvmpt3i 5960 . . . . . . 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 4544 . . . . 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 2458 . . . . . 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 5872 . . . . . . . . 9  |-  ( w  =  a  ->  (
x `  w )  =  ( x `  a ) )
3938mpteq2dv 4544 . . . . . . . 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 5882 . . . . . . . . . . . 12  |-  ( C `
 b )  e. 
_V
4241rgenw 2818 . . . . . . . . . . 11  |-  A. b  e.  A  ( C `  b )  e.  _V
43 ixpexg 7512 . . . . . . . . . . 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 2541 . . . . . . . . 9  |-  X  e. 
_V
4645mptex 6144 . . . . . . . 8  |-  ( x  e.  X  |->  ( x `
 w ) )  e.  _V
4739, 40, 46fvmpt3i 5960 . . . . . . 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 5871 . . . . . 6  |-  ( x  =  ( s  e.  A  |->  ( ( F `
 s ) `  u ) )  -> 
( x `  a
)  =  ( ( s  e.  A  |->  ( ( F `  s
) `  u )
) `  a )
)
5036, 37, 48, 49fmptco 6065 . . . . 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 2823 . . . . . . . 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 5926 . . . . 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 2509 . . . 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 2857 . 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 756 . . . . . 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 5926 . . . . 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 762 . . . . . . . . . . 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 5872 . . . . . . . . . . . . . 14  |-  ( a  =  s  ->  ( P `  a )  =  ( P `  s ) )
6261coeq1d 5174 . . . . . . . . . . . . 13  |-  ( a  =  s  ->  (
( P `  a
)  o.  h )  =  ( ( P `
 s )  o.  h ) )
638, 62eqeq12d 2479 . . . . . . . . . . . 12  |-  ( a  =  s  ->  (
( F `  a
)  =  ( ( P `  a )  o.  h )  <->  ( F `  s )  =  ( ( P `  s
)  o.  h ) ) )
6463rspccva 3209 . . . . . . . . . . 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 5874 . . . . . . . . 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 5950 . . . . . . . . . . 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 5872 . . . . . . . . . . . . . 14  |-  ( w  =  s  ->  (
x `  w )  =  ( x `  s ) )
7170mpteq2dv 4544 . . . . . . . . . . . . 13  |-  ( w  =  s  ->  (
x  e.  X  |->  ( x `  w ) )  =  ( x  e.  X  |->  ( x `
 s ) ) )
7271, 40, 46fvmpt3i 5960 . . . . . . . . . . . 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 5874 . . . . . . . . . 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 6030 . . . . . . . . . . . . 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 5871 . . . . . . . . . . . . 13  |-  ( x  =  ( h `  u )  ->  (
x `  s )  =  ( ( h `
 u ) `  s ) )
78 eqid 2457 . . . . . . . . . . . . 13  |-  ( x  e.  X  |->  ( x `
 s ) )  =  ( x  e.  X  |->  ( x `  s ) )
79 fvex 5882 . . . . . . . . . . . . 13  |-  ( x `
 s )  e. 
_V
8077, 78, 79fvmpt3i 5960 . . . . . . . . . . . 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 2498 . . . . . . . . 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 2502 . . . . . . . 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 4543 . . . . . . 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 2555 . . . . . . . . 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 7494 . . . . . . . . 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 5918 . . . . . . . 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 2501 . . . . . 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 4543 . . . . 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 2501 . . . 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 1720 . 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 5719 . . . 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 5171 . . . . . 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 2896 . . . 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 3270 . 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 1393    = wceq 1395    e. wcel 1819   E!weu 2283   A.wral 2807   _Vcvv 3109    |-> cmpt 4515    o. ccom 5012    Fn wfn 5589   -->wf 5590   ` cfv 5594   X_cixp 7488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-ixp 7489
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator