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

Theorem kelac1 29263
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 2435 . . . . . . . 8  |-  U. J  =  U. J
32cldss 18477 . . . . . . 7  |-  ( C  e.  ( Clsd `  J
)  ->  C  C_  U. J
)
41, 3syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  I )  ->  C  C_ 
U. J )
54ralrimiva 2791 . . . . 5  |-  ( ph  ->  A. x  e.  I  C  C_  U. J )
6 boxriin 7295 . . . . 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 18842 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Comp  ->  (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top )
10 0ntop 18362 . . . . . . . . . . 11  |-  -.  (/)  e.  Top
11 fvprc 5675 . . . . . . . . . . . 12  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( Xt_ `  (
x  e.  I  |->  J ) )  =  (/) )
1211eleq1d 2501 . . . . . . . . . . 11  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top  <->  (/)  e.  Top ) )
1310, 12mtbiri 303 . . . . . . . . . 10  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  -.  ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top )
1413con4i 130 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top  ->  ( x  e.  I  |->  J )  e.  _V )
158, 9, 143syl 20 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J )  e.  _V )
16 kelac1.j . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  J  e.  Top )
17 eqid 2435 . . . . . . . . 9  |-  ( x  e.  I  |->  J )  =  ( x  e.  I  |->  J )
1816, 17fmptd 5857 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J ) : I --> Top )
19 dmfex 6526 . . . . . . . 8  |-  ( ( ( x  e.  I  |->  J )  e.  _V  /\  ( x  e.  I  |->  J ) : I --> Top )  ->  I  e.  _V )
2015, 18, 19syl2anc 656 . . . . . . 7  |-  ( ph  ->  I  e.  _V )
2116ralrimiva 2791 . . . . . . 7  |-  ( ph  ->  A. x  e.  I  J  e.  Top )
22 eqid 2435 . . . . . . . 8  |-  ( Xt_ `  ( x  e.  I  |->  J ) )  =  ( Xt_ `  (
x  e.  I  |->  J ) )
2322ptunimpt 19012 . . . . . . 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 656 . . . . . 6  |-  ( ph  -> 
X_ x  e.  I  U. J  =  U. ( Xt_ `  ( x  e.  I  |->  J ) ) )
2524ineq1d 3541 . . . . 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 2435 . . . . . 6  |-  U. ( Xt_ `  ( x  e.  I  |->  J ) )  =  U. ( Xt_ `  ( x  e.  I  |->  J ) )
272topcld 18483 . . . . . . . . . 10  |-  ( J  e.  Top  ->  U. J  e.  ( Clsd `  J
) )
2816, 27syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  U. J  e.  ( Clsd `  J
) )
29 ifcl 3821 . . . . . . . . 9  |-  ( ( C  e.  ( Clsd `  J )  /\  U. J  e.  ( Clsd `  J ) )  ->  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  J )
)
301, 28, 29syl2anc 656 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  if ( x  =  y ,  C ,  U. J
)  e.  ( Clsd `  J ) )
3120, 16, 30ptcldmpt 19031 . . . . . . 7  |-  ( ph  -> 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  ( Xt_ `  ( x  e.  I  |->  J ) ) ) )
3231adantr 462 . . . . . 6  |-  ( (
ph  /\  y  e.  I )  ->  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
)  e.  ( Clsd `  ( Xt_ `  (
x  e.  I  |->  J ) ) ) )
33 simprr 751 . . . . . . . 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 5638 . . . . . . . . . . . . . . 15  |-  ( B : S -1-1-onto-> C  ->  B : S -onto-> C )
36 foima 5615 . . . . . . . . . . . . . . 15  |-  ( B : S -onto-> C  -> 
( B " S
)  =  C )
3734, 35, 363syl 20 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =  C )
3837eqcomd 2440 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  C  =  ( B " S ) )
39 kelac1.z . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  S  =/=  (/) )
40 f1ofn 5632 . . . . . . . . . . . . . . . . 17  |-  ( B : S -1-1-onto-> C  ->  B  Fn  S )
4134, 40syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  B  Fn  S )
42 ssid 3365 . . . . . . . . . . . . . . . 16  |-  S  C_  S
43 fnimaeq0 5522 . . . . . . . . . . . . . . . 16  |-  ( ( B  Fn  S  /\  S  C_  S )  -> 
( ( B " S )  =  (/)  <->  S  =  (/) ) )
4441, 42, 43sylancl 657 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =  (/)  <->  S  =  (/) ) )
4544necon3bid 2635 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =/=  (/)  <->  S  =/=  (/) ) )
4639, 45mpbird 232 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =/=  (/) )
4738, 46eqnetrd 2618 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  I )  ->  C  =/=  (/) )
48 n0 3636 . . . . . . . . . . . 12  |-  ( C  =/=  (/)  <->  E. w  w  e.  C )
4947, 48sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  I )  ->  E. w  w  e.  C )
50 rexv 2979 . . . . . . . . . . 11  |-  ( E. w  e.  _V  w  e.  C  <->  E. w  w  e.  C )
5149, 50sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  I )  ->  E. w  e.  _V  w  e.  C
)
5251ralrimiva 2791 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  I  E. w  e.  _V  w  e.  C )
53 ssralv 3406 . . . . . . . . . 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 462 . . . . . . . . 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 466 . . . . . . . 8  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  A. x  e.  z  E. w  e.  _V  w  e.  C )
56 eleq1 2495 . . . . . . . . 9  |-  ( w  =  ( f `  x )  ->  (
w  e.  C  <->  ( f `  x )  e.  C
) )
5756ac6sfi 7546 . . . . . . . 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 656 . . . . . . 7  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  E. f ( f : z --> _V  /\  A. x  e.  z  ( f `  x )  e.  C
) )
5924eqcomd 2440 . . . . . . . . . . 11  |-  ( ph  ->  U. ( Xt_ `  (
x  e.  I  |->  J ) )  =  X_ x  e.  I  U. J )
6059ineq1d 3541 . . . . . . . . . 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 720 . . . . . . . . 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 3787 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  z  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  ( f `
 x ) )
6362ad2antrl 722 . . . . . . . . . . . . . . . . . 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 748 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  ph )
65 simprl 750 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
z  C_  I )
6665sselda 3346 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  x  e.  I )
6764, 66, 4syl2anc 656 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  C  C_ 
U. J )
6867sseld 3345 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  (
( f `  x
)  e.  C  -> 
( f `  x
)  e.  U. J
) )
6968impr 616 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  -> 
( f `  x
)  e.  U. J
)
7063, 69eqeltrd 2509 . . . . . . . . . . . . . . . . 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 612 . . . . . . . . . . . . . . . 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 2786 . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . 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 3469 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( I  \ 
z )  ->  -.  x  e.  z )
75 iffalse 3789 . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
78 eldifi 3468 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( I  \ 
z )  ->  x  e.  I )
79 kelac1.u . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  U  e.  U. J )
8078, 79sylan2 471 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
8177, 80eqeltrd 2509 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  U. J
)
8281ralrimiva 2791 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. x  e.  ( I  \  z ) if ( x  e.  z ,  ( f `
 x ) ,  U )  e.  U. J )
8382ad2antrr 720 . . . . . . . . . . . . . 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 3528 . . . . . . . . . . . . . 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 656 . . . . . . . . . . . . 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 3749 . . . . . . . . . . . . . . . . 17  |-  ( z 
C_  I  <->  ( z  u.  ( I  \  z
) )  =  I )
8786biimpi 194 . . . . . . . . . . . . . . . 16  |-  ( z 
C_  I  ->  (
z  u.  ( I 
\  z ) )  =  I )
8887ad2antrl 722 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( z  u.  (
I  \  z )
)  =  I )
8988raleqdv 2915 . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 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 210 . . . . . . . . . . . 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 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  I  e.  _V )
93 mptelixpg 7290 . . . . . . . . . . . . 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 232 . . . . . . . . . . 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 2496 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C  =  if ( x  =  y ,  C ,  U. J )  -> 
( ( f `  x )  e.  C  <->  ( f `  x )  e.  if ( x  =  y ,  C ,  U. J ) ) )
97 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . 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 755 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  (
x  e.  z  /\  ( f `  x
)  e.  C ) )  /\  x  =  y )  ->  (
f `  x )  e.  C )
9969adantr 462 . . . . . . . . . . . . . . . . . . . . . 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 3814 . . . . . . . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . . . . 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 612 . . . . . . . . . . . . . . . . . . 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 2786 . . . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
10776adantl 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
108 incom 3533 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( I  \  z )  i^i  z )  =  ( z  i^i  (
I  \  z )
)
109 disjdif 3741 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  i^i  ( I  \ 
z ) )  =  (/)
110108, 109eqtri 2455 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( I  \  z )  i^i  z )  =  (/)
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  (
( I  \  z
)  i^i  z )  =  (/) )
112 simpr 458 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  e.  ( I  \  z
) )
113 simplr 749 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  y  e.  z )
114 disjne 3714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( I  \ 
z )  i^i  z
)  =  (/)  /\  x  e.  ( I  \  z
)  /\  y  e.  z )  ->  x  =/=  y )
115111, 112, 113, 114syl3anc 1213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  =/=  y )
116115neneqd 2616 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  -.  x  =  y )
117 iffalse 3789 . . . . . . . . . . . . . . . . . . . . 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 2516 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  e.  if ( x  =  y ,  C ,  U. J
) )
120119ralrimiva 2791 . . . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . 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 3528 . . . . . . . . . . . . . . . 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 656 . . . . . . . . . . . . . . 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 2915 . . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  I  e.  _V )
129 mptelixpg 7290 . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . 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 2791 . . . . . . . . . . . 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 5936 . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . 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 4166 . . . . . . . . . . . . 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 232 . . . . . . . . . . 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 ) )
13995, 138elind 3530 . . . . . . . . . 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 ) ) )
140 ne0i 3633 . . . . . . . . . 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
) )  =/=  (/) )
141139, 140syl 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 ) )  =/=  (/) )
14261, 141eqnetrd 2618 . . . . . . . 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 ) )  =/=  (/) )
143142adantrl 710 . . . . . . 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 ) )  =/=  (/) )
14458, 143exlimddv 1693 . . . . . 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
) )  =/=  (/) )
14526, 8, 32, 144cmpfiiin 28880 . . . . 5  |-  ( ph  ->  ( U. ( Xt_ `  ( x  e.  I  |->  J ) )  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
14625, 145eqnetrd 2618 . . . 4  |-  ( ph  ->  ( X_ x  e.  I  U. J  i^i  |^|_ y  e.  I  X_ x  e.  I  if ( x  =  y ,  C ,  U. J
) )  =/=  (/) )
1477, 146eqnetrd 2618 . . 3  |-  ( ph  -> 
X_ x  e.  I  C  =/=  (/) )
148 n0 3636 . . 3  |-  ( X_ x  e.  I  C  =/=  (/)  <->  E. y  y  e.  X_ x  e.  I  C )
149147, 148sylib 196 . 2  |-  ( ph  ->  E. y  y  e.  X_ x  e.  I  C )
150 elixp2 7257 . . . . . 6  |-  ( y  e.  X_ x  e.  I  C 
<->  ( y  e.  _V  /\  y  Fn  I  /\  A. x  e.  I  ( y `  x )  e.  C ) )
151150simp3bi 1000 . . . . 5  |-  ( y  e.  X_ x  e.  I  C  ->  A. x  e.  I 
( y `  x
)  e.  C )
152 f1ocnv 5643 . . . . . . . 8  |-  ( B : S -1-1-onto-> C  ->  `' B : C -1-1-onto-> S )
153 f1of 5631 . . . . . . . 8  |-  ( `' B : C -1-1-onto-> S  ->  `' B : C --> S )
154 ffvelrn 5831 . . . . . . . . 9  |-  ( ( `' B : C --> S  /\  ( y `  x
)  e.  C )  ->  ( `' B `  ( y `  x
) )  e.  S
)
155154ex 434 . . . . . . . 8  |-  ( `' B : C --> S  -> 
( ( y `  x )  e.  C  ->  ( `' B `  ( y `  x
) )  e.  S
) )
15634, 152, 153, 1554syl 21 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  (
( y `  x
)  e.  C  -> 
( `' B `  ( y `  x
) )  e.  S
) )
157156ralimdva 2786 . . . . . 6  |-  ( ph  ->  ( A. x  e.  I  ( y `  x )  e.  C  ->  A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
158157imp 429 . . . . 5  |-  ( (
ph  /\  A. x  e.  I  ( y `  x )  e.  C
)  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
159151, 158sylan2 471 . . . 4  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
160 mptelixpg 7290 . . . . . 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
) )
16120, 160syl 16 . . . . 5  |-  ( ph  ->  ( ( x  e.  I  |->  ( `' B `  ( y `  x
) ) )  e.  X_ x  e.  I  S 
<-> 
A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
162161adantr 462 . . . 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 ) )
163159, 162mpbird 232 . . 3  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S )
164 ne0i 3633 . . 3  |-  ( ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S  ->  X_ x  e.  I  S  =/=  (/) )
165163, 164syl 16 . 2  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  X_ x  e.  I  S  =/=  (/) )
166149, 165exlimddv 1693 1  |-  ( ph  -> 
X_ x  e.  I  S  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364   E.wex 1591    e. wcel 1757    =/= wne 2598   A.wral 2707   E.wrex 2708   _Vcvv 2964    \ cdif 3315    u. cun 3316    i^i cin 3317    C_ wss 3318   (/)c0 3627   ifcif 3781   U.cuni 4081   |^|_ciin 4162    e. cmpt 4340   `'ccnv 4828   "cima 4832    Fn wfn 5403   -->wf 5404   -onto->wfo 5406   -1-1-onto->wf1o 5407   ` cfv 5408   X_cixp 7253   Fincfn 7300   Xt_cpt 14362   Topctop 18342   Clsdccld 18464   Compccmp 18833
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 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-iin 4164  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-1st 6568  df-2nd 6569  df-recs 6820  df-rdg 6854  df-1o 6910  df-2o 6911  df-oadd 6914  df-er 7091  df-map 7206  df-ixp 7254  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304  df-fi 7651  df-topgen 14367  df-pt 14368  df-top 18347  df-bases 18349  df-cld 18467  df-cmp 18834
This theorem is referenced by:  kelac2  29265
  Copyright terms: Public domain W3C validator