Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  kelac1 Unicode version

Theorem kelac1 27037
Description: Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Hypotheses
Ref Expression
kelac1.z  |-  ( (
ph  /\  x  e.  I )  ->  S  =/=  (/) )
kelac1.j  |-  ( (
ph  /\  x  e.  I )  ->  J  e.  Top )
kelac1.c  |-  ( (
ph  /\  x  e.  I )  ->  C  e.  ( Clsd `  J
) )
kelac1.b  |-  ( (
ph  /\  x  e.  I )  ->  B : S -1-1-onto-> C )
kelac1.u  |-  ( (
ph  /\  x  e.  I )  ->  U  e.  U. J )
kelac1.k  |-  ( ph  ->  ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Comp )
Assertion
Ref Expression
kelac1  |-  ( ph  -> 
X_ x  e.  I  S  =/=  (/) )
Distinct variable groups:    ph, x    x, I
Allowed substitution hints:    B( x)    C( x)    S( x)    U( x)    J( x)

Proof of Theorem kelac1
Dummy variables  f 
y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kelac1.c . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  C  e.  ( Clsd `  J
) )
2 eqid 2412 . . . . . . . 8  |-  U. J  =  U. J
32cldss 17056 . . . . . . 7  |-  ( C  e.  ( Clsd `  J
)  ->  C  C_  U. J
)
41, 3syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  C  C_ 
U. J )
54ralrimiva 2757 . . . . 5  |-  ( ph  ->  A. x  e.  I  C  C_  U. J )
6 boxriin 7071 . . . . 5  |-  ( A. x  e.  I  C  C_ 
U. J  ->  X_ x  e.  I  C  =  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) ) )
75, 6syl 16 . . . 4  |-  ( ph  -> 
X_ x  e.  I  C  =  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) ) )
8 kelac1.k . . . . . . . . 9  |-  ( ph  ->  ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Comp )
9 cmptop 17420 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Comp  ->  (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top )
10 0ntop 16941 . . . . . . . . . . 11  |-  -.  (/)  e.  Top
11 fvprc 5689 . . . . . . . . . . . 12  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( Xt_ `  (
x  e.  I  |->  J ) )  =  (/) )
1211eleq1d 2478 . . . . . . . . . . 11  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top  <->  (/)  e.  Top ) )
1310, 12mtbiri 295 . . . . . . . . . 10  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  -.  ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top )
1413con4i 124 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top  ->  ( x  e.  I  |->  J )  e.  _V )
158, 9, 143syl 19 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J )  e.  _V )
16 kelac1.j . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  J  e.  Top )
17 eqid 2412 . . . . . . . . 9  |-  ( x  e.  I  |->  J )  =  ( x  e.  I  |->  J )
1816, 17fmptd 5860 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J ) : I --> Top )
19 dmfex 5593 . . . . . . . 8  |-  ( ( ( x  e.  I  |->  J )  e.  _V  /\  ( x  e.  I  |->  J ) : I --> Top )  ->  I  e.  _V )
2015, 18, 19syl2anc 643 . . . . . . 7  |-  ( ph  ->  I  e.  _V )
2116ralrimiva 2757 . . . . . . 7  |-  ( ph  ->  A. x  e.  I  J  e.  Top )
22 eqid 2412 . . . . . . . 8  |-  ( Xt_ `  ( x  e.  I  |->  J ) )  =  ( Xt_ `  (
x  e.  I  |->  J ) )
2322ptunimpt 17588 . . . . . . 7  |-  ( ( I  e.  _V  /\  A. x  e.  I  J  e.  Top )  ->  X_ x  e.  I  U. J  =  U. ( Xt_ `  ( x  e.  I  |->  J ) ) )
2420, 21, 23syl2anc 643 . . . . . 6  |-  ( ph  -> 
X_ x  e.  I  U. J  =  U. ( Xt_ `  ( x  e.  I  |->  J ) ) )
2524ineq1d 3509 . . . . 5  |-  ( ph  ->  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =  ( U. ( Xt_ `  (
x  e.  I  |->  J ) )  i^i  |^|_ y  e.  I  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
) ) )
26 eqid 2412 . . . . . 6  |-  U. ( Xt_ `  ( x  e.  I  |->  J ) )  =  U. ( Xt_ `  ( x  e.  I  |->  J ) )
272topcld 17062 . . . . . . . . . 10  |-  ( J  e.  Top  ->  U. J  e.  ( Clsd `  J
) )
2816, 27syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  U. J  e.  ( Clsd `  J
) )
29 ifcl 3743 . . . . . . . . 9  |-  ( ( C  e.  ( Clsd `  J )  /\  U. J  e.  ( Clsd `  J ) )  ->  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  J )
)
301, 28, 29syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  if ( x  =  y ,  C ,  U. J
)  e.  ( Clsd `  J ) )
3120, 16, 30ptcldmpt 17607 . . . . . . 7  |-  ( ph  -> 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  ( Xt_ `  ( x  e.  I  |->  J ) ) ) )
3231adantr 452 . . . . . 6  |-  ( (
ph  /\  y  e.  I )  ->  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
)  e.  ( Clsd `  ( Xt_ `  (
x  e.  I  |->  J ) ) ) )
33 simprr 734 . . . . . . . 8  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
z  e.  Fin )
34 kelac1.b . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  B : S -1-1-onto-> C )
35 f1ofo 5648 . . . . . . . . . . . . . . 15  |-  ( B : S -1-1-onto-> C  ->  B : S -onto-> C )
36 foima 5625 . . . . . . . . . . . . . . 15  |-  ( B : S -onto-> C  -> 
( B " S
)  =  C )
3734, 35, 363syl 19 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =  C )
3837eqcomd 2417 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  C  =  ( B " S ) )
39 kelac1.z . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  S  =/=  (/) )
40 f1ofn 5642 . . . . . . . . . . . . . . . . 17  |-  ( B : S -1-1-onto-> C  ->  B  Fn  S )
4134, 40syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  B  Fn  S )
42 ssid 3335 . . . . . . . . . . . . . . . 16  |-  S  C_  S
43 fnimaeq0 5533 . . . . . . . . . . . . . . . 16  |-  ( ( B  Fn  S  /\  S  C_  S )  -> 
( ( B " S )  =  (/)  <->  S  =  (/) ) )
4441, 42, 43sylancl 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =  (/)  <->  S  =  (/) ) )
4544necon3bid 2610 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =/=  (/)  <->  S  =/=  (/) ) )
4639, 45mpbird 224 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =/=  (/) )
4738, 46eqnetrd 2593 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  I )  ->  C  =/=  (/) )
48 n0 3605 . . . . . . . . . . . 12  |-  ( C  =/=  (/)  <->  E. w  w  e.  C )
4947, 48sylib 189 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  I )  ->  E. w  w  e.  C )
50 rexv 2938 . . . . . . . . . . 11  |-  ( E. w  e.  _V  w  e.  C  <->  E. w  w  e.  C )
5149, 50sylibr 204 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  I )  ->  E. w  e.  _V  w  e.  C
)
5251ralrimiva 2757 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  I  E. w  e.  _V  w  e.  C )
53 ssralv 3375 . . . . . . . . . 10  |-  ( z 
C_  I  ->  ( A. x  e.  I  E. w  e.  _V  w  e.  C  ->  A. x  e.  z  E. w  e.  _V  w  e.  C ) )
5453adantr 452 . . . . . . . . 9  |-  ( ( z  C_  I  /\  z  e.  Fin )  ->  ( A. x  e.  I  E. w  e. 
_V  w  e.  C  ->  A. x  e.  z  E. w  e.  _V  w  e.  C )
)
5552, 54mpan9 456 . . . . . . . 8  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  A. x  e.  z  E. w  e.  _V  w  e.  C )
56 eleq1 2472 . . . . . . . . 9  |-  ( w  =  ( f `  x )  ->  (
w  e.  C  <->  ( f `  x )  e.  C
) )
5756ac6sfi 7318 . . . . . . . 8  |-  ( ( z  e.  Fin  /\  A. x  e.  z  E. w  e.  _V  w  e.  C )  ->  E. f
( f : z --> _V  /\  A. x  e.  z  ( f `  x )  e.  C
) )
5833, 55, 57syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  E. f ( f : z --> _V  /\  A. x  e.  z  ( f `  x )  e.  C
) )
5924eqcomd 2417 . . . . . . . . . . 11  |-  ( ph  ->  U. ( Xt_ `  (
x  e.  I  |->  J ) )  =  X_ x  e.  I  U. J )
6059ineq1d 3509 . . . . . . . . . 10  |-  ( ph  ->  ( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =  (
X_ x  e.  I  U. J  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) ) )
6160ad2antrr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) )  =  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) ) )
62 iftrue 3713 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  z  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  ( f `
 x ) )
6362ad2antrl 709 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  ( f `
 x ) )
64 simpll 731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  ph )
65 simprl 733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
z  C_  I )
6665sselda 3316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  x  e.  I )
6764, 66, 4syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  C  C_ 
U. J )
6867sseld 3315 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  (
( f `  x
)  e.  C  -> 
( f `  x
)  e.  U. J
) )
6968impr 603 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  -> 
( f `  x
)  e.  U. J
)
7063, 69eqeltrd 2486 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
)
7170expr 599 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  (
( f `  x
)  e.  C  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
) )
7271ralimdva 2752 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( A. x  e.  z  ( f `  x )  e.  C  ->  A. x  e.  z  if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  U. J ) )
7372imp 419 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  A. x  e.  z  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  U. J )
74 eldifn 3438 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( I  \ 
z )  ->  -.  x  e.  z )
75 iffalse 3714 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  x  e.  z  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
7674, 75syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( I  \ 
z )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
7776adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
78 eldifi 3437 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( I  \ 
z )  ->  x  e.  I )
79 kelac1.u . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  U  e.  U. J )
8078, 79sylan2 461 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
8177, 80eqeltrd 2486 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
)
8281ralrimiva 2757 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. x  e.  ( I  \  z ) if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  U. J )
8382ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  A. x  e.  ( I  \  z
) if ( x  e.  z ,  ( f `  x ) ,  U )  e. 
U. J )
84 ralun 3497 . . . . . . . . . . . . . 14  |-  ( ( A. x  e.  z  if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  U. J  /\  A. x  e.  ( I  \  z
) if ( x  e.  z ,  ( f `  x ) ,  U )  e. 
U. J )  ->  A. x  e.  (
z  u.  ( I 
\  z ) ) if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  U. J )
8573, 83, 84syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  A. x  e.  ( z  u.  (
I  \  z )
) if ( x  e.  z ,  ( f `  x ) ,  U )  e. 
U. J )
86 undif 3676 . . . . . . . . . . . . . . . . 17  |-  ( z 
C_  I  <->  ( z  u.  ( I  \  z
) )  =  I )
8786biimpi 187 . . . . . . . . . . . . . . . 16  |-  ( z 
C_  I  ->  (
z  u.  ( I 
\  z ) )  =  I )
8887ad2antrl 709 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( z  u.  (
I  \  z )
)  =  I )
8988raleqdv 2878 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( A. x  e.  ( z  u.  (
I  \  z )
) if ( x  e.  z ,  ( f `  x ) ,  U )  e. 
U. J  <->  A. x  e.  I  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  U. J ) )
9089adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( A. x  e.  ( z  u.  ( I  \  z
) ) if ( x  e.  z ,  ( f `  x
) ,  U )  e.  U. J  <->  A. x  e.  I  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  U. J ) )
9185, 90mpbid 202 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  A. x  e.  I  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  U. J )
9220ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  I  e.  _V )
93 mptelixpg 7066 . . . . . . . . . . . . 13  |-  ( I  e.  _V  ->  (
( x  e.  I  |->  if ( x  e.  z ,  ( f `
 x ) ,  U ) )  e.  X_ x  e.  I  U. J  <->  A. x  e.  I  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
) )
9492, 93syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( (
x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  X_ x  e.  I  U. J 
<-> 
A. x  e.  I  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
) )
9591, 94mpbird 224 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x
) ,  U ) )  e.  X_ x  e.  I  U. J )
96 eleq2 2473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C  =  if ( x  =  y ,  C ,  U. J )  -> 
( ( f `  x )  e.  C  <->  ( f `  x )  e.  if ( x  =  y ,  C ,  U. J ) ) )
97 eleq2 2473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U. J  =  if (
x  =  y ,  C ,  U. J
)  ->  ( (
f `  x )  e.  U. J  <->  ( f `  x )  e.  if ( x  =  y ,  C ,  U. J
) ) )
98 simplrr 738 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  (
x  e.  z  /\  ( f `  x
)  e.  C ) )  /\  x  =  y )  ->  (
f `  x )  e.  C )
9969adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  (
x  e.  z  /\  ( f `  x
)  e.  C ) )  /\  -.  x  =  y )  -> 
( f `  x
)  e.  U. J
)
10096, 97, 98, 99ifbothda 3737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  -> 
( f `  x
)  e.  if ( x  =  y ,  C ,  U. J
) )
10163, 100eqeltrd 2486 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  if ( x  =  y ,  C ,  U. J
) )
102101expr 599 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  (
( f `  x
)  e.  C  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  if ( x  =  y ,  C ,  U. J
) ) )
103102ralimdva 2752 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( A. x  e.  z  ( f `  x )  e.  C  ->  A. x  e.  z  if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J
) ) )
104103imp 419 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  A. x  e.  z  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
105104adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  A. x  e.  z  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
10680adantlr 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
10776adantl 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
108 incom 3501 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( I  \  z )  i^i  z )  =  ( z  i^i  (
I  \  z )
)
109 disjdif 3668 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  i^i  ( I  \ 
z ) )  =  (/)
110108, 109eqtri 2432 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( I  \  z )  i^i  z )  =  (/)
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  (
( I  \  z
)  i^i  z )  =  (/) )
112 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  e.  ( I  \  z
) )
113 simplr 732 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  y  e.  z )
114 disjne 3641 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( I  \ 
z )  i^i  z
)  =  (/)  /\  x  e.  ( I  \  z
)  /\  y  e.  z )  ->  x  =/=  y )
115111, 112, 113, 114syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  =/=  y )
116115neneqd 2591 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  -.  x  =  y )
117 iffalse 3714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  x  =  y  ->  if ( x  =  y ,  C ,  U. J )  =  U. J )
118116, 117syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  =  y ,  C ,  U. J
)  =  U. J
)
119106, 107, 1183eltr4d 2493 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  if ( x  =  y ,  C ,  U. J
) )
120119ralrimiva 2757 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  z )  ->  A. x  e.  ( I  \  z
) if ( x  e.  z ,  ( f `  x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
121120adantlr 696 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  y  e.  z )  ->  A. x  e.  ( I  \  z
) if ( x  e.  z ,  ( f `  x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
122121adantlr 696 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  A. x  e.  ( I  \  z
) if ( x  e.  z ,  ( f `  x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
123 ralun 3497 . . . . . . . . . . . . . . . 16  |-  ( ( A. x  e.  z  if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J
)  /\  A. x  e.  ( I  \  z
) if ( x  e.  z ,  ( f `  x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )  ->  A. x  e.  (
z  u.  ( I 
\  z ) ) if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J
) )
124105, 122, 123syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  A. x  e.  ( z  u.  (
I  \  z )
) if ( x  e.  z ,  ( f `  x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
12588raleqdv 2878 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( A. x  e.  ( z  u.  (
I  \  z )
) if ( x  e.  z ,  ( f `  x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J )  <->  A. x  e.  I  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) ) )
126125ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  ( A. x  e.  (
z  u.  ( I 
\  z ) ) if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  if ( x  =  y ,  C ,  U. J
)  <->  A. x  e.  I  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  if ( x  =  y ,  C ,  U. J
) ) )
127124, 126mpbid 202 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  A. x  e.  I  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) )
12820ad3antrrr 711 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  I  e.  _V )
129 mptelixpg 7066 . . . . . . . . . . . . . . 15  |-  ( I  e.  _V  ->  (
( x  e.  I  |->  if ( x  e.  z ,  ( f `
 x ) ,  U ) )  e.  X_ x  e.  I  if ( x  =  y ,  C ,  U. J )  <->  A. x  e.  I  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) ) )
130128, 129syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  (
( x  e.  I  |->  if ( x  e.  z ,  ( f `
 x ) ,  U ) )  e.  X_ x  e.  I  if ( x  =  y ,  C ,  U. J )  <->  A. x  e.  I  if (
x  e.  z ,  ( f `  x
) ,  U )  e.  if ( x  =  y ,  C ,  U. J ) ) )
131127, 130mpbird 224 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  (
x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )
132131ralrimiva 2757 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  A. y  e.  z  ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x
) ,  U ) )  e.  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
) )
133 mptexg 5932 . . . . . . . . . . . . . . 15  |-  ( I  e.  _V  ->  (
x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  _V )
13420, 133syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( x  e.  I  |->  if ( x  e.  z ,  ( f `
 x ) ,  U ) )  e. 
_V )
135134ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x
) ,  U ) )  e.  _V )
136 eliin 4066 . . . . . . . . . . . . 13  |-  ( ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  _V  ->  ( ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U ) )  e.  |^|_ y  e.  z 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J )  <->  A. y  e.  z  ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x
) ,  U ) )  e.  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
) ) )
137135, 136syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( (
x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  |^|_ y  e.  z  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
)  <->  A. y  e.  z  ( x  e.  I  |->  if ( x  e.  z ,  ( f `
 x ) ,  U ) )  e.  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) ) )
138132, 137mpbird 224 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x
) ,  U ) )  e.  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) )
139 elin 3498 . . . . . . . . . . 11  |-  ( ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  (
X_ x  e.  I  U. J  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) )  <-> 
( ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U ) )  e.  X_ x  e.  I  U. J  /\  (
x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  |^|_ y  e.  z  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
) ) )
14095, 138, 139sylanbrc 646 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x
) ,  U ) )  e.  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  z 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) ) )
141 ne0i 3602 . . . . . . . . . 10  |-  ( ( x  e.  I  |->  if ( x  e.  z ,  ( f `  x ) ,  U
) )  e.  (
X_ x  e.  I  U. J  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) )  ->  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
142140, 141syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  z 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) )  =/=  (/) )
14361, 142eqnetrd 2593 . . . . . . . 8  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  ( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) )  =/=  (/) )
144143adantrl 697 . . . . . . 7  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( f : z --> _V  /\  A. x  e.  z  ( f `  x )  e.  C ) )  ->  ( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  z 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J ) )  =/=  (/) )
14558, 144exlimddv 1645 . . . . . 6  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  z  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
14626, 8, 32, 145cmpfiiin 26649 . . . . 5  |-  ( ph  ->  ( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
14725, 146eqnetrd 2593 . . . 4  |-  ( ph  ->  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
1487, 147eqnetrd 2593 . . 3  |-  ( ph  -> 
X_ x  e.  I  C  =/=  (/) )
149 n0 3605 . . 3  |-  ( X_ x  e.  I  C  =/=  (/)  <->  E. y  y  e.  X_ x  e.  I  C )
150148, 149sylib 189 . 2  |-  ( ph  ->  E. y  y  e.  X_ x  e.  I  C )
151 elixp2 7033 . . . . . 6  |-  ( y  e.  X_ x  e.  I  C 
<->  ( y  e.  _V  /\  y  Fn  I  /\  A. x  e.  I  ( y `  x )  e.  C ) )
152151simp3bi 974 . . . . 5  |-  ( y  e.  X_ x  e.  I  C  ->  A. x  e.  I 
( y `  x
)  e.  C )
153 f1ocnv 5654 . . . . . . . . 9  |-  ( B : S -1-1-onto-> C  ->  `' B : C -1-1-onto-> S )
154 f1of 5641 . . . . . . . . 9  |-  ( `' B : C -1-1-onto-> S  ->  `' B : C --> S )
155153, 154syl 16 . . . . . . . 8  |-  ( B : S -1-1-onto-> C  ->  `' B : C --> S )
156 ffvelrn 5835 . . . . . . . . 9  |-  ( ( `' B : C --> S  /\  ( y `  x
)  e.  C )  ->  ( `' B `  ( y `  x
) )  e.  S
)
157156ex 424 . . . . . . . 8  |-  ( `' B : C --> S  -> 
( ( y `  x )  e.  C  ->  ( `' B `  ( y `  x
) )  e.  S
) )
15834, 155, 1573syl 19 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  (
( y `  x
)  e.  C  -> 
( `' B `  ( y `  x
) )  e.  S
) )
159158ralimdva 2752 . . . . . 6  |-  ( ph  ->  ( A. x  e.  I  ( y `  x )  e.  C  ->  A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
160159imp 419 . . . . 5  |-  ( (
ph  /\  A. x  e.  I  ( y `  x )  e.  C
)  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
161152, 160sylan2 461 . . . 4  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
162 mptelixpg 7066 . . . . . 6  |-  ( I  e.  _V  ->  (
( x  e.  I  |->  ( `' B `  ( y `  x
) ) )  e.  X_ x  e.  I  S 
<-> 
A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
16320, 162syl 16 . . . . 5  |-  ( ph  ->  ( ( x  e.  I  |->  ( `' B `  ( y `  x
) ) )  e.  X_ x  e.  I  S 
<-> 
A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
164163adantr 452 . . . 4  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  ( (
x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S  <->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S ) )
165161, 164mpbird 224 . . 3  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S )
166 ne0i 3602 . . 3  |-  ( ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S  ->  X_ x  e.  I  S  =/=  (/) )
167165, 166syl 16 . 2  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  X_ x  e.  I  S  =/=  (/) )
168150, 167exlimddv 1645 1  |-  ( ph  -> 
X_ x  e.  I  S  =/=  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1721    =/= wne 2575   A.wral 2674   E.wrex 2675   _Vcvv 2924    \ cdif 3285    u. cun 3286    i^i cin 3287    C_ wss 3288   (/)c0 3596   ifcif 3707   U.cuni 3983   |^|_ciin 4062    e. cmpt 4234   `'ccnv 4844   "cima 4848    Fn wfn 5416   -->wf 5417   -onto->wfo 5419   -1-1-onto->wf1o 5420   ` cfv 5421   X_cixp 7030   Fincfn 7076   Xt_cpt 13629   Topctop 16921   Clsdccld 17043   Compccmp 17411
This theorem is referenced by:  kelac2  27039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-iin 4064  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-1st 6316  df-2nd 6317  df-recs 6600  df-rdg 6635  df-1o 6691  df-2o 6692  df-oadd 6695  df-er 6872  df-map 6987  df-ixp 7031  df-en 7077  df-dom 7078  df-sdom 7079  df-fin 7080  df-fi 7382  df-topgen 13630  df-pt 13631  df-top 16926  df-bases 16928  df-cld 17046  df-cmp 17412
  Copyright terms: Public domain W3C validator