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 27152
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 2438 . . . . . . . 8  |-  U. J  =  U. J
32cldss 17098 . . . . . . 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 7107 . . . . 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 17463 . . . . . . . . 9  |-  ( (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Comp  ->  (
Xt_ `  ( x  e.  I  |->  J ) )  e.  Top )
10 0ntop 16983 . . . . . . . . . . 11  |-  -.  (/)  e.  Top
11 fvprc 5725 . . . . . . . . . . . 12  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( Xt_ `  (
x  e.  I  |->  J ) )  =  (/) )
1211eleq1d 2504 . . . . . . . . . . 11  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  ( ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top  <->  (/)  e.  Top ) )
1310, 12mtbiri 296 . . . . . . . . . 10  |-  ( -.  ( x  e.  I  |->  J )  e.  _V  ->  -.  ( Xt_ `  (
x  e.  I  |->  J ) )  e.  Top )
1413con4i 125 . . . . . . . . 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 2438 . . . . . . . . 9  |-  ( x  e.  I  |->  J )  =  ( x  e.  I  |->  J )
1816, 17fmptd 5896 . . . . . . . 8  |-  ( ph  ->  ( x  e.  I  |->  J ) : I --> Top )
19 dmfex 5629 . . . . . . . 8  |-  ( ( ( x  e.  I  |->  J )  e.  _V  /\  ( x  e.  I  |->  J ) : I --> Top )  ->  I  e.  _V )
2015, 18, 19syl2anc 644 . . . . . . 7  |-  ( ph  ->  I  e.  _V )
2116ralrimiva 2791 . . . . . . 7  |-  ( ph  ->  A. x  e.  I  J  e.  Top )
22 eqid 2438 . . . . . . . 8  |-  ( Xt_ `  ( x  e.  I  |->  J ) )  =  ( Xt_ `  (
x  e.  I  |->  J ) )
2322ptunimpt 17632 . . . . . . 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 644 . . . . . 6  |-  ( ph  -> 
X_ x  e.  I  U. J  =  U. ( Xt_ `  ( x  e.  I  |->  J ) ) )
2524ineq1d 3543 . . . . 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 2438 . . . . . 6  |-  U. ( Xt_ `  ( x  e.  I  |->  J ) )  =  U. ( Xt_ `  ( x  e.  I  |->  J ) )
272topcld 17104 . . . . . . . . . 10  |-  ( J  e.  Top  ->  U. J  e.  ( Clsd `  J
) )
2816, 27syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  I )  ->  U. J  e.  ( Clsd `  J
) )
29 ifcl 3777 . . . . . . . . 9  |-  ( ( C  e.  ( Clsd `  J )  /\  U. J  e.  ( Clsd `  J ) )  ->  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  J )
)
301, 28, 29syl2anc 644 . . . . . . . 8  |-  ( (
ph  /\  x  e.  I )  ->  if ( x  =  y ,  C ,  U. J
)  e.  ( Clsd `  J ) )
3120, 16, 30ptcldmpt 17651 . . . . . . 7  |-  ( ph  -> 
X_ x  e.  I  if ( x  =  y ,  C ,  U. J )  e.  (
Clsd `  ( Xt_ `  ( x  e.  I  |->  J ) ) ) )
3231adantr 453 . . . . . 6  |-  ( (
ph  /\  y  e.  I )  ->  X_ x  e.  I  if (
x  =  y ,  C ,  U. J
)  e.  ( Clsd `  ( Xt_ `  (
x  e.  I  |->  J ) ) ) )
33 simprr 735 . . . . . . . 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 5684 . . . . . . . . . . . . . . 15  |-  ( B : S -1-1-onto-> C  ->  B : S -onto-> C )
36 foima 5661 . . . . . . . . . . . . . . 15  |-  ( B : S -onto-> C  -> 
( B " S
)  =  C )
3734, 35, 363syl 19 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =  C )
3837eqcomd 2443 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  C  =  ( B " S ) )
39 kelac1.z . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  S  =/=  (/) )
40 f1ofn 5678 . . . . . . . . . . . . . . . . 17  |-  ( B : S -1-1-onto-> C  ->  B  Fn  S )
4134, 40syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  I )  ->  B  Fn  S )
42 ssid 3369 . . . . . . . . . . . . . . . 16  |-  S  C_  S
43 fnimaeq0 5569 . . . . . . . . . . . . . . . 16  |-  ( ( B  Fn  S  /\  S  C_  S )  -> 
( ( B " S )  =  (/)  <->  S  =  (/) ) )
4441, 42, 43sylancl 645 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =  (/)  <->  S  =  (/) ) )
4544necon3bid 2638 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  I )  ->  (
( B " S
)  =/=  (/)  <->  S  =/=  (/) ) )
4639, 45mpbird 225 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  I )  ->  ( B " S )  =/=  (/) )
4738, 46eqnetrd 2621 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  I )  ->  C  =/=  (/) )
48 n0 3639 . . . . . . . . . . . 12  |-  ( C  =/=  (/)  <->  E. w  w  e.  C )
4947, 48sylib 190 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  I )  ->  E. w  w  e.  C )
50 rexv 2972 . . . . . . . . . . 11  |-  ( E. w  e.  _V  w  e.  C  <->  E. w  w  e.  C )
5149, 50sylibr 205 . . . . . . . . . 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 3409 . . . . . . . . . 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 453 . . . . . . . . 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 457 . . . . . . . 8  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  A. x  e.  z  E. w  e.  _V  w  e.  C )
56 eleq1 2498 . . . . . . . . 9  |-  ( w  =  ( f `  x )  ->  (
w  e.  C  <->  ( f `  x )  e.  C
) )
5756ac6sfi 7354 . . . . . . . 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 644 . . . . . . 7  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  ->  E. f ( f : z --> _V  /\  A. x  e.  z  ( f `  x )  e.  C
) )
5924eqcomd 2443 . . . . . . . . . . 11  |-  ( ph  ->  U. ( Xt_ `  (
x  e.  I  |->  J ) )  =  X_ x  e.  I  U. J )
6059ineq1d 3543 . . . . . . . . . 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 708 . . . . . . . . 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 3747 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  z  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  ( f `
 x ) )
6362ad2antrl 710 . . . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  ph )
65 simprl 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
z  C_  I )
6665sselda 3350 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  x  e.  I )
6764, 66, 4syl2anc 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  C  C_ 
U. J )
6867sseld 3349 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  x  e.  z )  ->  (
( f `  x
)  e.  C  -> 
( f `  x
)  e.  U. J
) )
6968impr 604 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  ( x  e.  z  /\  (
f `  x )  e.  C ) )  -> 
( f `  x
)  e.  U. J
)
7063, 69eqeltrd 2512 . . . . . . . . . . . . . . . . 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 600 . . . . . . . . . . . . . . . 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 420 . . . . . . . . . . . . . 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 3472 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( I  \ 
z )  ->  -.  x  e.  z )
75 iffalse 3748 . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
78 eldifi 3471 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ( I  \ 
z )  ->  x  e.  I )
79 kelac1.u . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  I )  ->  U  e.  U. J )
8078, 79sylan2 462 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
8177, 80eqeltrd 2512 . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . 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 3531 . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . 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 3710 . . . . . . . . . . . . . . . . 17  |-  ( z 
C_  I  <->  ( z  u.  ( I  \  z
) )  =  I )
8786biimpi 188 . . . . . . . . . . . . . . . 16  |-  ( z 
C_  I  ->  (
z  u.  ( I 
\  z ) )  =  I )
8887ad2antrl 710 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  C_  I  /\  z  e. 
Fin ) )  -> 
( z  u.  (
I  \  z )
)  =  I )
8988raleqdv 2912 . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . 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 203 . . . . . . . . . . . 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 708 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  C_  I  /\  z  e.  Fin )
)  /\  A. x  e.  z  ( f `  x )  e.  C
)  ->  I  e.  _V )
93 mptelixpg 7102 . . . . . . . . . . . . 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 225 . . . . . . . . . . 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 2499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C  =  if ( x  =  y ,  C ,  U. J )  -> 
( ( f `  x )  e.  C  <->  ( f `  x )  e.  if ( x  =  y ,  C ,  U. J ) ) )
97 eleq2 2499 . . . . . . . . . . . . . . . . . . . . . 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 739 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  (
x  e.  z  /\  ( f `  x
)  e.  C ) )  /\  x  =  y )  ->  (
f `  x )  e.  C )
9969adantr 453 . . . . . . . . . . . . . . . . . . . . . 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 3771 . . . . . . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . . . . . . . . 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 600 . . . . . . . . . . . . . . . . . . 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 420 . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  U  e.  U. J )
10776adantl 454 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  if ( x  e.  z ,  ( f `  x ) ,  U
)  =  U )
108 incom 3535 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( I  \  z )  i^i  z )  =  ( z  i^i  (
I  \  z )
)
109 disjdif 3702 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  i^i  ( I  \ 
z ) )  =  (/)
110108, 109eqtri 2458 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( I  \  z )  i^i  z )  =  (/)
111110a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  (
( I  \  z
)  i^i  z )  =  (/) )
112 simpr 449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  e.  ( I  \  z
) )
113 simplr 733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  y  e.  z )
114 disjne 3675 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( I  \ 
z )  i^i  z
)  =  (/)  /\  x  e.  ( I  \  z
)  /\  y  e.  z )  ->  x  =/=  y )
115111, 112, 113, 114syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  x  =/=  y )
116115neneqd 2619 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  z )  /\  x  e.  ( I  \  z
) )  ->  -.  x  =  y )
117 iffalse 3748 . . . . . . . . . . . . . . . . . . . . 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 2519 . . . . . . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . . . . 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 3531 . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . 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 2912 . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  C_  I  /\  z  e.  Fin ) )  /\  A. x  e.  z  (
f `  x )  e.  C )  /\  y  e.  z )  ->  I  e.  _V )
129 mptelixpg 7102 . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . 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 5968 . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . 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 4100 . . . . . . . . . . . . 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 225 . . . . . . . . . . 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 3532 . . . . . . . . . . 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 647 . . . . . . . . . 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 3636 . . . . . . . . . 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 2621 . . . . . . . 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 698 . . . . . . 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 1649 . . . . . 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 26765 . . . . 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 2621 . . . 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 2621 . . 3  |-  ( ph  -> 
X_ x  e.  I  C  =/=  (/) )
149 n0 3639 . . 3  |-  ( X_ x  e.  I  C  =/=  (/)  <->  E. y  y  e.  X_ x  e.  I  C )
150148, 149sylib 190 . 2  |-  ( ph  ->  E. y  y  e.  X_ x  e.  I  C )
151 elixp2 7069 . . . . . 6  |-  ( y  e.  X_ x  e.  I  C 
<->  ( y  e.  _V  /\  y  Fn  I  /\  A. x  e.  I  ( y `  x )  e.  C ) )
152151simp3bi 975 . . . . 5  |-  ( y  e.  X_ x  e.  I  C  ->  A. x  e.  I 
( y `  x
)  e.  C )
153 f1ocnv 5690 . . . . . . . 8  |-  ( B : S -1-1-onto-> C  ->  `' B : C -1-1-onto-> S )
154 f1of 5677 . . . . . . . 8  |-  ( `' B : C -1-1-onto-> S  ->  `' B : C --> S )
155 ffvelrn 5871 . . . . . . . . 9  |-  ( ( `' B : C --> S  /\  ( y `  x
)  e.  C )  ->  ( `' B `  ( y `  x
) )  e.  S
)
156155ex 425 . . . . . . . 8  |-  ( `' B : C --> S  -> 
( ( y `  x )  e.  C  ->  ( `' B `  ( y `  x
) )  e.  S
) )
15734, 153, 154, 1564syl 20 . . . . . . 7  |-  ( (
ph  /\  x  e.  I )  ->  (
( y `  x
)  e.  C  -> 
( `' B `  ( y `  x
) )  e.  S
) )
158157ralimdva 2786 . . . . . 6  |-  ( ph  ->  ( A. x  e.  I  ( y `  x )  e.  C  ->  A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
159158imp 420 . . . . 5  |-  ( (
ph  /\  A. x  e.  I  ( y `  x )  e.  C
)  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
160152, 159sylan2 462 . . . 4  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  A. x  e.  I  ( `' B `  ( y `  x ) )  e.  S )
161 mptelixpg 7102 . . . . . 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
) )
16220, 161syl 16 . . . . 5  |-  ( ph  ->  ( ( x  e.  I  |->  ( `' B `  ( y `  x
) ) )  e.  X_ x  e.  I  S 
<-> 
A. x  e.  I 
( `' B `  ( y `  x
) )  e.  S
) )
163162adantr 453 . . . 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 ) )
164160, 163mpbird 225 . . 3  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S )
165 ne0i 3636 . . 3  |-  ( ( x  e.  I  |->  ( `' B `  ( y `
 x ) ) )  e.  X_ x  e.  I  S  ->  X_ x  e.  I  S  =/=  (/) )
166164, 165syl 16 . 2  |-  ( (
ph  /\  y  e.  X_ x  e.  I  C )  ->  X_ x  e.  I  S  =/=  (/) )
167150, 166exlimddv 1649 1  |-  ( ph  -> 
X_ x  e.  I  S  =/=  (/) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726    =/= wne 2601   A.wral 2707   E.wrex 2708   _Vcvv 2958    \ cdif 3319    u. cun 3320    i^i cin 3321    C_ wss 3322   (/)c0 3630   ifcif 3741   U.cuni 4017   |^|_ciin 4096    e. cmpt 4269   `'ccnv 4880   "cima 4884    Fn wfn 5452   -->wf 5453   -onto->wfo 5455   -1-1-onto->wf1o 5456   ` cfv 5457   X_cixp 7066   Fincfn 7112   Xt_cpt 13671   Topctop 16963   Clsdccld 17085   Compccmp 17454
This theorem is referenced by:  kelac2  27154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-recs 6636  df-rdg 6671  df-1o 6727  df-2o 6728  df-oadd 6731  df-er 6908  df-map 7023  df-ixp 7067  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-fi 7419  df-topgen 13672  df-pt 13673  df-top 16968  df-bases 16970  df-cld 17088  df-cmp 17455
  Copyright terms: Public domain W3C validator